Require Import Bool.
Require Import Arith.
Require Import ZArith.
Require Import String.
Require Import Vbase.

Set Implicit Arguments.

Fixpoint eqn_rec (x y: nat) {struct x} :=
   match x, y with
     | O, O => true
     | S x, S y => eqn_rec x y
     | _, _ => false
   end.

Definition eqn := match tt with tt => eqn_rec end.

Lemma eqnP: forall x y, reflect (x = y) (eqn x y).

Canonical Structure nat_eqMixin := EqMixin eqnP.
Canonical Structure nat_eqType := Eval hnf in EqType nat nat_eqMixin.

Lemma eqnE : eqn = (@eq_op _).

Inductive bool3 := B3tt | B3ff | B3un.

Definition bool3_beq (x y : bool3) :=
  match x, y with
    | B3tt, B3tt => true
    | B3ff, B3ff => true
    | B3un, B3un => true
    | _, _ => false
  end.

Lemma bool3P : forall x y, reflect (x = y) (bool3_beq x y).

Definition negb3 (b:bool3) : bool3 :=
  match b with
   | B3tt => B3ff
   | B3ff => B3tt
   | B3un => B3un
  end.

Definition andb3 (b1 b2:bool3) : bool3 :=
  match b1, b2 with
    | B3tt, _ => b2
    | B3ff, _ => B3ff
    | B3un, B3ff => B3ff
    | B3un, _ => B3un
  end.

Definition orb3 (b1 b2:bool3) : bool3 :=
  match b1, b2 with
    | B3tt, _ => B3tt
    | B3ff, _ => b2
    | B3un, B3tt => B3tt
    | B3un, _ => B3un
  end.

Definition bool2bool3 (b: bool) : bool3 :=
  if b then B3tt else B3ff.

Definition b3_moredef (b1 : bool3) (b2: bool) : bool :=
  match b1 with
    | B3tt => b2
    | B3ff => negb b2
    | B3un => false
  end.

Lemma andb3T: forall b, andb3 b B3tt = b.
Lemma andb3F: forall b, andb3 b B3ff = B3ff.
Lemma orb3T: forall b, orb3 b B3tt = B3tt.
Lemma orb3F: forall b, orb3 b B3ff = b.

Lemma negb3P: forall x, bool2bool3 (negb x) = negb3 (bool2bool3 x).

Lemma andb3P: forall x y, bool2bool3 (andb x y) = andb3 (bool2bool3 x) (bool2bool3 y).

Lemma orb3P: forall x y, bool2bool3 (orb x y) = orb3 (bool2bool3 x) (bool2bool3 y).

Lemma negb3_neg : forall x, negb3 (negb3 x) = x.

Lemma negb3_and : forall b1 b2, negb3 (andb3 b1 b2) = orb3 (negb3 b1) (negb3 b2).

Lemma negb3_or : forall b1 b2, negb3 (orb3 b1 b2) = andb3 (negb3 b1) (negb3 b2).

Hint Rewrite negb3_neg negb3_and negb3_or negb3P andb3P orb3P : vlib.

Delimit Scope coq_nat_scope with coq_nat.

Notation "m <= n" := (le m n) : coq_nat_scope.
Notation "m < n" := (lt m n) : coq_nat_scope.
Notation "m >= n" := (ge m n) : coq_nat_scope.
Notation "m > n" := (gt m n) : coq_nat_scope.

Inductive LtSpec (A : Type) (le lt : A -> A -> Prop) (x y: A): bool -> Prop :=
  | LtSpecLt : lt x y -> LtSpec le lt x y true
  | LtSpecGe : le y x -> LtSpec le lt x y false.

Inductive CmpSpecFull (A : Type) (lt : A -> A -> Prop) (x y: A)
  : bool -> bool -> bool -> bool -> bool -> bool -> comparison -> Prop :=
  | CmpSpecLt : lt x y -> CmpSpecFull lt x y true true false false false false Lt
  | CmpSpecEq : x = y -> CmpSpecFull lt x y false true true true false true Eq
  | CmpSpecGt : lt y x -> CmpSpecFull lt x y false false false false true true Gt.

