Require Import Coq.Arith.Div2.
Require Import Coq.micromega.Lia.
Require Import Coq.NArith.NArith.
Require Import Coq.ZArith.ZArith.
Require Import bbv.N_Z_nat_conversions.
Require Export bbv.Nomega.

Set Implicit Arguments.

Fixpoint mod2 (n : nat) : bool :=
  match n with
    | 0 => false
    | 1 => true
    | S (S n') => mod2 n'
  end.

Ltac rethink :=
  match goal with
    | [ H : ?f ?n = _ |- ?f ?m = _ ] => replace m with n; simpl; auto
  end.

Theorem mod2_S_double : forall n, mod2 (S (2 * n)) = true.
(* Goal: forall n : nat, @eq bool (mod2 (S (Init.Nat.mul (S (S O)) n))) true *)
  induction n; simpl; intuition; rethink.
Qed.

Theorem mod2_double : forall n, mod2 (2 * n) = false.
(* Goal: forall n : nat, @eq bool (mod2 (Init.Nat.mul (S (S O)) n)) false *)
  induction n; simpl; intuition; rewrite <- plus_n_Sm; rethink.
Qed.

Theorem div2_double : forall n, div2 (2 * n) = n.
(* Goal: forall n : nat, @eq nat (Nat.div2 (Init.Nat.mul (S (S O)) n)) n *)
  induction n; simpl; intuition; rewrite <- plus_n_Sm; f_equal; rethink.
Qed.

Theorem div2_S_double : forall n, div2 (S (2 * n)) = n.
(* Goal: forall n : nat, @eq nat (Nat.div2 (S (Init.Nat.mul (S (S O)) n))) n *)
  induction n; simpl; intuition; f_equal; rethink.
Qed.

Notation pow2 := (Nat.pow 2).

Fixpoint Npow2 (n : nat) : N :=
  match n with
    | O => 1
    | S n' => 2 * Npow2 n'
  end%N.

Theorem untimes2 : forall n, n + (n + 0) = 2 * n.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  auto.
Qed.

Section strong.
  Variable P : nat -> Prop.

  Hypothesis PH : forall n, (forall m, m < n -> P m) -> P n.

  Lemma strong' : forall n m, m <= n -> P m.
(* Goal: forall (n m : nat) (_ : le m n), P m *)
    induction n; simpl; intuition; apply PH; intuition.
(* Goal: P m0 *)
    elimtype False; omega.
  Qed.

  Theorem strong : forall n, P n.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
    intros; eapply strong'; eauto.
  Qed.
End strong.

Theorem div2_odd : forall n,
  mod2 n = true
  -> n = S (2 * div2 n).
(* Goal: forall (n : nat) (_ : @eq bool (mod2 n) false), @eq nat n (Init.Nat.mul (S (S O)) (Nat.div2 n)) *)
  induction n as [n] using strong; simpl; intuition.

(* Goal: @eq nat (S n) (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end O)) *)
  destruct n as [|n]; simpl in *; intuition.
(* Goal: @eq nat (Nat.modulo k (S (S O))) O *)
    discriminate.
(* Goal: @eq nat (S n) (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end O)) *)
  destruct n as [|n]; simpl in *; intuition.
(* Goal: @eq nat (S (S n)) (S (S (Init.Nat.add (Nat.div2 n) (S (Init.Nat.add (Nat.div2 n) O))))) *)
  do 2 f_equal.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  replace (div2 n + S (div2 n + 0)) with (S (div2 n + (div2 n + 0))); auto.
Qed.

Theorem div2_even : forall n,
  mod2 n = false
  -> n = 2 * div2 n.
(* Goal: forall (n : nat) (_ : @eq bool (mod2 n) false), @eq nat n (Init.Nat.mul (S (S O)) (Nat.div2 n)) *)
  induction n as [n] using strong; simpl; intuition.

(* Goal: @eq nat (S n) (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end O)) *)
  destruct n as [|n]; simpl in *; intuition.
(* Goal: @eq nat (S n) (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end (Init.Nat.add match n with | O => O | S n' => S (Nat.div2 n') end O)) *)
  destruct n as [|n]; simpl in *; intuition.
(* Goal: @eq nat (Nat.modulo k (S (S O))) O *)
    discriminate.
(* Goal: @eq nat (S (S n)) (S (Init.Nat.add (Nat.div2 n) (S (Init.Nat.add (Nat.div2 n) O)))) *)
  f_equal.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  replace (div2 n + S (div2 n + 0)) with (S (div2 n + (div2 n + 0))); auto.
