Require Import Coq.ZArith.BinInt.
Require Import Coq.micromega.Lia.
Require Import Coq.ZArith.ZArith.

Local Open Scope Z_scope.


Lemma mod2_cases: forall (n: Z), n mod 2 = 0 \/ n mod 2 = 1.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. pose proof (Z.mod_pos_bound n 2). omega.
Qed.

Lemma div_mul_undo: forall a b,
    b <> 0 ->
    a mod b = 0 ->
    a / b * b = a.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: @eq Z (Z.mul (Z.div a b) b) a *)
  pose proof Z.div_mul_cancel_l as A. specialize (A a 1 b).
(* Goal: False *)
  replace (b * 1) with b in A by omega.
(* Goal: @eq Z (Z.mul (Z.div a b) b) a *)
  rewrite Z.div_1_r in A.
(* Goal: @eq Z b (Z.modulo (Z.add (Z.modulo (Z.mul base a) base) b) base) *)
  rewrite Z.mul_comm.
(* Goal: @eq Z (Z.mul b (Z.div a b)) a *)
  rewrite <- Z.divide_div_mul_exact; try assumption.
  - apply A; congruence.
  - apply Z.mod_divide; assumption.
Qed.

Lemma mod_0_r: forall (m: Z),
    m mod 0 = 0.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. destruct m; reflexivity.
Qed.

Lemma sub_mod_0: forall (a b m: Z),
    a mod m = 0 ->
    b mod m = 0 ->
    (a - b) mod m = 0.
Proof.
(* Goal: forall (a b m : Z) (_ : @eq Z (Z.modulo a m) Z0) (_ : @eq Z (Z.modulo b m) Z0), @eq Z (Z.modulo (Z.add a b) m) Z0 *)
  intros *. intros E1 E2.
(* Goal: @eq Z (Z.modulo (Z.sub a b) m) Z0 *)
  rewrite Zminus_mod.
(* Goal: @eq Z (Z.modulo (Z.add (Z.modulo a m) (Z.modulo b m)) m) Z0 *)
  rewrite E1. rewrite E2.
(* Goal: @eq Z b b *)
  reflexivity.
Qed.

Lemma add_mod_0: forall a b m : Z,
    a mod m = 0 ->
    b mod m = 0 ->
    (a + b) mod m = 0.
Proof.
(* Goal: forall (a b m : Z) (_ : @eq Z (Z.modulo a m) Z0) (_ : @eq Z (Z.modulo b m) Z0), @eq Z (Z.modulo (Z.add a b) m) Z0 *)
  intros *. intros E1 E2.
(* Goal: @eq Z (Z.modulo (Z.add a b) m) Z0 *)
  rewrite Zplus_mod.
(* Goal: @eq Z (Z.modulo (Z.add (Z.modulo a m) (Z.modulo b m)) m) Z0 *)
  rewrite E1. rewrite E2.
(* Goal: @eq Z b b *)
  reflexivity.
Qed.

Lemma Z_mod_mult': forall a b : Z,
    (a * b) mod a = 0.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. rewrite Z.mul_comm. apply Z_mod_mult.
Qed.

Lemma mod_add_r: forall a b,
    b <> 0 ->
    (a + b) mod b = a mod b.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. rewrite <- Z.add_mod_idemp_r by omega.
(* Goal: False *)
  rewrite Z.mod_same by omega.
(* Goal: @eq Z (Z.modulo (Z.add a Z0) b) (Z.modulo a b) *)
  rewrite Z.add_0_r.
(* Goal: @eq Z b b *)
  reflexivity.
Qed.

Lemma mod_pow2_same_cases: forall a n,
    a mod 2 ^ n = a ->
    2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: False *)
  assert (n < 0 \/ 0 <= n) as C by omega. destruct C as [C | C].
  - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto.
  - right.
    rewrite <- H. apply Z.mod_pos_bound.
(* Goal: False *)
    apply Z.pow_pos_nonneg; omega.
Qed.    

Lemma mod_pow2_same_bounds: forall a n,
    a mod 2 ^ n = a ->
    0 <= n ->
    0 <= a < 2 ^ n.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. rewrite <- H. apply Z.mod_pos_bound.
(* Goal: False *)
  apply Z.pow_pos_nonneg; omega.
Qed.    

