Library mcertikos.layerlib.ArithLemma

Require Export Arith.
Require Export Omega.
Require Export ZArith.
Require Export Bool.
Require Export Datatypes.
Require Export Coqlib.
Require Export AuxFunctions.

Open Scope nat_scope.
Lemma x_s1_p1_0:
  ∀ x: nat,
    x ≥ 1 →
    x - 1 + 1 = x.
Proof.
  intros. rewrite <- NPeano.Nat.add_sub_swap. rewrite plus_comm. rewrite minus_plus. reflexivity.
  omega.
Qed.

Lemma psum_true:
  ∀ {T: Type} {P} {Q} {dec: {P} + {Q}} {t1: T} {t2: T},
    (∃ b, dec = left b) →
    (if proj_sumbool dec then t1 else t2) = t1.
Proof.
  intros. destruct H. subst. simpl. trivial.
Qed.

Lemma psum_false:
  ∀ {T: Type} {P} {Q} {dec: {P} + {Q}} {t1: T} {t2: T},
    (∃ b, dec = right b) →
    (if proj_sumbool dec then t1 else t2) = t2.
Proof.
  intros. destruct H. subst. simpl. trivial.
Qed.

Lemma proj_sumbool_left:
  ∀ {A B: Prop} (a: A),
    proj_sumbool (@left A B a) = true.
Proof.
  simpl. trivial.
Qed.

Lemma proj_sumbool_right:
  ∀ {A B: Prop} (b: B),
    proj_sumbool (@right A B b) = false.
Proof.
  simpl. trivial.
Qed.

Open Scope Z_scope.
Lemma Z_succ_pred:
  ∀ x, Z.succ x - 1 = x.
Proof.
  intros. omega.
Qed.

Lemma Z_OF_NAT_0: Z.of_nat 0 = 0. compute. reflexivity. Qed.
Lemma Z_OF_NAT_1: Z.of_nat 1 = 1. compute. reflexivity. Qed.
Lemma Z_OF_NAT_2: Z.of_nat 2 = 2. compute. reflexivity. Qed.
Lemma Z_OF_NAT_512: Z.of_nat 512 = 512. compute. reflexivity. Qed.

Lemma Z_TO_NAT_1: Z.to_nat 1 = 1%nat. compute. reflexivity. Qed.

Lemma gt_eq_point:
  ∀ a b c,
    a + b > c →
    0 ≤ b < c →
    ∃ a´, a´ + b = c.
Proof.
  intros. ∃ (c - b). omega.
Qed.

Lemma Z_add_mod_0:
  ∀ a n,
    n ≠ 0 →
    (a + 0) mod n = a mod n.
Proof.
  intros. rewrite Z.add_0_r. reflexivity.
Qed.

Lemma Z_add_mod_0_l:
  ∀ a n,
    n ≠ 0 →
    (0 + a) mod n = a mod n.
Proof.
  intros. rewrite Z.add_0_l. reflexivity.
Qed.

Lemma Z_add_mod_same:
  ∀ a n,
    n ≠ 0 →
    (a + n) mod n = a mod n.
Proof.
  intros.
  rewrite Z.add_mod by omega. rewrite Z.mod_same by omega.
  rewrite Z_add_mod_0 by omega. rewrite Z.mod_mod by omega.
  reflexivity.
Qed.

Lemma Z_add_mod_same_l:
  ∀ a n,
    n ≠ 0 →
    (n + a) mod n = a mod n.
Proof.
  intros. rewrite Z.add_comm. apply Z_add_mod_same; auto.
Qed.

Lemma Z_add_mod_lt:
  ∀ a n,
    0 ≤ a < n →
    0 ≤ (a + 1) mod n < n.
Proof.
  intros.
  assert (Hcase: 0 ≤ a < (n - 1) ∨ a = n - 1) by omega. destruct Hcase.
  - apply (Z_mod_lt (a + 1) n); omega.
  - subst. replace (n - 1 + 1) with n by omega. rewrite Z.mod_same; omega.
Qed.

Lemma Z_add_mod_comm:
  ∀ a b c n,
    n ≠ 0 →
    ((a + b) mod n + (c mod n)) mod n = (a + b + c) mod n.
Proof.
  intros.
  rewrite <- Z.add_mod by omega. reflexivity.
Qed.

Lemma Z_add_mod_comm_le:
  ∀ a b c n,
    n ≠ 0 →
    0 ≤ c < n →
    ((a + b) mod n + c) mod n = (a + b + c) mod n.