Definition len (m n:nat) := match tt with tt => leb m n end.

Definition ltn m n := len (S m) n.

Notation "m <= n" := (len m n) : nat_scope.
Notation "m < n" := (ltn m n) : nat_scope.
Notation "m >= n" := (n <= m) (only parsing) : nat_scope.
Notation "m > n" := (n < m) (only parsing) : nat_scope.

Lemma add0n : forall n, 0 + n = n.
Lemma addSn : forall m n, S m + n = S (m + n).
Lemma add1n : forall n, 1 + n = S n.
Lemma addn0 : forall x, x + 0 = x.
Lemma addnS : forall m n, m + (S n) = S (m + n).
Lemma addn1 : forall n, n + 1 = S n.
Lemma addSnnS : forall m n, S m + n = m + (S n).

Lemma addnC : forall x y, x + y = y + x.
Lemma addnA : forall x y z, x + (y + z) = x + y + z.
Lemma addnCA : forall x y z, x + (y + z) = y + (x + z).
Lemma addnAC : forall x y z, x + y + z = x + z + y.

Lemma addn_eq0 : forall m n, (m + n == 0) = (m == 0) && (n == 0).

Lemma eqn_addl : forall p m n, (p + m == p + n) = (m == n).

Lemma eqn_addr : forall p m n, (m + p == n + p) = (m == n).

Lemma sub0n : forall x, 0 - x = 0.
Lemma subn0 : forall x, x - 0 = x.
Lemma subnn : forall x, x - x = 0.
Lemma subSS : forall n m, S m - S n = m - n.

Lemma subn_add2l : forall p m n, (p + m) - (p + n) = m - n.
Lemma subn_add2r : forall p m n, (m + p) - (n + p) = m - n.

Lemma subSnn : forall n, S n - n = 1.
Lemma subn_sub : forall m n p, (n - m) - p = n - (m + p).
Lemma subnAC : forall x y z, x - y - z = x - z - y.

Hint Rewrite
  add0n addSn addn0 addnS addn_eq0 eqn_addl eqn_addr
  sub0n subn0 subnn subSS subn_add2l subn_add2r : vlib.

Lemma eq0S : forall n, (O == S n) = false.
Lemma eqS0 : forall n, (S n == O) = false.
Lemma eqSS : forall m n, (S m == S n) = (m == n).
Lemma eqnn : forall n : nat, (n == n).
Lemma eqnC : forall x y : nat, (x == y) = (y == x).

Hint Resolve eqnn.
Hint Rewrite eqnn eqSS eq0S eqS0 : vlib.

Lemma ltnE : forall m n, (m < n) = negb (n <= m).

Lemma lenE : forall m n, (m <= n) = negb (n < m).

Lemma lenE_sub : forall m n, (m <= n) = (m - n == 0).

Lemma ltnE_sub : forall m n, (m < n) = (m + 1 - n == 0).

Lemma leP : forall x y, LtSpec lt le x y (x <= y).

Lemma ltP : forall x y, LtSpec le lt x y (x < y).

Lemma ltn_correct: forall x y, (x < y)%coq_nat -> x < y.

Lemma len_correct: forall x y, (x <= y)%coq_nat -> x <= y.

Lemma ltn_complete: forall x y, x < y -> (x < y)%coq_nat.

Lemma len_complete: forall x y, x <= y -> (x <= y)%coq_nat.

Lemma lenP : forall x y, LtSpec ltn len x y (x <= y).

Lemma ltnP : forall x y, LtSpec len ltn x y (x < y).

Lemma le0n : forall n, 0 <= n.
Lemma len0 : forall n, (n <= 0) = (n == 0).
Lemma lenn : forall n, n <= n.
Lemma lenSn : forall n, n <= S n.

Lemma lt0Sn : forall n, 0 < S n.
Lemma ltn0 : forall n, (n < 0) = false.
Lemma ltnn : forall n, (n < n) = false.
Lemma ltnSn : forall n, (n < S n).