Qed.

Theorem drop_mod2 : forall n k,
  2 * k <= n
  -> mod2 (n - 2 * k) = mod2 n.
(* Goal: forall (n k : nat) (_ : le (Init.Nat.mul (S (S O)) k) n), @eq nat (Nat.div2 (Init.Nat.sub n (Init.Nat.mul (S (S O)) k))) (Init.Nat.sub (Nat.div2 n) k) *)
  induction n as [n] using strong; intros.

(* Goal: @eq bool (mod2 (Init.Nat.sub n (Init.Nat.mul (S (S O)) k))) (mod2 n) *)
  do 2 (destruct n; simpl in *; repeat rewrite untimes2 in *; intuition).

(* Goal: @eq nat (Nat.div2 match Init.Nat.mul (S (S O)) k with | O => S (S n) | S (O as l) => S n | S (S l0 as l) => Init.Nat.sub n l0 end) match k with | O => S (Nat.div2 n) | S l => Init.Nat.sub (Nat.div2 n) l end *)
  destruct k; simpl in *; intuition.

(* Goal: @eq bool (mod2 match Init.Nat.mul (S (S O)) k with | O => S (S n) | S (O as l) => S n | S (S l0 as l) => Init.Nat.sub n l0 end) (mod2 n) *)
  destruct k; simpl; intuition.
(* Goal: @eq nat (Nat.div2 match Init.Nat.add k (S (Init.Nat.add k O)) with | O => S n | S l => Init.Nat.sub n l end) (Init.Nat.sub (Nat.div2 n) k) *)
  rewrite <- plus_n_Sm.
(* Goal: @eq bool (mod2 (Init.Nat.sub n (Init.Nat.add k (Init.Nat.add k O)))) (mod2 n) *)
  repeat rewrite untimes2 in *.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  simpl; auto.
(* Goal: @eq nat (Nat.div2 (Init.Nat.sub n (Init.Nat.add k (Init.Nat.add k O)))) (Init.Nat.sub (Nat.div2 n) k) *)
  apply H; omega.
Qed.

Theorem div2_minus_2 : forall n k,
  2 * k <= n
  -> div2 (n - 2 * k) = div2 n - k.
(* Goal: forall (n k : nat) (_ : le (Init.Nat.mul (S (S O)) k) n), @eq nat (Nat.div2 (Init.Nat.sub n (Init.Nat.mul (S (S O)) k))) (Init.Nat.sub (Nat.div2 n) k) *)
  induction n as [n] using strong; intros.

(* Goal: @eq nat (Nat.div2 (Init.Nat.sub n (Init.Nat.mul (S (S O)) k))) (Init.Nat.sub (Nat.div2 n) k) *)
  do 2 (destruct n; simpl in *; intuition; repeat rewrite untimes2 in *).
(* Goal: @eq nat (Nat.div2 match Init.Nat.mul (S (S O)) k with | O => S (S n) | S (O as l) => S n | S (S l0 as l) => Init.Nat.sub n l0 end) match k with | O => S (Nat.div2 n) | S l => Init.Nat.sub (Nat.div2 n) l end *)
  destruct k; simpl in *; intuition.

(* Goal: @eq nat (Nat.div2 match Init.Nat.mul (S (S O)) k with | O => S (S n) | S (O as l) => S n | S (S l0 as l) => Init.Nat.sub n l0 end) match k with | O => S (Nat.div2 n) | S l => Init.Nat.sub (Nat.div2 n) l end *)
  destruct k; simpl in *; intuition.
(* Goal: @eq nat (Nat.div2 match Init.Nat.add k (S (Init.Nat.add k O)) with | O => S n | S l => Init.Nat.sub n l end) (Init.Nat.sub (Nat.div2 n) k) *)
  rewrite <- plus_n_Sm.
(* Goal: @eq nat (Nat.div2 (Init.Nat.sub n (Init.Nat.add k (Init.Nat.add k O)))) (Init.Nat.sub (Nat.div2 n) k) *)
  apply H; omega.
Qed.

Theorem div2_bound : forall k n,
  2 * k <= n
  -> k <= div2 n.
(* Goal: forall (k n : nat) (_ : le (Init.Nat.mul (S (S O)) k) n), le k (Nat.div2 n) *)
  intros ? n H; case_eq (mod2 n); intro Heq.

(* Goal: le k (Nat.div2 n) *)
(* Goal: le k (Nat.div2 n) *)
  rewrite (div2_odd _ Heq) in H.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.