Proof.
  intros.
  replace ((a+b) mod n + c) with ((a+b) mod n + c mod n).
  rewrite Z_add_mod_comm by omega. reflexivity.
  rewrite (Z.mod_small c); omega.
Qed.

Lemma Z_minus_comm:
  ∀ n m,
    n - m = -m + n.
Proof.
  intros.
  omega.
Qed.

Lemma Z_minus_comm_minus:
  ∀ n m,
    -n - m = -m - n.
Proof.
  intros.
  omega.
Qed.

Lemma Z_minus_assoc_plus:
  ∀ a b c,
    a - (b + c) = a - b - c.
Proof.
  intros. omega.
Qed.

Lemma Z_minus_assoc_minus:
  ∀ a b c,
    a - (b - c) = a - b + c.
Proof.
  intros. omega.
Qed.

Lemma Z_plus_assoc_minus:
  ∀ a b c,
    a + (b - c) = a + b - c.
Proof.
  intros. omega.
Qed.

Lemma zle_le_true_ex:
  ∀ a b c: Z,
    a ≤ b ≤ c →
    ∃ x, zle_le a b c = left x.
Proof.
  intros. destruct (zle_le a b c).
  - ∃ a0. trivial.
  - omega.
Qed.

Lemma true_ex:
  ∀ {p q: Prop} (dec: {p} + {q}),
    p →
    ¬ q →
    ∃ x, dec = left x.
Proof.
  intros. destruct dec.
  - ∃ p0. trivial.
  - contradiction.
Qed.

Lemma false_ex:
  ∀ {p q: Prop} (dec: {p} + {q}),
    ¬ p →
    q →
    ∃ x, dec = right x.
Proof.
  intros. destruct dec.
  - contradiction.
  - ∃ q0. trivial.
Qed.

Lemma if_dec_true:
  ∀ {T: Type} {t1 t2: T} {p q: Prop} (dec: {p} + {q}),
    p →
    ¬q →
    (if dec then t1 else t2) = t1.
Proof.
  intros. destruct dec. trivial. contradiction.
Qed.

Lemma if_dec_false:
  ∀ {T: Type} {t1 t2: T} {p q: Prop} (dec: {p} + {q}),
    ¬p →
    q →
    (if dec then t1 else t2) = t2.
Proof.
  intros. destruct dec. contradiction. trivial.
Qed.

Lemma if_bool_true:
  ∀ {T: Type} {t1 t2: T} (b: bool),
    b = true →
    (if b then t1 else t2) = t1.
Proof.
  intros. subst. reflexivity.
Qed.

Lemma if_bool_false:
  ∀ {T: Type} {t1 t2: T} (b: bool),
    b = false →
    (if b then t1 else t2) = t2.
Proof.
  intros. subst. reflexivity.
Qed.

Lemma Z_even_mod:
  ∀ n,
    (n × 2) mod 2 = 0.
Proof.
  intros. rewrite Z_mod_mult. trivial.
Qed.

Lemma Z_odd_mod:
  ∀ n,
    (n × 2 + 1) mod 2 = 1.
Proof.
  intros. rewrite Z.add_mod. rewrite Z_even_mod. compute. reflexivity.
  omega.
Qed.

Lemma Z_neg_absurd:
  ∀ p,
    Z.neg p ≥ 0 → False.
Proof.
  intros.
  pose proof (Zlt_neg_0 p). omega.
Qed.

Lemma Z_mult_div:
  ∀ a b,
    b > 0 →
    a mod b = 0 →
    a / b × b = a.
Proof.
  intros.
  rewrite Z.mul_comm.
  rewrite Z_div_exact_2 with (b:=b). trivial.
  assumption. assumption.
Qed.

Lemma Z_mult_mod:
  ∀ a b n,
    n ≠ 0 →
    a mod n = 0 →
    (a × b) mod n = 0.
Proof.
  intros. rewrite Z.mul_mod by assumption. rewrite H0.
  rewrite Z.mul_0_l. rewrite Z.mod_0_l by assumption. reflexivity.
Qed.

Lemma succ_lt_lt:
  ∀ x y, Z.succ x < y → x < y.
Proof.
  intros. omega.
Qed.

Require Import XOmega.

Lemma mod_2_testbit:
  ∀ x,
    (x mod 2 =? 1) = Z.testbit x 0.
Proof.
  intros.
  rewrite Z.testbit_eqb with (a:=x)(n:=0).
  change (2 ^ 0) with 1. rewrite Zdiv_1_r. reflexivity.
  omega.
Qed.

Lemma mod_2_testbit_true:
  ∀ x,
    Z.testbit x 0 = true →
    x mod 2 = 1.