Lemma leSS : forall m n, (S m <= S n) = (m <= n).
Lemma ltSS : forall m n, (S m < S n) = (m < n).

Hint Resolve lenn lenSn ltnn ltnSn.

Lemma eq_len : forall m n, m = n -> m <= n.

Lemma ltnS : forall m n, (m < S n) = (m <= n).

Lemma leSn : forall m n, (S m <= n) = (m < n).

Hint Rewrite leSS le0n len0 lenn lenSn ltSS lt0Sn ltn0 ltnn ltnSn ltnS leSn : vlib.

Lemma lt0n : forall n, (0 < n) = negb (n == 0).
Lemma lt0n_neq0 : forall n, 0 < n -> negb (n == 0).
Lemma eqn0_Nlt0n : forall n, n == 0 = negb (0 < n).
Lemma neq0_lt0n : forall n, n == 0 = false -> 0 < n.
Hint Resolve lt0n_neq0 neq0_lt0n.

Lemma len_anti : forall m n, m <= n -> n <= m -> n = m.
Hint Immediate len_anti : lib.

Lemma eqn_leAle : forall m n, (m == n) = (m <= n) && (n <= m).

Lemma neqn_ltVlt : forall m n, negb (m == n) = (m < n) || (n < m).

Lemma len_eqVlt : forall m n, len m n = (m == n) || (m < n).

Lemma ltn_neqAle : forall m n, (m < n) = negb (m == n) && (m <= n).

Lemma len_trans : forall n m p, m <= n -> n <= p -> m <= p.

Lemma len_ltn_trans : forall n m p, m <= n -> n < p -> m < p.

Lemma ltn_len_trans : forall n m p, m < n -> n <= p -> m < p.

Lemma ltn_trans : forall n m p, m < n -> n < p -> m < p.

Lemma ltnW : forall m n, m < n -> m <= n.
Hint Resolve ltnW.

Lemma lenW : forall m n, m <= n -> m <= (S n).

Lemma len_total : forall m n, (m <= n) || (n <= m).

Lemma nat_comparenn: forall x, nat_compare x x = Eq.

Lemma cmpP : forall x y,
  CmpSpecFull ltn x y (x < y) (x <= y) (x == y) (y == x) (y < x) (y <= x) (nat_compare x y).

Lemma len_add2l : forall p m n, (p + m <= p + n) = (m <= n).

Lemma ltn_add2l : forall p m n, (p + m < p + n) = (m < n).

Lemma len_add2r : forall p m n, (m + p <= n + p) = (m <= n).

Lemma ltn_add2r : forall p m n, (m + p < n + p) = (m < n).

Lemma len_add : forall m1 m2 n1 n2,
  m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2.

Lemma len_addr : forall m n, n <= n + m.

Lemma len_addl : forall m n, n <= m + n.

Lemma ltn_addr : forall m n p, m < n -> m < n + p.

Lemma ltn_addl : forall m n p, m < n -> m < p + n.

Lemma lt0_addn : forall m n, (0 < m + n) = (0 < m) || (0 < n).

Lemma lt0_subn : forall m n, (0 < n - m) = (m < n).

Lemma subn_eq0 : forall m n, (m - n == 0) = (m <= n).

Lemma len_sub_add : forall m n p, (m - n <= p) = (m <= n + p).

Lemma len_subr : forall m n, n - m <= n.

Lemma subnKC : forall m n, m <= n -> m + (n - m) = n.

Lemma subnK : forall m n, m <= n -> (n - m) + m = n.

Lemma addn_subA : forall m n p, p <= n -> m + (n - p) = m + n - p.

Lemma subn_subA : forall m n p, p <= n -> m - (n - p) = m + p - n.

Lemma subKn : forall m n, m <= n -> n - (n - m) = m.

Lemma len_subS : forall m n, m <= n -> S n - m = S (n - m).

Lemma ltn_subS : forall m n, m < n -> n - m = S (n - S m).

Lemma len_sub2r : forall p m n, (m <= n) -> (m - p <= n - p).