(* Goal: le k (Nat.div2 n) *)
  rewrite (div2_even _ Heq) in H.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.
Qed.

Lemma two_times_div2_bound: forall n, 2 * Nat.div2 n <= n.
Proof.
(* Goal: forall n : nat, le (Init.Nat.mul (S (S O)) (Nat.div2 n)) n *)
  eapply strong. intros n IH.
(* Goal: le (Init.Nat.mul (S (S O)) (Nat.div2 (S n))) (S n) *)
  destruct n.
  - constructor.
(* Goal: le (Init.Nat.mul (S (S O)) (Nat.div2 (S n))) (S n) *)
  - destruct n.
(* Goal: N.lt N0 (Npos p) *)
    + simpl. constructor. constructor.
    + simpl (Nat.div2 (S (S n))).
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
      specialize (IH n). omega.
Qed.

Lemma div2_compat_lt_l: forall a b, b < 2 * a -> Nat.div2 b < a.
Proof.
(* Goal: forall (a b : nat) (_ : lt b (Init.Nat.mul (S (S O)) a)), lt (Nat.div2 b) a *)
  induction a; intros.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  - omega.
  - destruct b.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
    + simpl. omega.
    + destruct b.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
      * simpl. omega.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
      * simpl. apply lt_n_S. apply IHa. omega.
Qed.

(* otherwise b is made implicit, while a isn't, which is weird *)
Arguments div2_compat_lt_l {_} {_} _.

Lemma pow2_add_mul: forall a b,
  pow2 (a + b) = (pow2 a) * (pow2 b).
Proof.
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
  induction a; destruct b; firstorder; simpl.
(* Goal: le (Init.Nat.add (Nat.add (Nat.pow (S (S O)) sz) (Nat.add (Nat.pow (S (S O)) sz) O)) (S O)) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) O)) *)
  repeat rewrite Nat.add_0_r.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  rewrite Nat.mul_1_r; auto.
(* Goal: le (Init.Nat.add (Nat.add (Nat.pow (S (S O)) sz) (Nat.add (Nat.pow (S (S O)) sz) O)) (S O)) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) O)) *)
  repeat rewrite Nat.add_0_r.
(* Goal: @eq nat (Nat.add (Nat.pow (S (S O)) (Init.Nat.add a (S b))) (Nat.pow (S (S O)) (Init.Nat.add a (S b)))) (Init.Nat.mul (Nat.add (Nat.pow (S (S O)) a) (Nat.pow (S (S O)) a)) (Nat.add (Nat.pow (S (S O)) b) (Nat.pow (S (S O)) b))) *)
  rewrite IHa.
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
  simpl.
(* Goal: le (Init.Nat.add (Nat.add (Nat.pow (S (S O)) sz) (Nat.add (Nat.pow (S (S O)) sz) O)) (S O)) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) O)) *)
  repeat rewrite Nat.add_0_r.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  rewrite Nat.mul_add_distr_r; auto.
Qed.

Lemma mult_pow2_bound: forall a b x y,
  x < pow2 a -> y < pow2 b -> x * y < pow2 (a + b).
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: le (Nat.pow (S (S O)) n) (Nat.pow (S (S O)) (Init.Nat.add n x)) *)
  rewrite pow2_add_mul.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  apply Nat.mul_lt_mono_nonneg; omega.
Qed.

Lemma mult_pow2_bound_ex: forall a c x y,
  x < pow2 a -> y < pow2 (c - a) -> c >= a -> x * y < pow2 c.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace c with (a + (c - a)) by omega.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  apply mult_pow2_bound; auto.
Qed.

Lemma lt_mul_mono' : forall c a b,
  a < b -> a < b * (S c).
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  induction c; intros.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  rewrite Nat.mul_1_r; auto.
(* Goal: lt a (Init.Nat.mul b (S (S c))) *)
  rewrite Nat.mul_succ_r.
(* Goal: lt a (Nat.add (Nat.mul b (S c)) b) *)
  apply lt_plus_trans.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  apply IHc; auto.
Qed.

Lemma lt_mul_mono : forall a b c,
  c <> 0 -> a < b -> a < b * c.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace c with (S (c - 1)) by omega.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  apply lt_mul_mono'; auto.
Qed.

Lemma zero_lt_pow2 : forall sz, 0 < pow2 sz.
Proof.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  induction sz; simpl; omega.
Qed.