Proof.
  intros.
  generalize (mod_2_testbit x).
  assert (Ham2: x mod 2 = 1 ∨ x mod 2 = 0) by xomega.
  destruct Ham2 as [Ham2 | Ham2].
  - rewrite Ham2. simpl. intros. reflexivity.
  - rewrite Ham2. rewrite H. simpl. inversion 1.
Qed.

Lemma mod_2_testbit_false:
  ∀ x,
    Z.testbit x 0 = false →
    x mod 2 = 0.
Proof.
  intros.
  generalize (mod_2_testbit x).
  assert (Ham2: x mod 2 = 1 ∨ x mod 2 = 0) by xomega.
  destruct Ham2 as [Ham2 | Ham2].
  - rewrite Ham2. rewrite H. simpl. inversion 1.
  - rewrite Ham2. simpl. intros. reflexivity.
Qed.

Lemma lor_mod_2:
  ∀ n a,
    (n > 0)% nat →
    Z.lor a (2 ^ Z.of_nat n) mod 2 = a mod 2.
Proof.
  intros.
  rewrite <- Z.setbit_spec´.
  assert (Ham2: a mod 2 = 1 ∨ a mod 2 = 0) by xomega.
  destruct Ham2 as [Ham2 | Ham2].
  {
    rewrite Ham2. apply mod_2_testbit_true.
    rewrite Z.setbit_neq. rewrite <- mod_2_testbit. rewrite Ham2. reflexivity.
    omega. omega.
  }
  {
    rewrite Ham2. apply mod_2_testbit_false.
    rewrite Z.setbit_neq. rewrite <- mod_2_testbit. rewrite Ham2. reflexivity.
    omega. omega.
  }
Qed.

Lemma lor_eq_plus:
  ∀ (n: nat) a b,
    0 ≤ a < 2 ^ (Z.of_nat n) →
    b = 2 ^ (Z.of_nat n) →
    Z.lor a b = a + b.
Proof.
  induction n.
  - simpl. intros. assert (a = 0) by omega. rewrite H0, H1.
    reflexivity.
  - intros.
    assert (nge0: 0 ≤ Z.of_nat n) by omega.
    generalize (Z.pow_succ_r 2 _ nge0); intro pow_succ.
    unfold Z.succ in pow_succ.
    replace (Z.of_nat n + 1) with (Z.of_nat (S n)) in pow_succ by xomega.
    assert (0 ≤ a / 2 < 2 ^ Z.of_nat n).
    {
      assert (2 > 0) by omega.
      assert (a ≤ 2 ^ Z.of_nat (S n) - 1) by omega.
      generalize (Z_div_le _ _ _ H1 H2); intro.
      xomega.
    }
    assert (b / 2 = 2 ^ Z.of_nat n) by xomega.
    generalize (IHn _ _ H1 H2); intros.
    assert (Z.lor a b = 2 × (Z.lor (a / 2) (b / 2)) + a mod 2).
    {
      assert (Z.shiftr (Z.lor a b) 1 = Z.lor (Z.shiftr a 1) (Z.shiftr b 1)) by apply Z.shiftr_lor.
      assert (0 ≤ 1) by omega.
      repeat rewrite Z.shiftr_div_pow2 in H4 by assumption.
      change (2 ^ 1) with 2 in H4.
      assert (Z.lor a b = Z.lor a b / 2 × 2 + Z.lor a b mod 2) by xomega.
      rewrite H6.
      rewrite H4.
      assert ((S n > 0)%nat) by omega.
      generalize (lor_mod_2 (S n) a H7); intro.
      rewrite H0 in ×.
      xomega.
    }
    assert (a + b = (a / 2 + b / 2) × 2 + a mod 2) by xomega.
    omega.
Qed.

Lemma lor_plus_eq_plus:
  ∀ (n: nat) a b,
    0 ≤ a < 2 ^ (Z.of_nat n) →
    b = 2 ^ (Z.of_nat n) →
    Z.lor (a + b) b = a + b.
Proof.
  intros.
  rewrite <- lor_eq_plus with (n:=n); try omega.
  rewrite <- Z.lor_assoc. rewrite Z.lor_diag. reflexivity.
Qed.

Lemma ones_spec:
  ∀ n,
    0 ≤ n →
    Z.ones n = 2 ^ n - 1.
Proof.
  intros. unfold Z.ones. unfold Z.pred.
  rewrite Z.shiftl_mul_pow2; omega.
Qed.

Lemma land_eq_smaller:
  ∀ (n: nat) a b,
    (0 ≤ n)%nat →
    b = 2 ^ (Z.of_nat n) - 1 →
    Z.land a b = a mod (2 ^ (Z.of_nat n)).