Lemma len_sub2l : forall p m n, m <= n -> p - n <= p - m.

Lemma len_sub2 : forall m1 m2 n1 n2,
  m1 <= m2 -> n2 <= n1 -> m1 - n1 <= m2 - n2.

Lemma ltn_sub2r : forall p m n, p < n -> m < n -> m - p < n - p.

Lemma ltn_sub2l : forall p m n, m < p -> m < n -> p - n < p - m.

Lemma ltn_add_sub : forall m n p, (m + n < p) = (n < p - m).

Lemma lenE_diff: forall m n, m <= n -> exists k, n = m + k.

Lemma ltnE_diff: forall m n, m < n -> exists k, n = S (m + k).

Lemma len_subnE : forall m n, (m <= m - n) = (n == 0) || (m == 0).

Lemma mul0n : forall n, 0 * n = 0.
Lemma muln0 : forall n, n * 0 = 0.
Lemma mul1n : forall n, 1 * n = n.
Lemma muln1 : forall n, n * 1 = n.

Lemma mulSn : forall m n, S m * n = n + m * n.
Lemma mulSnr : forall m n, S m * n = m * n + n.
Lemma mulnS : forall m n, m * S n = m + m * n.
Lemma mulnSr : forall m n, m * S n = m * n + m.

Lemma mulnC : forall m n, m * n = n * m.

Lemma muln_addl : forall x y z, (x + y) * z = x * z + y * z.

Lemma muln_addr : forall x y z, x * (y + z) = x * y + x * z.

Lemma muln_subl : forall x y z, (x - y) * z = x * z - y * z.

Lemma muln_subr : forall x y z, x * (y - z) = x * y - x * z.

Lemma mulnA : forall x y z, x * (y * z) = x * y * z.

Lemma mulnCA : forall x y z, x * (y * z) = y * (x * z).

Lemma mulnAC : forall x y z, x * y * z = x * z * y.

Lemma eqn_mul0 : forall m n, (m * n == 0) = (m == 0) || (n == 0).

Lemma eqn_mul1 : forall m n, (m * n == 1) = (m == 1) && (n == 1).

Lemma lt0_muln : forall m n, (0 < m * n) = (0 < m) && (0 < n).

Lemma len_pmull : forall m n, 0 < n -> m <= n * m.

Lemma len_pmulr : forall m n, 0 < n -> m <= m * n.

Lemma len_mul2l : forall m n1 n2, (m * n1 <= m * n2) = (m == 0) || (n1 <= n2).

Lemma len_mul2r : forall m n1 n2, (n1 * m <= n2 * m) = (m == 0) || (n1 <= n2).

Lemma len_mul : forall m1 m2 n1 n2, m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2.

Lemma eqn_mul2l : forall m n1 n2, (m * n1 == m * n2) = (m == 0) || (n1 == n2).

Lemma eqn_mul2r : forall m n1 n2, (n1 * m == n2 * m) = (m == 0) || (n1 == n2).

Lemma len_pmul2l : forall m n1 n2, 0 < m -> (m * n1 <= m * n2) = (n1 <= n2).
Implicit Arguments len_pmul2l [m n1 n2].

Lemma len_pmul2r : forall m n1 n2, 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2).
Implicit Arguments len_pmul2r [m n1 n2].

Lemma eqn_pmul2l : forall m n1 n2, 0 < m -> (m * n1 == m * n2) = (n1 == n2).
Implicit Arguments eqn_pmul2l [m n1 n2].

Lemma eqn_pmul2r : forall m n1 n2, 0 < m -> (n1 * m == n2 * m) = (n1 == n2).
Implicit Arguments eqn_pmul2r [m n1 n2].

Lemma ltn_mul2l : forall m n1 n2, (m * n1 < m * n2) = (0 < m) && (n1 < n2).

Lemma ltn_mul2r : forall m n1 n2, (n1 * m < n2 * m) = (0 < m) && (n1 < n2).

Lemma ltn_pmul2l : forall m n1 n2, 0 < m -> (m * n1 < m * n2) = (n1 < n2).
Implicit Arguments ltn_pmul2l [m n1 n2].