Lemma one_lt_pow2:
  forall n,
    1 < pow2 (S n).
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: forall n : nat, or (@ex nat (fun a : nat => @eq nat n (Init.Nat.mul (S (S O)) a))) (@ex nat (fun a : nat => @eq nat n (Init.Nat.add (Init.Nat.mul (S (S O)) a) (S O)))) *)
  induction n.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  simpl; omega.
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
  remember (S n); simpl.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.
Qed.

Lemma one_le_pow2 : forall sz, 1 <= pow2 sz.
Proof.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  intros. pose proof (zero_lt_pow2 sz). omega.
Qed.

Lemma pow2_ne_zero: forall n, pow2 n <> 0.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: not (@eq nat (Nat.pow (S (S O)) n) O) *)
  pose proof (zero_lt_pow2 n).
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.
Qed.

Lemma mul2_add : forall n, n * 2 = n + n.
Proof.
(* Goal: forall n : nat, @eq nat (Init.Nat.mul n (S (S O))) (Init.Nat.add n n) *)
  induction n; firstorder.
Qed.

Lemma pow2_le_S : forall sz, (pow2 sz) + 1 <= pow2 (sz + 1).
Proof.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  induction sz; simpl; auto.
(* Goal: le (Init.Nat.add (Nat.add (Nat.pow (S (S O)) sz) (Nat.add (Nat.pow (S (S O)) sz) O)) (S O)) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) (Nat.add (Nat.pow (S (S O)) (Init.Nat.add sz (S O))) O)) *)
  repeat rewrite Nat.add_0_r.
(* Goal: le (Nat.pow (S (S O)) n) (Nat.pow (S (S O)) (Init.Nat.add n x)) *)
  rewrite pow2_add_mul.
(* Goal: le (Init.Nat.add (Nat.add (Nat.pow (S (S O)) sz) (Nat.pow (S (S O)) sz)) (S O)) (Nat.add (Init.Nat.mul (Nat.pow (S (S O)) sz) (Nat.pow (S (S O)) (S O))) (Init.Nat.mul (Nat.pow (S (S O)) sz) (Nat.pow (S (S O)) (S O)))) *)
  repeat rewrite mul2_add.
(* Goal: le (Init.Nat.add (Nat.add (Nat.pow (S (S O)) sz) (Nat.pow (S (S O)) sz)) (S O)) (Nat.add (Init.Nat.add (Nat.pow (S (S O)) sz) (Nat.pow (S (S O)) sz)) (Init.Nat.add (Nat.pow (S (S O)) sz) (Nat.pow (S (S O)) sz))) *)
  pose proof (zero_lt_pow2 sz).
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.
Qed.

Lemma pow2_bound_mono: forall a b x,
  x < pow2 a -> a <= b -> x < pow2 b.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace b with (a + (b - a)) by omega.
(* Goal: le (Nat.pow (S (S O)) n) (Nat.pow (S (S O)) (Init.Nat.add n x)) *)
  rewrite pow2_add_mul.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  apply lt_mul_mono; auto.
  pose proof (zero_lt_pow2 (b - a)).
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.
Qed.

Lemma pow2_inc : forall n m,
  0 < n -> n < m ->
    pow2 n < pow2 m.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  generalize dependent n; intros.
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
  induction m; simpl.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros. inversion H0.
(* Goal: lt (Nat.pow (S (S O)) n) (Nat.add (Nat.pow (S (S O)) m) (Nat.add (Nat.pow (S (S O)) m) O)) *)
  unfold lt in H0.
(* Goal: @eq nat (Nat.modulo (Nat.add a O) b) (Nat.modulo a b) *)
  rewrite Nat.add_0_r.
(* Goal: lt (Nat.pow (S (S O)) n) (Nat.add (Nat.pow (S (S O)) m) (Nat.pow (S (S O)) m)) *)
  inversion H0.
(* Goal: lt (Nat.pow (S (S O)) m) (Nat.add (Nat.pow (S (S O)) m) (Nat.pow (S (S O)) m)) *)
  apply Nat.lt_add_pos_r.
(* Goal: lt O (Nat.pow (S (S O)) m) *)
  apply zero_lt_pow2.
(* Goal: lt (Nat.pow (S (S O)) n) (Nat.add (Nat.pow (S (S O)) m) (Nat.pow (S (S O)) m)) *)
  apply Nat.lt_trans with (pow2 m).
(* Goal: lt (Nat.pow (S (S O)) n) (Nat.pow (S (S O)) m) *)
(* Goal: lt (Nat.pow (S (S O)) m) (Nat.add (Nat.pow (S (S O)) m) (Nat.pow (S (S O)) m)) *)
  apply IHm.