Lemma pow2_nonneg: forall n,
    0 <= 2 ^ n.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. apply Z.pow_nonneg. omega.
Qed.

Lemma pow2_pos: forall n,
    0 <= n ->
    0 < 2 ^ n.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. apply Z.pow_pos_nonneg; omega.
Qed.

Lemma pow2_times2: forall i,
    0 < i ->
    2 ^ i = 2 * 2 ^ (i - 1).
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: False *)
  rewrite <- Z.pow_succ_r by omega.
(* Goal: @eq Z (Z.pow (Zpos (xO xH)) i) (Z.pow (Zpos (xO xH)) (Z.succ (Z.sub i (Zpos xH)))) *)
  f_equal.
(* Goal: False *)
  omega.
Qed.

Lemma pow2_div2: forall i,
    0 <= i ->
    2 ^ (i - 1) = 2 ^ i / 2.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: False *)
  assert (i = 0 \/ 0 < i) as C by omega. destruct C as [C | C].
  - subst. reflexivity.
(* Goal: False *)
  - rewrite Z.pow_sub_r by omega.
(* Goal: @eq Z b b *)
    reflexivity.
Qed.

Lemma div_mul_undo_le: forall a b,
    0 <= a ->
    0 < b ->
    a / b * b <= a.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: Z.le (Z.mul (Z.div a b) b) a *)
  pose proof (Zmod_eq_full a b) as P.
(* Goal: Z.le (Z.mul (Z.div a b) b) a *)
  pose proof (Z.mod_bound_pos a b) as Q.
(* Goal: False *)
  omega.
Qed.

Lemma testbit_true_nonneg: forall a i,
    0 <= a ->
    0 <= i ->
    Z.testbit a i = true ->
    2 ^ i <= a.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: Z.le (Z.pow (Zpos (xO xH)) i) a *)
  apply Z.testbit_true in H1; [|assumption].
(* Goal: Z.le (Z.pow (Zpos (xO xH)) i) a *)
  pose proof (pow2_pos i H0).
(* Goal: Z.le (Z.pow (Zpos (xO xH)) i) a *)
  eapply Z.le_trans; [| apply (div_mul_undo_le a (2 ^ i)); omega].
(* Goal: False *)
  replace (2 ^ i) with (1 * 2 ^ i) at 1 by omega.
(* Goal: Z.le (Z.mul (Zpos xH) (Z.pow (Zpos (xO xH)) i)) (Z.mul (Z.div a (Z.pow (Zpos (xO xH)) i)) (Z.pow (Zpos (xO xH)) i)) *)
  apply Z.mul_le_mono_nonneg_r; [omega|].
(* Goal: Z.le (Zpos xH) (Z.div a (Z.pow (Zpos (xO xH)) i)) *)
  pose proof (Z.div_pos a (2 ^ i)).
(* Goal: Z.le (Zpos xH) (Z.div a (Z.pow (Zpos (xO xH)) i)) *)
  assert (a / 2 ^ i <> 0); [|omega].
(* Goal: not (@eq Z (Z.div a (Z.pow (Zpos (xO xH)) i)) Z0) *)
  intro E. rewrite E in H1. cbv in H1. discriminate H1.
Qed.

Lemma range_div_pos: forall a b c d,
    0 < d ->
    a <= b <= c ->
    a / d <= b / d <= c / d.
Proof.
(* Goal: forall (a b c d : Z) (_ : Z.lt Z0 d) (_ : and (Z.le a b) (Z.le b c)), and (Z.le (Z.div a d) (Z.div b d)) (Z.le (Z.div b d) (Z.div c d)) *)
  intuition idtac.
  - apply (Z.div_le_mono _ _ _ H H1).
  - apply (Z.div_le_mono _ _ _ H H2).
Qed.

Lemma testbit_true_nonneg': forall a i,
    0 <= i ->
    2 ^ i <= a < 2 ^ (i + 1) ->
    Z.testbit a i = true.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: @eq bool (Z.testbit a i) true *)
  apply Z.testbit_true; [assumption|].
(* Goal: @eq Z (Z.modulo (Z.div a (Z.pow (Zpos (xO xH)) i)) (Zpos (xO xH))) (Zpos xH) *)
  destruct H0 as [A B].