Lemma ltn_pmul2r : forall m n1 n2, 0 < m -> (n1 * m < n2 * m) = (n1 < n2).
Implicit Arguments ltn_pmul2r [m n1 n2].

Lemma ltn_mul : forall m1 m2 n1 n2, m1 < n1 -> m2 < n2 -> m1 * m2 < n1 * n2.

Lemma ltn_Pmull : forall m n, 1 < n -> 0 < m -> m < n * m.

Lemma ltn_Pmulr : forall m n, 1 < n -> 0 < m -> m < m * n.

Lemma lenS : forall m n, n <= m -> n <= S m.

Lemma ltn_of_leS : forall n m : nat, (n < m) -> (S n <= m).

Lemma leSn_of_lt : forall n m : nat, (S n <= m) -> (n < m).

Lemma len_mul2l_imp : forall m n1 n2, n1 <= n2 -> (m * n1 <= m * n2).

Lemma len_mul2r_imp : forall m n1 n2, n1 <= n2 -> (n1 * m <= n2 * m).

Hint Resolve lenS len_addl len_addr len_trans len_add2r len_add2l len_sub2r len_sub2l
             len_mul2l_imp len_mul2r_imp : vlib.
Hint Immediate ltn_of_leS leSn_of_lt: vlib.

Hint Rewrite add0n addSn addn0 addnS addn_eq0 eqn_addl eqn_addr
  sub0n subn0 subnn subSS subn_add2l subn_add2r
  nat_comparenn
  len_add2l ltn_add2l len_add2r ltn_add2r len_addr len_addl
  lt0_addn lt0_subn len_sub_add len_subnE
  mul0n muln0 mul1n muln1

  muln_addl muln_addr muln_subl muln_subr
  eqn_mul0 eqn_mul1 lt0_muln
  len_mul2l len_mul2r eqn_mul2l eqn_mul2r ltn_mul2l ltn_mul2r : vlib.

Hint Rewrite addnA mulnA : vlibA.

Fixpoint iter (A : Type) n (f : A -> A) (v : A): A :=
  match n with
    | O => v
    | S n => f (iter n f v)
  end.

Fixpoint iter_rec (A : Type) n (f : A -> A) (v : A): A :=
  match n with
    | O => v
    | S n => iter_rec n f (f v)
  end.

Lemma iter_recS: forall A n f (v: A), iter_rec (S n) f v = f (iter_rec n f v).

Lemma iter_recE: forall A n f (v: A), iter_rec n f v = iter n f v.

Section ZZZ.

Local Open Scope Z_scope.

Lemma Zplus_mod_same: forall a n : Z, (a + n) mod n = a mod n.

Lemma Zmod_too_small:
  forall a n, -n <= a < 0 -> a mod n = n + a.

Lemma Zmod_too_big:
  forall a n, n <= a < n + n -> a mod n = a - n.

Lemma Zopp_mod_idemp: forall a m, - (a mod m) mod m = - a mod m.

Lemma Zmod_opp_expand: forall a b, - a mod b = (b - a) mod b.

Lemma Zmod_eqD :
  forall a b m (H: a mod m = b mod m) (NEQ: m <> 0), exists k, a = b + k * m.

Lemma ZdoubleE: forall x, Zdouble x = x * 2.

Lemma ZltP:
  forall x y, LtSpec Zle Zlt x y (Zlt_bool x y).

Lemma ZleP:
  forall x y, LtSpec Zlt Zle x y (Zle_bool x y).

Lemma ZcmpP:
  forall x y, CmpSpecFull Zlt x y
    (Zlt_bool x y) (Zle_bool x y) (Zeq_bool x y) (Zeq_bool y x)
    (Zlt_bool y x) (Zle_bool y x) (Zcompare x y).

End ZZZ.

Hint Rewrite
  Zmod_0_l Z_mod_same_full
  Zplus_mod_idemp_l Zplus_mod_idemp_r
  Zminus_mod_idemp_l Zminus_mod_idemp_r Zopp_mod_idemp : vlib.