(* Goal: lt n m *)
(* Goal: lt (Nat.pow (S (S O)) m) (Nat.add (Nat.pow (S (S O)) m) (Nat.pow (S (S O)) m)) *)
  exact H2.
(* Goal: lt (Nat.pow (S (S O)) m) (Nat.add (Nat.pow (S (S O)) m) (Nat.pow (S (S O)) m)) *)
  apply Nat.lt_add_pos_r.
(* Goal: lt O (Nat.pow (S (S O)) m) *)
  apply zero_lt_pow2.
Qed.

Lemma pow2_S: forall x, pow2 (S x) = 2 * pow2 x.
Proof. intros. reflexivity. Qed.

Lemma mod2_S_S : forall n,
  mod2 (S (S n)) = mod2 n.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  destruct n; auto; destruct n; auto.
Qed.

Lemma mod2_S_not : forall n,
  mod2 (S n) = if (mod2 n) then false else true.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  induction n; auto.
(* Goal: @eq bool (mod2 (S (S n))) (if mod2 (S n) then false else true) *)
  rewrite mod2_S_S.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  destruct (mod2 n); replace (mod2 (S n)); auto.
Qed.

Lemma mod2_S_eq : forall n k,
  mod2 n = mod2 k ->
  mod2 (S n) = mod2 (S k).
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: @eq bool (mod2 (S n)) (mod2 (S k)) *)
  do 2 rewrite mod2_S_not.
(* Goal: @eq Z (Z.modulo (Z.sub (Z.of_nat (Nat.modulo a m)) (Z.of_nat (Nat.modulo b m))) (Z.of_nat m)) Z0 *)
  rewrite H.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  auto.
Qed.

Theorem drop_mod2_add : forall n k,
  mod2 (n + 2 * k) = mod2 n.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: forall n : nat, or (@ex nat (fun a : nat => @eq nat n (Init.Nat.mul (S (S O)) a))) (@ex nat (fun a : nat => @eq nat n (Init.Nat.add (Init.Nat.mul (S (S O)) a) (S O)))) *)
  induction n.
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
  simpl.
(* Goal: @eq nat (Nat.modulo (Nat.add a O) b) (Nat.modulo a b) *)
  rewrite Nat.add_0_r.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace (k + k) with (2 * k) by omega.
(* Goal: @eq bool (mod2 (Init.Nat.mul (S (S O)) (Nat.pow (S (S O)) n))) false *)
  apply mod2_double.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace (S n + 2 * k) with (S (n + 2 * k)) by omega.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  apply mod2_S_eq; auto.
Qed.

Lemma mod2sub: forall a b,
  b <= a ->
  mod2 (a - b) = xorb (mod2 a) (mod2 b).
Proof.
  intros. remember (a - b) as c. revert dependent b. revert a. revert c.
  change (forall c,
    (fun c => forall a b, b <= a -> c = a - b -> mod2 c = xorb (mod2 a) (mod2 b)) c).
(* Goal: forall c : nat, (fun c0 : nat => forall (a b : nat) (_ : le b a) (_ : @eq nat c0 (Init.Nat.sub a b)), @eq bool (mod2 c0) (xorb (mod2 a) (mod2 b))) c *)
  apply strong.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n) (a b : nat) (_ : le b a) (_ : @eq nat m (Init.Nat.sub a b)), @eq bool (mod2 m) (xorb (mod2 a) (mod2 b))) (a b : nat) (_ : le b a) (_ : @eq nat n (Init.Nat.sub a b)), @eq bool (mod2 n) (xorb (mod2 a) (mod2 b)) *)
  intros c IH a b AB N.
(* Goal: @eq bool (mod2 (S c)) (xorb (mod2 a) (mod2 b)) *)
  destruct c.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  - assert (a=b) by omega. subst. rewrite Bool.xorb_nilpotent. reflexivity.
  - destruct c.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
    + assert (a = S b) by omega. subst a. simpl (mod2 1). rewrite mod2_S_not.
(* Goal: @eq nat (Nat.modulo m O) O *)
      destruct (mod2 b); reflexivity.
    + destruct a; [omega|].
(* Goal: @eq bool (mod2 (S (S c))) (xorb (mod2 (S a)) (mod2 b)) *)
      destruct a; [omega|].
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
      simpl.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
      apply IH; omega.
Qed.

Theorem mod2_pow2_twice: forall n,
  mod2 (pow2 n + (pow2 n + 0)) = false.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace (pow2 n + (pow2 n + 0)) with (2 * pow2 n) by omega.