Proof.
  intros n a b Hn Hb.
  rewrite Hb.
  rewrite <- ones_spec by omega.
  rewrite Z.land_ones; omega.
Qed.

Lemma Zdiv2_cases:
  ∀ x,
    x / 2 = 0 →
    x = 0 ∨ x = 1.
Proof.
  intros.
  xomega.
Qed.

Lemma Zland_mod_spec:
  ∀ x y,
    Z.land x y = 1 →
    x mod 2 = 1 ∧ y mod 2 = 1.
Proof.
  intros.
  remember (Z.land x y) as k.
  assert (k mod 2 = 1). rewrite H. reflexivity.
  generalize (Z.testbit_true k 0).
  replace (k / 2 ^ 0) with k. intros.
  apply H1 in H0. subst.
  rewrite Z.land_spec in H0.
  apply andb_true_iff in H0.
  destruct H0 as [Hx Hy].
  apply mod_2_testbit_true in Hx.
  apply mod_2_testbit_true in Hy.
  omega.
  omega.
  {
    change (2 ^ 0) with 1. rewrite Zdiv_1_r. reflexivity.
  }
Qed.

Lemma Zmod_even:
  ∀ n x,
    (0 < n)%nat →
    x mod (2 ^ (Z.of_nat n)) = 0 →
    x mod 2 = 0.
Proof.
  induction n.
  - simpl. intros. omega.
  - rewrite Nat2Z.inj_succ. remember (Z.of_nat n) as nn.
    rewrite <- Z.add_1_r. rewrite Zpower_exp by omega.
    change (2 ^ 1) with 2.
    intros.
    assert (ncase: (n = 0)%nat ∨ (n ≠ 0)%nat) by omega.
    case_eq ncase; intros.
    {
      subst.
      apply H0.
    }
    {
      eapply IHn.
      omega.
      subst.
      assert (0 < 2 ^ Z.of_nat n).
      {
        apply Z.pow_pos_nonneg.
        omega.
        xomega.
      }
      rewrite Z.mod_eq.
      rewrite <- Z.divide_div_mul_exact.
      rewrite Z.mul_comm.
      rewrite Z.divide_div_mul_exact.
      rewrite Z_div_same_full.
      omega.
      omega.
      omega.
      unfold Z.divide.
      ∃ 1; omega.
      omega.
      unfold Z.divide.
      eapply Zmod_divide in H0.
      unfold Z.divide in H0.
      destruct H0.
      ∃ (x0 × 2).
      rewrite H0.
      rewrite Zmult_assoc_reverse.
      rewrite Z.mul_comm with (n:= 2).
      reflexivity.
      omega.
      omega.
    }
Qed.

Lemma land_eq_0:
  ∀ (n: nat) a b,
    0 ≤ a < 2 ^ (Z.of_nat n) →
    b mod (2 ^ (Z.of_nat n)) = 0 →
    Z.land a b = 0.
Proof.
  induction n.
  - simpl. intros.
    assert (Ha: a = 0) by omega.
    rewrite Ha. simpl. reflexivity.
  - intros.
    assert (nge0: 0 ≤ Z.of_nat n) by omega.
    generalize (Z.pow_succ_r 2 _ nge0); intro pow_succ.
    unfold Z.succ in pow_succ.
    replace (Z.of_nat n + 1) with (Z.of_nat (S n)) in pow_succ by xomega.
    assert (0 ≤ a / 2 < 2 ^ Z.of_nat n).
    {
      assert (2 > 0) by omega.
      assert (a ≤ 2 ^ Z.of_nat (S n) - 1) by omega.
      generalize (Z_div_le _ _ _ H1 H2); intro.
      xomega.
    }
    assert ((b/2) mod 2 ^ Z.of_nat n = 0).
    {
      rewrite pow_succ in H0.
      rewrite Z.mul_comm in H0.
      rewrite Zmod_recombine in H0 by xomega.
      xomega.
    }
    generalize (IHn (a / 2) (b / 2) H1 H2).
    repeat (rewrite <- Zdiv2_div; rewrite Z.div2_spec).
    rewrite <- Z.shiftr_land. rewrite <- Z.div2_spec.
    rewrite Zdiv2_div.
    remember (Z.land a b) as x.
    intros Hspec. apply Zdiv2_cases in Hspec.
    destruct Hspec.
    + assumption.
    +
      subst.
      apply Zland_mod_spec in H3. destruct H3.
      apply Zmod_even in H0. omega. omega.
Qed.