(* Goal: @eq Z (Z.modulo (Z.div a (Z.pow (Zpos (xO xH)) i)) (Zpos (xO xH))) (Zpos xH) *)
  pose proof (pow2_pos i H) as Q.
(* Goal: @eq Z (Z.modulo (Z.div a (Z.pow (Zpos (xO xH)) i)) (Zpos (xO xH))) (Zpos xH) *)
  apply (Z.div_le_mono _ _ _ Q) in A.
(* Goal: False *)
  rewrite Z_div_same in A by omega.
(* Goal: @eq Z (Z.modulo (Z.div a (Z.pow (Zpos (xO xH)) i)) (Zpos (xO xH))) (Zpos xH) *)
  pose proof (Z.div_lt_upper_bound a (2 ^ i) 2 Q) as P.
(* Goal: @eq Z (Z.modulo (Z.div a (Z.pow (Zpos (xO xH)) i)) (Zpos (xO xH))) (Zpos xH) *)
  rewrite Z.mul_comm in P.
(* Goal: False *)
  replace i with (i + 1 - 1) in P by omega.
(* Goal: False *)
  rewrite <- pow2_times2 in P by omega.
(* Goal: @eq Z (Z.modulo (Z.div a (Z.pow (Zpos (xO xH)) i)) (Zpos (xO xH))) (Zpos xH) *)
  specialize (P B).
(* Goal: False *)
  replace (i + 1 - 1) with i in P by omega.
(* Goal: False *)
  replace (a / 2 ^ i) with 1 by omega.
(* Goal: @eq Z b b *)
  reflexivity.
Qed.  

Lemma testbit_false_nonneg: forall a i,
    0 <= a < 2 ^ i ->
    0 < i ->
    Z.testbit a (i - 1) = false ->
    a < 2 ^ (i - 1).
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: False *)
  assert (2 ^ (i - 1) <= a < 2 ^ i \/ a < 2 ^ (i - 1)) as C by omega.
(* Goal: Z.lt a (Z.pow (Zpos (xO xH)) (Z.sub i (Zpos xH))) *)
  destruct C as [C | C]; [exfalso|assumption].
  assert (Z.testbit a (i - 1) = true); [|congruence].
(* Goal: False *)
  replace i with (i - 1 + 1) in C at 2 by omega.
(* Goal: False *)
  apply testbit_true_nonneg'; omega.
Qed.  

Lemma signed_bounds_to_sz_pos: forall sz n,
    - 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) ->
    0 < sz.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: False *)
  assert (0 < sz \/ sz - 1 < 0) as C by omega.
(* Goal: Z.lt Z0 sz *)
  destruct C as [C | C]; [assumption|exfalso].
(* Goal: False *)
  rewrite Z.pow_neg_r in H by assumption.
(* Goal: False *)
  omega.
Qed.

Lemma two_digits_encoding_inj_lo: forall base a b c d: Z,
  0 <= b < base ->
  0 <= d < base ->
  base * a + b = base * c + d ->
  b = d.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros.
(* Goal: @eq Z b d *)
  pose proof Z.mod_unique as P.
(* Goal: @eq Z b d *)
  specialize P with (b := base) (q := c) (r := d).
(* Goal: @eq Z b d *)
  specialize P with (2 := H1).
(* Goal: False *)
  rewrite P by omega.
(* Goal: False *)
  rewrite <- Z.add_mod_idemp_l by omega.
(* Goal: @eq Z b (Z.modulo (Z.add (Z.modulo (Z.mul base a) base) b) base) *)
  rewrite Z.mul_comm.
(* Goal: False *)
  rewrite Z.mod_mul by omega.
(* Goal: @eq Z b (Z.modulo (Z.add Z0 b) base) *)
  rewrite Z.add_0_l.
(* Goal: False *)
  rewrite Z.mod_small by omega.
(* Goal: @eq Z b b *)
  reflexivity.
Qed.

Lemma two_digits_encoding_inj_hi: forall base a b c d: Z,
  0 <= b < base ->
  0 <= d < base ->
  base * a + b = base * c + d ->
  a = c.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. nia.
Qed.

Lemma Z_to_nat_neg: forall (n: Z),
    n < 0 ->
    Z.to_nat n = 0%nat.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq nat (Z.to_nat n) O *)
  intros. destruct n; try lia. apply Z2Nat.inj_neg.
Qed.