(* Goal: @eq bool (mod2 (Init.Nat.mul (S (S O)) (Nat.pow (S (S O)) n))) false *)
  apply mod2_double.
Qed.

Theorem div2_plus_2 : forall n k,
  div2 (n + 2 * k) = div2 n + k.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  induction n; intros.
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
  simpl.
(* Goal: @eq nat (Nat.modulo (Nat.add a O) b) (Nat.modulo a b) *)
  rewrite Nat.add_0_r.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace (k + k) with (2 * k) by omega.
(* Goal: @eq nat (Nat.div2 (Init.Nat.mul (S (S O)) k)) k *)
(* Goal: @eq nat (Nat.div2 (Init.Nat.add (S n) (Init.Nat.mul (S (S O)) k))) (Init.Nat.add (Nat.div2 (S n)) k) *)
  apply div2_double.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace (S n + 2 * k) with (S (n + 2 * k)) by omega.
(* Goal: @eq nat (Nat.div2 (S (Init.Nat.add n (Init.Nat.mul (S (S O)) k)))) (Init.Nat.add (Nat.div2 (S n)) k) *)
  destruct (Even.even_or_odd n).
  - rewrite <- even_div2.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
    rewrite <- even_div2 by auto.
(* Goal: @eq nat (Nat.div2 (Init.Nat.add n (Init.Nat.mul (S (S O)) k))) (Init.Nat.add (Nat.div2 n) k) *)
(* Goal: Even.even (Init.Nat.add n (Init.Nat.mul (S (S O)) k)) *)
    apply IHn.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
    apply Even.even_even_plus; auto.
(* Goal: N.lt N0 (Npos p) *)
    apply Even.even_mult_l; repeat constructor.

  - rewrite <- odd_div2.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
    rewrite <- odd_div2 by auto.
(* Goal: @eq nat (S (Nat.div2 (Init.Nat.add n (Init.Nat.mul (S (S O)) k)))) (Init.Nat.add (S (Nat.div2 n)) k) *)
(* Goal: Even.odd (Init.Nat.add n (Init.Nat.mul (S (S O)) k)) *)
    rewrite IHn.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
    omega.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
    apply Even.odd_plus_l; auto.
(* Goal: N.lt N0 (Npos p) *)
    apply Even.even_mult_l; repeat constructor.
Qed.

Lemma pred_add:
  forall n, n <> 0 -> pred n + 1 = n.
Proof.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  intros; rewrite pred_of_minus; omega.
Qed.

Lemma pow2_zero: forall sz, (pow2 sz > 0)%nat.
Proof.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  induction sz; simpl; auto; omega.
Qed.

Section omega_compat.

Ltac omega ::= lia.

Theorem Npow2_nat : forall n, nat_of_N (Npow2 n) = pow2 n.
(* Goal: forall n : nat, @eq nat (N.to_nat (Npow2 n)) (Nat.pow (S (S O)) n) *)
  induction n as [|n IHn]; simpl; intuition.
  rewrite <- IHn; clear IHn.
(* Goal: @eq nat (N.to_nat match Npow2 n with | N0 => N0 | Npos q => Npos (xO q) end) (Nat.add (N.to_nat (Npow2 n)) (Nat.add (N.to_nat (Npow2 n)) O)) *)
  case_eq (Npow2 n); intuition.
Qed.

End omega_compat.

Theorem pow2_N : forall n, Npow2 n = N.of_nat (pow2 n).
Proof.
(* Goal: forall n : nat, @eq N (Npow2 n) (N.of_nat (Nat.pow (S (S O)) n)) *)
  intro n. apply nat_of_N_eq. rewrite Nat2N.id. apply Npow2_nat.
Qed.

Lemma Z_of_N_Npow2: forall n, Z.of_N (Npow2 n) = (2 ^ Z.of_nat n)%Z.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: @eq Z (Z.of_N (Npow2 n)) (Z.pow (Zpos (xO xH)) (Z.of_nat n)) *)
  rewrite pow2_N.
(* Goal: @eq Z (Z.of_N (N.of_nat (Nat.pow (S (S O)) n))) (Z.pow (Zpos (xO xH)) (Z.of_nat n)) *)
  rewrite nat_N_Z.
(* Goal: @eq Z (Z.of_nat (Nat.pow (S (S O)) n)) (Z.pow (Zpos (xO xH)) (Z.of_nat n)) *)
  rewrite Nat2Z.inj_pow.
(* Goal: @eq nat (Nat.modulo m O) O *)
  reflexivity.
Qed.

Lemma pow2_S_z:
  forall n, Z.of_nat (pow2 (S n)) = (2 * Z.of_nat (pow2 n))%Z.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
  replace (2 * Z.of_nat (pow2 n))%Z with
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
      (Z.of_nat (pow2 n) + Z.of_nat (pow2 n))%Z by omega.
(* Goal: @eq Z (Z.of_nat (Nat.modulo (Init.Nat.sub a b) m)) (Z.of_nat O) *)
  simpl.
(* Goal: @eq Z (Z.of_nat (Nat.add (Nat.pow (S (S O)) n) (Nat.add (Nat.pow (S (S O)) n) O))) (Z.add (Z.of_nat (Nat.pow (S (S O)) n)) (Z.of_nat (Nat.pow (S (S O)) n))) *)
  repeat rewrite Nat2Z.inj_add.
(* Goal: @eq Z (Z.add (Z.of_nat (Nat.pow (S (S O)) n)) (Z.add (Z.of_nat (Nat.pow (S (S O)) n)) (Z.of_nat O))) (Z.add (Z.of_nat (Nat.pow (S (S O)) n)) (Z.of_nat (Nat.pow (S (S O)) n))) *)
  ring.
Qed.

Lemma pow2_le:
  forall n m, (n <= m)%nat -> (pow2 n <= pow2 m)%nat.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
  assert (exists s, n + s = m) by (exists (m - n); omega).
(* Goal: @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  destruct H0; subst.
(* Goal: le (Nat.pow (S (S O)) n) (Nat.pow (S (S O)) (Init.Nat.add n x)) *)
  rewrite pow2_add_mul.
(* Goal: le (Nat.pow (S (S O)) n) (Init.Nat.mul (Nat.pow (S (S O)) n) (Nat.pow (S (S O)) x)) *)
  pose proof (pow2_zero x).
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace (pow2 n) with (pow2 n * 1) at 1 by omega.
(* Goal: le (Init.Nat.mul (Nat.pow (S (S O)) n) (S O)) (Init.Nat.mul (Nat.pow (S (S O)) n) (Nat.pow (S (S O)) x)) *)
  apply mult_le_compat_l.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.
Qed.

Lemma Zabs_of_nat:
  forall n, Z.abs (Z.of_nat n) = Z.of_nat n.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  unfold Z.of_nat; intros.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  destruct n; auto.
Qed.

Lemma Npow2_not_zero:
  forall n, Npow2 n <> 0%N.
Proof.
(* Goal: forall n : nat, not (@eq N (Npow2 n) N0) *)
  induction n; simpl; intros; [discriminate|].
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  destruct (Npow2 n); auto.
(* Goal: @eq nat (Nat.modulo k (S (S O))) O *)
  discriminate.
Qed.

Lemma Npow2_S:
  forall n, Npow2 (S n) = (Npow2 n + Npow2 n)%N.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  simpl; intros.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  destruct (Npow2 n); auto.
  rewrite <-Pos.add_diag.
(* Goal: @eq nat (Nat.modulo m O) O *)
  reflexivity.
Qed.

Lemma Npow2_pos: forall a,
    (0 < Npow2 a)%N.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: N.lt N0 (Npow2 a) *)
  destruct (Npow2 a) eqn: E.
  - exfalso. apply (Npow2_not_zero a). assumption.
  - constructor.
Qed.

Lemma minus_minus: forall a b c,
  c <= b <= a ->
  a - (b - c) = a - b + c.
Proof. intros. omega. Qed.

Lemma even_odd_destruct: forall n,
  (exists a, n = 2 * a) \/ (exists a, n = 2 * a + 1).
Proof.
(* Goal: forall n : nat, or (@ex nat (fun a : nat => @eq nat n (Init.Nat.mul (S (S O)) a))) (@ex nat (fun a : nat => @eq nat n (Init.Nat.add (Init.Nat.mul (S (S O)) a) (S O)))) *)
  induction n.
  - left. exists 0. reflexivity.
  - destruct IHn as [[a E] | [a E]].
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
    + right. exists a. omega.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
    + left. exists (S a). omega.
Qed.

Lemma mul_div_undo: forall i c,
    c <> 0 ->
    c * i / c = i.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: @eq nat (Nat.div (Init.Nat.mul c i) c) i *)
  pose proof (Nat.div_mul_cancel_l i 1 c) as P.
(* Goal: @eq nat (Nat.div (Init.Nat.mul c i) c) i *)
  rewrite Nat.div_1_r in P.
(* Goal: @eq nat (Nat.div (Init.Nat.mul c i) c) i *)
  rewrite Nat.mul_1_r in P.
(* Goal: @eq bool (if mod2 k then false else true) (if mod2 k then false else true) *)
  apply P; auto.
Qed.

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

Lemma mod2_cases: forall (n: nat), n mod 2 = 0 \/ n mod 2 = 1.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: or (@eq nat (Nat.modulo n (S (S O))) O) (@eq nat (Nat.modulo n (S (S O))) (S O)) *)
  assert (n mod 2 < 2). {
(* Goal: lt (Nat.modulo n (S (S O))) (S (S O)) *)
    apply Nat.mod_upper_bound. congruence.
  }
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  omega.
Qed.

Lemma div_mul_undo: forall a b,
    b <> 0 ->
    a mod b = 0 ->
    a / b * b = a.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros.
(* Goal: @eq nat (Init.Nat.mul (Nat.div a b) b) a *)
  pose proof Nat.div_mul_cancel_l as A. specialize (A a 1 b).
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  replace (b * 1) with b in A by omega.
(* Goal: @eq nat (Init.Nat.mul (Nat.div a b) b) a *)
  rewrite Nat.div_1_r in A.
(* Goal: @eq nat (Init.Nat.mul (Nat.div a b) b) a *)
  rewrite mult_comm.
  rewrite <- Nat.divide_div_mul_exact; try assumption.
  - apply A; congruence.
  - apply Nat.mod_divide; assumption.
Qed.

Lemma Smod2_1: forall k, S k mod 2 = 1 -> k mod 2 = 0.
Proof.
(* Goal: forall (k : nat) (_ : @eq nat (Nat.modulo (S k) (S (S O))) (S O)), @eq nat (Nat.modulo k (S (S O))) O *)
  intros k C.
  change (S k) with (1 + k) in C.
(* Goal: not (@eq nat (S (S O)) O) *)
  rewrite Nat.add_mod in C by congruence.
(* Goal: @eq nat (Nat.modulo k (S (S O))) O *)
  pose proof (Nat.mod_upper_bound k 2).
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  assert (k mod 2 = 0 \/ k mod 2 = 1) as E by omega.
(* Goal: @eq nat (Nat.modulo k (S (S O))) O *)
  destruct E as [E | E]; [assumption|].
(* Goal: @eq nat (Nat.modulo k (S (S O))) O *)
  rewrite E in C. simpl in C. discriminate.
Qed.

Lemma mod_0_r: forall (m: nat),
    m mod 0 = 0.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros. reflexivity.
Qed.

Lemma sub_mod_0: forall (a b m: nat),
    a mod m = 0 ->
    b mod m = 0 ->
    (a - b) mod m = 0.
Proof.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  intros. assert (m = 0 \/ m <> 0) as C by omega. destruct C as [C | C].
  - subst. apply mod_0_r.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
  - assert (a - b = 0 \/ b < a) as D by omega. destruct D as [D | D].
    + rewrite D. apply Nat.mod_0_l. assumption.
    + apply Nat2Z.inj. simpl.
(* Goal: not (@eq nat m O) *)
      rewrite Zdiv.mod_Zmod by assumption.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
      rewrite Nat2Z.inj_sub by omega.
(* Goal: @eq Z (Z.modulo (Z.sub (Z.of_nat a) (Z.of_nat b)) (Z.of_nat m)) Z0 *)
      rewrite Zdiv.Zminus_mod.
      rewrite <-! Zdiv.mod_Zmod by assumption.
(* Goal: @eq Z (Z.modulo (Z.sub (Z.of_nat (Nat.modulo a m)) (Z.of_nat (Nat.modulo b m))) (Z.of_nat m)) Z0 *)
      rewrite H. rewrite H0.
(* Goal: @eq Z (Z.modulo (Z.sub (Z.of_nat O) (Z.of_nat O)) (Z.of_nat m)) Z0 *)
      apply Z.mod_0_l.
(* Goal: not (@eq Z (Z.of_nat m) Z0) *)
      omega.
Qed.

Lemma mul_div_exact: forall (a b: nat),
    b <> 0 ->
    a mod b = 0 ->
    b * (a / b) = a.
Proof.
(* Goal: forall (a b m : nat) (_ : @eq nat (Nat.modulo a m) O) (_ : @eq nat (Nat.modulo b m) O), @eq nat (Nat.modulo (Init.Nat.sub a b) m) O *)
  intros. edestruct Nat.div_exact as [_ P]; [eassumption|].
  specialize (P H0). symmetry. exact P.
Qed.
