diff options
Diffstat (limited to 'theories/Numbers/Natural')
19 files changed, 6855 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v new file mode 100644 index 00000000..f58b87d8 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -0,0 +1,156 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NBase. + +Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NBasePropMod := NBasePropFunct NAxiomsMod. + +Open Local Scope NatScope. + +Theorem add_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2. +Proof NZadd_wd. + +Theorem add_0_l : forall n : N, 0 + n == n. +Proof NZadd_0_l. + +Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m). +Proof NZadd_succ_l. + +(** Theorems that are valid for both natural numbers and integers *) + +Theorem add_0_r : forall n : N, n + 0 == n. +Proof NZadd_0_r. + +Theorem add_succ_r : forall n m : N, n + S m == S (n + m). +Proof NZadd_succ_r. + +Theorem add_comm : forall n m : N, n + m == m + n. +Proof NZadd_comm. + +Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p. +Proof NZadd_assoc. + +Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q). +Proof NZadd_shuffle1. + +Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p). +Proof NZadd_shuffle2. + +Theorem add_1_l : forall n : N, 1 + n == S n. +Proof NZadd_1_l. + +Theorem add_1_r : forall n : N, n + 1 == S n. +Proof NZadd_1_r. + +Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m. +Proof NZadd_cancel_l. + +Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m. +Proof NZadd_cancel_r. + +(* Theorems that are valid for natural numbers but cannot be proved for Z *) + +Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. +Proof. +intros n m; induct n. +(* The next command does not work with the axiom add_0_l from NAddSig *) +rewrite add_0_l. intuition reflexivity. +intros n IH. rewrite add_succ_l. +setoid_replace (S (n + m) == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). +setoid_replace (S n == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). tauto. +Qed. + +Theorem eq_add_succ : + forall n m : N, (exists p : N, n + m == S p) <-> + (exists n' : N, n == S n') \/ (exists m' : N, m == S m'). +Proof. +intros n m; cases n. +split; intro H. +destruct H as [p H]. rewrite add_0_l in H; right; now exists p. +destruct H as [[n' H] | [m' H]]. +symmetry in H; false_hyp H neq_succ_0. +exists m'; now rewrite add_0_l. +intro n; split; intro H. +left; now exists n. +exists (n + m); now rewrite add_succ_l. +Qed. + +Theorem eq_add_1 : forall n m : N, + n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. +Proof. +intros n m H. +assert (H1 : exists p : N, n + m == S p) by now exists 0. +apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. +left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H. +apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. +right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H. +apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. +Qed. + +Theorem succ_add_discr : forall n m : N, m ~= S (n + m). +Proof. +intro n; induct m. +apply neq_symm. apply neq_succ_0. +intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. +unfold not in IH; now apply IH. +Qed. + +Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m). +Proof. +intros n m; cases n. +intro H; now elim H. +intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ. +Qed. + +Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m). +Proof. +intros n m H; rewrite (add_comm n (P m)); +rewrite (add_comm n m); now apply add_pred_l. +Qed. + +(* One could define n <= m as exists p : N, p + n == m. Then we have +dichotomy: + +forall n m : N, n <= m \/ m <= n, + +i.e., + +forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n) (1) + +We will need (1) in the proof of induction principle for integers +constructed as pairs of natural numbers. The formula (1) can be proved +using properties of order and truncated subtraction. Thus, p would be +m - n or n - m and (1) would hold by theorem sub_add from Sub.v +depending on whether n <= m or m <= n. However, in proving induction +for integers constructed from natural numbers we do not need to +require implementations of order and sub; it is enough to prove (1) +here. *) + +Theorem add_dichotomy : + forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n). +Proof. +intros n m; induct n. +left; exists m; apply add_0_r. +intros n IH. +destruct IH as [[p H] | [p H]]. +destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H. +rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l. +left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H. +right; exists (S p). rewrite add_succ_l; now rewrite H. +Qed. + +End NAddPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v new file mode 100644 index 00000000..7024fd00 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NAddOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NOrder. + +Module NAddOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. +Open Local Scope NatScope. + +Theorem add_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m. +Proof NZadd_lt_mono_l. + +Theorem add_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p. +Proof NZadd_lt_mono_r. + +Theorem add_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q. +Proof NZadd_lt_mono. + +Theorem add_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m. +Proof NZadd_le_mono_l. + +Theorem add_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p. +Proof NZadd_le_mono_r. + +Theorem add_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q. +Proof NZadd_le_mono. + +Theorem add_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q. +Proof NZadd_lt_le_mono. + +Theorem add_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. +Proof NZadd_le_lt_mono. + +Theorem add_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m. +Proof NZadd_pos_pos. + +Theorem lt_add_pos_l : forall n m : N, 0 < n -> m < n + m. +Proof NZlt_add_pos_l. + +Theorem lt_add_pos_r : forall n m : N, 0 < n -> m < m + n. +Proof NZlt_add_pos_r. + +Theorem le_lt_add_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. +Proof NZle_lt_add_lt. + +Theorem lt_le_add_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. +Proof NZlt_le_add_lt. + +Theorem le_le_add_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_add_le. + +Theorem add_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. +Proof NZadd_lt_cases. + +Theorem add_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. +Proof NZadd_le_cases. + +Theorem add_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. +Proof NZadd_pos_cases. + +(* Theorems true for natural numbers *) + +Theorem le_add_r : forall n m : N, n <= n + m. +Proof. +intro n; induct m. +rewrite add_0_r; now apply eq_le_incl. +intros m IH. rewrite add_succ_r; now apply le_le_succ_r. +Qed. + +Theorem lt_lt_add_r : forall n m p : N, n < m -> n < m + p. +Proof. +intros n m p H; rewrite <- (add_0_r n). +apply add_lt_le_mono; [assumption | apply le_0_l]. +Qed. + +Theorem lt_lt_add_l : forall n m p : N, n < m -> n < p + m. +Proof. +intros n m p; rewrite add_comm; apply lt_lt_add_r. +Qed. + +Theorem add_pos_l : forall n m : N, 0 < n -> 0 < n + m. +Proof. +intros; apply NZadd_pos_nonneg. assumption. apply le_0_l. +Qed. + +Theorem add_pos_r : forall n m : N, 0 < m -> 0 < n + m. +Proof. +intros; apply NZadd_nonneg_pos. apply le_0_l. assumption. +Qed. + +(* The following property is used to prove the correctness of the +definition of order on integers constructed from pairs of natural numbers *) + +Theorem add_lt_repl_pair : forall n m n' m' u v : N, + n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. +Proof. +intros n m n' m' u v H1 H2. +symmetry in H2. assert (H3 : n' + m <= n + m') by now apply eq_le_incl. +pose proof (add_lt_le_mono _ _ _ _ H1 H3) as H4. +rewrite (add_shuffle2 n u), (add_shuffle1 m v), (add_comm m n) in H4. +do 2 rewrite <- add_assoc in H4. do 2 apply <- add_lt_mono_l in H4. +now rewrite (add_comm n' u), (add_comm m' v). +Qed. + +End NAddOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v new file mode 100644 index 00000000..750cc977 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -0,0 +1,71 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NZAxioms. + +Set Implicit Arguments. + +Module Type NAxiomsSig. +Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. + +Delimit Scope NatScope with Nat. +Notation N := NZ. +Notation Neq := NZeq. +Notation N0 := NZ0. +Notation N1 := (NZsucc NZ0). +Notation S := NZsucc. +Notation P := NZpred. +Notation add := NZadd. +Notation mul := NZmul. +Notation sub := NZsub. +Notation lt := NZlt. +Notation le := NZle. +Notation min := NZmin. +Notation max := NZmax. +Notation "x == y" := (Neq x y) (at level 70) : NatScope. +Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope. +Notation "0" := NZ0 : NatScope. +Notation "1" := (NZsucc NZ0) : NatScope. +Notation "x + y" := (NZadd x y) : NatScope. +Notation "x - y" := (NZsub x y) : NatScope. +Notation "x * y" := (NZmul x y) : NatScope. +Notation "x < y" := (NZlt x y) : NatScope. +Notation "x <= y" := (NZle x y) : NatScope. +Notation "x > y" := (NZlt y x) (only parsing) : NatScope. +Notation "x >= y" := (NZle y x) (only parsing) : NatScope. + +Open Local Scope NatScope. + +Parameter Inline recursion : forall A : Type, A -> (N -> A -> A) -> N -> A. +Implicit Arguments recursion [A]. + +Axiom pred_0 : P 0 == 0. + +Axiom recursion_wd : forall (A : Type) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' -> + forall x x' : N, x == x' -> + Aeq (recursion a f x) (recursion a' f' x'). + +Axiom recursion_0 : + forall (A : Type) (a : A) (f : N -> A -> A), recursion a f 0 = a. + +Axiom recursion_succ : + forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A), + Aeq a a -> fun2_wd Neq Aeq Aeq f -> + forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)). + +(*Axiom dep_rec : + forall A : N -> Type, A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.*) + +End NAxiomsSig. + diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v new file mode 100644 index 00000000..3e4032b5 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -0,0 +1,288 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NBase.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export Decidable. +Require Export NAxioms. +Require Import NZMulOrder. (* The last property functor on NZ, which subsumes all others *) + +Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig). + +Open Local Scope NatScope. + +(* We call the last property functor on NZ, which includes all the previous +ones, to get all properties of NZ at once. This way we will include them +only one time. *) + +Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod. + +(* Here we probably need to re-prove all axioms declared in NAxioms.v to +make sure that the definitions like N, S and add are unfolded in them, +since unfolding is done only inside a functor. In fact, we'll do it in the +files that prove the corresponding properties. In those files, we will also +rename properties proved in NZ files by removing NZ from their names. In +this way, one only has to consult, for example, NAdd.v to see all +available properties for add, i.e., one does not have to go to NAxioms.v +for axioms and NZAdd.v for theorems. *) + +Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2. +Proof NZsucc_wd. + +Theorem pred_wd : forall n1 n2 : N, n1 == n2 -> P n1 == P n2. +Proof NZpred_wd. + +Theorem pred_succ : forall n : N, P (S n) == n. +Proof NZpred_succ. + +Theorem pred_0 : P 0 == 0. +Proof pred_0. + +Theorem Neq_refl : forall n : N, n == n. +Proof (proj1 NZeq_equiv). + +Theorem Neq_symm : forall n m : N, n == m -> m == n. +Proof (proj2 (proj2 NZeq_equiv)). + +Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p. +Proof (proj1 (proj2 NZeq_equiv)). + +Theorem neq_symm : forall n m : N, n ~= m -> m ~= n. +Proof NZneq_symm. + +Theorem succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2. +Proof NZsucc_inj. + +Theorem succ_inj_wd : forall n1 n2 : N, S n1 == S n2 <-> n1 == n2. +Proof NZsucc_inj_wd. + +Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m. +Proof NZsucc_inj_wd_neg. + +(* Decidability and stability of equality was proved only in NZOrder, but +since it does not mention order, we'll put it here *) + +Theorem eq_dec : forall n m : N, decidable (n == m). +Proof NZeq_dec. + +Theorem eq_dne : forall n m : N, ~ ~ n == m <-> n == m. +Proof NZeq_dne. + +(* Now we prove that the successor of a number is not zero by defining a +function (by recursion) that maps 0 to false and the successor to true *) + +Definition if_zero (A : Set) (a b : A) (n : N) : A := + recursion a (fun _ _ => b) n. + +Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd. +Proof. +intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). +reflexivity. unfold fun2_eq; now intros. assumption. +Qed. + +Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a. +Proof. +unfold if_zero; intros; now rewrite recursion_0. +Qed. + +Theorem if_zero_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b. +Proof. +intros; unfold if_zero. +now rewrite (@recursion_succ A (@eq A)); [| | unfold fun2_wd; now intros]. +Qed. + +Implicit Arguments if_zero [A]. + +Theorem neq_succ_0 : forall n : N, S n ~= 0. +Proof. +intros n H. +assert (true = false); [| discriminate]. +replace true with (if_zero false true (S n)) by apply if_zero_succ. +pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0. +now rewrite H. +Qed. + +Theorem neq_0_succ : forall n : N, 0 ~= S n. +Proof. +intro n; apply neq_symm; apply neq_succ_0. +Qed. + +(* Next, we show that all numbers are nonnegative and recover regular induction +from the bidirectional induction on NZ *) + +Theorem le_0_l : forall n : N, 0 <= n. +Proof. +NZinduct n. +now apply NZeq_le_incl. +intro n; split. +apply NZle_le_succ_r. +intro H; apply -> NZle_succ_r in H; destruct H as [H | H]. +assumption. +symmetry in H; false_hyp H neq_succ_0. +Qed. + +Theorem induction : + forall A : N -> Prop, predicate_wd Neq A -> + A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n. +Proof. +intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption. +intros; auto; apply le_0_l. apply le_0_l. +Qed. + +(* The theorems NZinduction, NZcentral_induction and the tactic NZinduct +refer to bidirectional induction, which is not useful on natural +numbers. Therefore, we define a new induction tactic for natural numbers. +We do not have to call "Declare Left Step" and "Declare Right Step" +commands again, since the data for stepl and stepr tactics is inherited +from NZ. *) + +Ltac induct n := induction_maker n ltac:(apply induction). + +Theorem case_analysis : + forall A : N -> Prop, predicate_wd Neq A -> + A 0 -> (forall n : N, A (S n)) -> forall n : N, A n. +Proof. +intros; apply induction; auto. +Qed. + +Ltac cases n := induction_maker n ltac:(apply case_analysis). + +Theorem neq_0 : ~ forall n, n == 0. +Proof. +intro H; apply (neq_succ_0 0). apply H. +Qed. + +Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m. +Proof. +cases n. split; intro H; +[now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0]. +intro n; split; intro H; [now exists n | apply neq_succ_0]. +Qed. + +Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m. +Proof. +cases n. +now left. +intro n; right; now exists n. +Qed. + +Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1. +Proof. +cases n. +rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto. +split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H]. +intro n. rewrite pred_succ. +setoid_replace (S n == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). +rewrite succ_inj_wd. tauto. +Qed. + +Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n. +Proof. +cases n. +intro H; elimtype False; now apply H. +intros; now rewrite pred_succ. +Qed. + +Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m. +Proof. +intros n m; cases n. +intros H; elimtype False; now apply H. +intros n _; cases m. +intros H; elimtype False; now apply H. +intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3. +Qed. + +(* The following induction principle is useful for reasoning about, e.g., +Fibonacci numbers *) + +Section PairInduction. + +Variable A : N -> Prop. +Hypothesis A_wd : predicate_wd Neq A. + +Add Morphism A with signature Neq ==> iff as A_morph. +Proof. +exact A_wd. +Qed. + +Theorem pair_induction : + A 0 -> A 1 -> + (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n. +Proof. +intros until 3. +assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))]. +induct n; [ | intros n [IH1 IH2]]; auto. +Qed. + +End PairInduction. + +(*Ltac pair_induct n := induction_maker n ltac:(apply pair_induction).*) + +(* The following is useful for reasoning about, e.g., Ackermann function *) +Section TwoDimensionalInduction. + +Variable R : N -> N -> Prop. +Hypothesis R_wd : relation_wd Neq Neq R. + +Add Morphism R with signature Neq ==> Neq ==> iff as R_morph. +Proof. +exact R_wd. +Qed. + +Theorem two_dim_induction : + R 0 0 -> + (forall n m, R n m -> R n (S m)) -> + (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m. +Proof. +intros H1 H2 H3. induct n. +induct m. +exact H1. exact (H2 0). +intros n IH. induct m. +now apply H3. exact (H2 (S n)). +Qed. + +End TwoDimensionalInduction. + +(*Ltac two_dim_induct n m := + try intros until n; + try intros until m; + pattern n, m; apply two_dim_induction; clear n m; + [solve_relation_wd | | | ].*) + +Section DoubleInduction. + +Variable R : N -> N -> Prop. +Hypothesis R_wd : relation_wd Neq Neq R. + +Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1. +Proof. +exact R_wd. +Qed. + +Theorem double_induction : + (forall m : N, R 0 m) -> + (forall n : N, R (S n) 0) -> + (forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m. +Proof. +intros H1 H2 H3; induct n; auto. +intros n H; cases m; auto. +Qed. + +End DoubleInduction. + +Ltac double_induct n m := + try intros until n; + try intros until m; + pattern n, m; apply double_induction; clear n m; + [solve_relation_wd | | | ]. + +End NBasePropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v new file mode 100644 index 00000000..e15e4672 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -0,0 +1,298 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NDefOps.v 11039 2008-06-02 23:26:13Z letouzey $ i*) + +Require Import Bool. (* To get the orb and negb function *) +Require Export NStrongRec. + +Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod. +Open Local Scope NatScope. + +(*****************************************************) +(** Addition *) + +Definition def_add (x y : N) := recursion y (fun _ p => S p) x. + +Infix Local "++" := def_add (at level 50, left associativity). + +Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd. +Proof. +unfold def_add. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (Aeq := Neq). +assumption. +unfold fun2_eq; intros _ _ _ p p' Epp'; now rewrite Epp'. +assumption. +Qed. + +Theorem def_add_0_l : forall y : N, 0 ++ y == y. +Proof. +intro y. unfold def_add. now rewrite recursion_0. +Qed. + +Theorem def_add_succ_l : forall x y : N, S x ++ y == S (x ++ y). +Proof. +intros x y; unfold def_add. +rewrite (@recursion_succ N Neq); try reflexivity. +unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2. +Qed. + +Theorem def_add_add : forall n m : N, n ++ m == n + m. +Proof. +intros n m; induct n. +now rewrite def_add_0_l, add_0_l. +intros n H. now rewrite def_add_succ_l, add_succ_l, H. +Qed. + +(*****************************************************) +(** Multiplication *) + +Definition def_mul (x y : N) := recursion 0 (fun _ p => p ++ x) y. + +Infix Local "**" := def_mul (at level 40, left associativity). + +Lemma def_mul_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_add p x). +Proof. +unfold fun2_wd. intros. now apply def_add_wd. +Qed. + +Lemma def_mul_step_equal : + forall x x' : N, x == x' -> + fun2_eq Neq Neq Neq (fun _ p => def_add p x) (fun x p => def_add p x'). +Proof. +unfold fun2_eq; intros; apply def_add_wd; assumption. +Qed. + +Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd. +Proof. +unfold def_mul. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (Aeq := Neq). +reflexivity. apply def_mul_step_equal. assumption. assumption. +Qed. + +Theorem def_mul_0_r : forall x : N, x ** 0 == 0. +Proof. +intro. unfold def_mul. now rewrite recursion_0. +Qed. + +Theorem def_mul_succ_r : forall x y : N, x ** S y == x ** y ++ x. +Proof. +intros x y; unfold def_mul. +now rewrite (@recursion_succ N Neq); [| apply def_mul_step_wd |]. +Qed. + +Theorem def_mul_mul : forall n m : N, n ** m == n * m. +Proof. +intros n m; induct m. +now rewrite def_mul_0_r, mul_0_r. +intros m IH; now rewrite def_mul_succ_r, mul_succ_r, def_add_add, IH. +Qed. + +(*****************************************************) +(** Order *) + +Definition def_ltb (m : N) : N -> bool := +recursion + (if_zero false true) + (fun _ f => fun n => recursion false (fun n' _ => f n') n) + m. + +Infix Local "<<" := def_ltb (at level 70, no associativity). + +Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true). +unfold fun_wd; intros; now apply if_zero_wd. +Qed. + +Lemma lt_step_wd : +fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool)) + (fun _ f => fun n => recursion false (fun n' _ => f n') n). +Proof. +unfold fun2_wd, fun_eq. +intros x x' Exx' f f' Eff' y y' Eyy'. +apply recursion_wd with (Aeq := @eq bool). +reflexivity. +unfold fun2_eq; intros; now apply Eff'. +assumption. +Qed. + +Lemma lt_curry_wd : + forall m m' : N, m == m' -> fun_eq Neq (@eq bool) (def_ltb m) (def_ltb m'). +Proof. +unfold def_ltb. +intros m m' Emm'. +apply recursion_wd with (Aeq := fun_eq Neq (@eq bool)). +apply lt_base_wd. +apply lt_step_wd. +assumption. +Qed. + +Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd. +Proof. +intros; now apply lt_curry_wd. +Qed. + +Theorem def_ltb_base : forall n : N, 0 << n = if_zero false true n. +Proof. +intro n; unfold def_ltb; now rewrite recursion_0. +Qed. + +Theorem def_ltb_step : + forall m n : N, S m << n = recursion false (fun n' _ => m << n') n. +Proof. +intros m n; unfold def_ltb. +pose proof + (@recursion_succ + (N -> bool) + (fun_eq Neq (@eq bool)) + (if_zero false true) + (fun _ f => fun n => recursion false (fun n' _ => f n') n) + lt_base_wd + lt_step_wd + m n n) as H. +now rewrite H. +Qed. + +(* Above, we rewrite applications of function. Is it possible to rewrite +functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to +lt_step n (recursion lt_base lt_step n)? *) + +Theorem def_ltb_0 : forall n : N, n << 0 = false. +Proof. +cases n. +rewrite def_ltb_base; now rewrite if_zero_0. +intro n; rewrite def_ltb_step. now rewrite recursion_0. +Qed. + +Theorem def_ltb_0_succ : forall n : N, 0 << S n = true. +Proof. +intro n; rewrite def_ltb_base; now rewrite if_zero_succ. +Qed. + +Theorem succ_def_ltb_mono : forall n m : N, (S n << S m) = (n << m). +Proof. +intros n m. +rewrite def_ltb_step. rewrite (@recursion_succ bool (@eq bool)); try reflexivity. +unfold fun2_wd; intros; now apply def_ltb_wd. +Qed. + +Theorem def_ltb_lt : forall n m : N, n << m = true <-> n < m. +Proof. +double_induct n m. +cases m. +rewrite def_ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r]. +intro n. rewrite def_ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity]. +intro n. rewrite def_ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r]. +intros n m. rewrite succ_def_ltb_mono. now rewrite <- succ_lt_mono. +Qed. + +(* +(*****************************************************) +(** Even *) + +Definition even (x : N) := recursion true (fun _ p => negb p) x. + +Lemma even_step_wd : fun2_wd Neq (@eq bool) (@eq bool) (fun x p => if p then false else true). +Proof. +unfold fun2_wd. +intros x x' Exx' b b' Ebb'. +unfold eq_bool; destruct b; destruct b'; now simpl. +Qed. + +Add Morphism even with signature Neq ==> (@eq bool) as even_wd. +Proof. +unfold even; intros. +apply recursion_wd with (A := bool) (Aeq := (@eq bool)). +now unfold eq_bool. +unfold fun2_eq. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl. +assumption. +Qed. + +Theorem even_0 : even 0 = true. +Proof. +unfold even. +now rewrite recursion_0. +Qed. + +Theorem even_succ : forall x : N, even (S x) = negb (even x). +Proof. +unfold even. +intro x; rewrite (recursion_succ (@eq bool)); try reflexivity. +unfold fun2_wd. +intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl. +Qed. + +(*****************************************************) +(** Division by 2 *) + +Definition half_aux (x : N) : N * N := + recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x. + +Definition half (x : N) := snd (half_aux x). + +Definition E2 := prod_rel Neq Neq. + +Add Relation (prod N N) E2 +reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv) +symmetry proved by (prod_rel_symm N N Neq Neq E_equiv E_equiv) +transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv) +as E2_rel. + +Lemma half_step_wd: fun2_wd Neq E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))). +Proof. +unfold fun2_wd, E2, prod_rel. +intros _ _ _ p1 p2 [H1 H2]. +destruct p1; destruct p2; simpl in *. +now split; [rewrite H2 |]. +Qed. + +Add Morphism half with signature Neq ==> Neq as half_wd. +Proof. +unfold half. +assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)). +intros x y Exy; unfold half_aux; apply recursion_wd with (Aeq := E2); unfold E2. +unfold E2. +unfold prod_rel; simpl; now split. +unfold fun2_eq, prod_rel; simpl. +intros _ _ _ p1 p2; destruct p1; destruct p2; simpl. +intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption. +unfold E2, prod_rel in H. intros x y Exy; apply H in Exy. +exact (proj2 Exy). +Qed. + +(*****************************************************) +(** Logarithm for the base 2 *) + +Definition log (x : N) : N := +strong_rec 0 + (fun x g => + if (e x 0) then 0 + else if (e x 1) then 0 + else S (g (half x))) + x. + +Add Morphism log with signature Neq ==> Neq as log_wd. +Proof. +intros x x' Exx'. unfold log. +apply strong_rec_wd with (Aeq := Neq); try (reflexivity || assumption). +unfold fun2_eq. intros y y' Eyy' g g' Egg'. +assert (H : e y 0 = e y' 0); [now apply e_wd|]. +rewrite <- H; clear H. +assert (H : e y 1 = e y' 1); [now apply e_wd|]. +rewrite <- H; clear H. +assert (H : S (g (half y)) == S (g' (half y'))); +[apply succ_wd; apply Egg'; now apply half_wd|]. +now destruct (e y 0); destruct (e y 1). +Qed. +*) +End NdefOpsPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v new file mode 100644 index 00000000..f6ccf3db --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -0,0 +1,122 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NIso.v 10934 2008-05-15 21:58:20Z letouzey $ i*) + +Require Import NBase. + +Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). + +Module NBasePropMod2 := NBasePropFunct NAxiomsMod2. + +Notation Local N1 := NAxiomsMod1.N. +Notation Local N2 := NAxiomsMod2.N. +Notation Local Eq1 := NAxiomsMod1.Neq. +Notation Local Eq2 := NAxiomsMod2.Neq. +Notation Local O1 := NAxiomsMod1.N0. +Notation Local O2 := NAxiomsMod2.N0. +Notation Local S1 := NAxiomsMod1.S. +Notation Local S2 := NAxiomsMod2.S. +Notation Local "n == m" := (Eq2 n m) (at level 70, no associativity). + +Definition homomorphism (f : N1 -> N2) : Prop := + f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n). + +Definition natural_isomorphism : N1 -> N2 := + NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p). + +Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd. +Proof. +unfold natural_isomorphism. +intros n m Eqxy. +apply NAxiomsMod1.recursion_wd with (Aeq := Eq2). +reflexivity. +unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd. +assumption. +Qed. + +Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2. +Proof. +unfold natural_isomorphism; now rewrite NAxiomsMod1.recursion_0. +Qed. + +Theorem natural_isomorphism_succ : + forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n). +Proof. +unfold natural_isomorphism. +intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ; +[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd]. +Qed. + +Theorem hom_nat_iso : homomorphism natural_isomorphism. +Proof. +unfold homomorphism, natural_isomorphism; split; +[exact natural_isomorphism_0 | exact natural_isomorphism_succ]. +Qed. + +End Homomorphism. + +Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). + +Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1. +(* This makes the tactic induct available. Since it is taken from +(NBasePropFunct NAxiomsMod1), it refers to induction on N1. *) + +Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2. +Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1. + +Notation Local N1 := NAxiomsMod1.N. +Notation Local N2 := NAxiomsMod2.N. +Notation Local h12 := Hom12.natural_isomorphism. +Notation Local h21 := Hom21.natural_isomorphism. + +Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity). + +Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n. +Proof. +induct n. +now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0. +intros n IH. +now rewrite Hom12.natural_isomorphism_succ, Hom21.natural_isomorphism_succ, IH. +Qed. + +End Inverse. + +Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). + +Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2. +Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1. + +Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2. +Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1. + +Notation Local N1 := NAxiomsMod1.N. +Notation Local N2 := NAxiomsMod2.N. +Notation Local Eq1 := NAxiomsMod1.Neq. +Notation Local Eq2 := NAxiomsMod2.Neq. +Notation Local h12 := Hom12.natural_isomorphism. +Notation Local h21 := Hom21.natural_isomorphism. + +Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop := + Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\ + forall n : N1, Eq1 (f2 (f1 n)) n /\ + forall n : N2, Eq2 (f1 (f2 n)) n. + +Theorem iso_nat_iso : isomorphism h12 h21. +Proof. +unfold isomorphism. +split. apply Hom12.hom_nat_iso. +split. apply Hom21.hom_nat_iso. +split. apply Inverse12.inverse_nat_iso. +apply Inverse21.inverse_nat_iso. +Qed. + +End Isomorphism. + diff --git a/theories/Numbers/Natural/Abstract/NMul.v b/theories/Numbers/Natural/Abstract/NMul.v new file mode 100644 index 00000000..0b00f689 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMul.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NAdd. + +Module NMulPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NAddPropMod := NAddPropFunct NAxiomsMod. +Open Local Scope NatScope. + +Theorem mul_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2. +Proof NZmul_wd. + +Theorem mul_0_l : forall n : N, 0 * n == 0. +Proof NZmul_0_l. + +Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m. +Proof NZmul_succ_l. + +(** Theorems that are valid for both natural numbers and integers *) + +Theorem mul_0_r : forall n, n * 0 == 0. +Proof NZmul_0_r. + +Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. +Proof NZmul_succ_r. + +Theorem mul_comm : forall n m : N, n * m == m * n. +Proof NZmul_comm. + +Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p. +Proof NZmul_add_distr_r. + +Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p. +Proof NZmul_add_distr_l. + +Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p. +Proof NZmul_assoc. + +Theorem mul_1_l : forall n : N, 1 * n == n. +Proof NZmul_1_l. + +Theorem mul_1_r : forall n : N, n * 1 == n. +Proof NZmul_1_r. + +(* Theorems that cannot be proved in NZMul *) + +(* In proving the correctness of the definition of multiplication on +integers constructed from pairs of natural numbers, we'll need the +following fact about natural numbers: + +a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u = a * m' + v + +Here n + m' == n' + m expresses equality of integers (n, m) and (n', m'), +since a pair (a, b) of natural numbers represents the integer a - b. On +integers, the formula above could be proved by moving a * m to the left, +factoring out a and replacing n - m by n' - m'. However, the formula is +required in the process of constructing integers, so it has to be proved +for natural numbers, where terms cannot be moved from one side of an +equation to the other. The proof uses the cancellation laws add_cancel_l +and add_cancel_r. *) + +Theorem add_mul_repl_pair : forall a n m n' m' u v : N, + a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v. +Proof. +intros a n m n' m' u v H1 H2. +apply (@NZmul_wd a a) in H2; [| reflexivity]. +do 2 rewrite mul_add_distr_l in H2. symmetry in H2. +pose proof (NZadd_wd _ _ H1 _ _ H2) as H3. +rewrite (add_shuffle1 (a * m)), (add_comm (a * m) (a * n)) in H3. +do 2 rewrite <- add_assoc in H3. apply -> add_cancel_l in H3. +rewrite (add_assoc u), (add_comm (a * m)) in H3. +apply -> add_cancel_r in H3. +now rewrite (add_comm (a * n') u), (add_comm (a * m') v). +Qed. + +End NMulPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v new file mode 100644 index 00000000..aa21fb50 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -0,0 +1,131 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NAddOrder. + +Module NMulOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NAddOrderPropMod := NAddOrderPropFunct NAxiomsMod. +Open Local Scope NatScope. + +Theorem mul_lt_pred : + forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). +Proof NZmul_lt_pred. + +Theorem mul_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m). +Proof NZmul_lt_mono_pos_l. + +Theorem mul_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p). +Proof NZmul_lt_mono_pos_r. + +Theorem mul_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m). +Proof NZmul_cancel_l. + +Theorem mul_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m). +Proof NZmul_cancel_r. + +Theorem mul_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1). +Proof NZmul_id_l. + +Theorem mul_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1). +Proof NZmul_id_r. + +Theorem mul_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m). +Proof NZmul_le_mono_pos_l. + +Theorem mul_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p). +Proof NZmul_le_mono_pos_r. + +Theorem mul_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. +Proof NZmul_pos_pos. + +Theorem lt_1_mul_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m. +Proof NZlt_1_mul_pos. + +Theorem eq_mul_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0. +Proof NZeq_mul_0. + +Theorem neq_mul_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. +Proof NZneq_mul_0. + +Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0. +Proof NZeq_square_0. + +Theorem eq_mul_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0. +Proof NZeq_mul_0_l. + +Theorem eq_mul_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0. +Proof NZeq_mul_0_r. + +Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m. +Proof. +intros n m; split; intro; +[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg]; +try assumption; apply le_0_l. +Qed. + +Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m. +Proof. +intros n m; split; intro; +[apply NZsquare_le_mono_nonneg | apply NZsquare_le_simpl_nonneg]; +try assumption; apply le_0_l. +Qed. + +Theorem mul_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZmul_2_mono_l. + +(* Theorems that are either not valid on Z or have different proofs on N and Z *) + +Theorem mul_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m. +Proof. +intros; apply NZmul_le_mono_nonneg_l. apply le_0_l. assumption. +Qed. + +Theorem mul_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p. +Proof. +intros; apply NZmul_le_mono_nonneg_r. apply le_0_l. assumption. +Qed. + +Theorem mul_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q. +Proof. +intros; apply NZmul_lt_mono_nonneg; try assumption; apply le_0_l. +Qed. + +Theorem mul_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q. +Proof. +intros; apply NZmul_le_mono_nonneg; try assumption; apply le_0_l. +Qed. + +Theorem lt_0_mul : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. +Proof. +intros n m; split; [intro H | intros [H1 H2]]. +apply -> NZlt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. +now apply NZmul_pos_pos. +Qed. + +Notation mul_pos := lt_0_mul (only parsing). + +Theorem eq_mul_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1. +Proof. +intros n m. +split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. +intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]]. +apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ. +rewrite H1, mul_1_l in H; now split. +destruct (eq_0_gt_0_cases m) as [H2 | H2]. +rewrite H2, mul_0_r in H; false_hyp H neq_0_succ. +apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. +assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m). +rewrite H in H3; false_hyp H3 lt_irrefl. +Qed. + +End NMulOrderPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v new file mode 100644 index 00000000..826ffa2c --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -0,0 +1,539 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NMul. + +Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NMulPropMod := NMulPropFunct NAxiomsMod. +Open Local Scope NatScope. + +(* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *) + +(* Axioms *) + +Theorem lt_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 < m1 <-> n2 < m2). +Proof NZlt_wd. + +Theorem le_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 <= m1 <-> n2 <= m2). +Proof NZle_wd. + +Theorem min_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> min n1 m1 == min n2 m2. +Proof NZmin_wd. + +Theorem max_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> max n1 m1 == max n2 m2. +Proof NZmax_wd. + +Theorem lt_eq_cases : forall n m : N, n <= m <-> n < m \/ n == m. +Proof NZlt_eq_cases. + +Theorem lt_irrefl : forall n : N, ~ n < n. +Proof NZlt_irrefl. + +Theorem lt_succ_r : forall n m : N, n < S m <-> n <= m. +Proof NZlt_succ_r. + +Theorem min_l : forall n m : N, n <= m -> min n m == n. +Proof NZmin_l. + +Theorem min_r : forall n m : N, m <= n -> min n m == m. +Proof NZmin_r. + +Theorem max_l : forall n m : N, m <= n -> max n m == n. +Proof NZmax_l. + +Theorem max_r : forall n m : N, n <= m -> max n m == m. +Proof NZmax_r. + +(* Renaming theorems from NZOrder.v *) + +Theorem lt_le_incl : forall n m : N, n < m -> n <= m. +Proof NZlt_le_incl. + +Theorem eq_le_incl : forall n m : N, n == m -> n <= m. +Proof NZeq_le_incl. + +Theorem lt_neq : forall n m : N, n < m -> n ~= m. +Proof NZlt_neq. + +Theorem le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m. +Proof NZle_neq. + +Theorem le_refl : forall n : N, n <= n. +Proof NZle_refl. + +Theorem lt_succ_diag_r : forall n : N, n < S n. +Proof NZlt_succ_diag_r. + +Theorem le_succ_diag_r : forall n : N, n <= S n. +Proof NZle_succ_diag_r. + +Theorem lt_0_1 : 0 < 1. +Proof NZlt_0_1. + +Theorem le_0_1 : 0 <= 1. +Proof NZle_0_1. + +Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m. +Proof NZlt_lt_succ_r. + +Theorem le_le_succ_r : forall n m : N, n <= m -> n <= S m. +Proof NZle_le_succ_r. + +Theorem le_succ_r : forall n m : N, n <= S m <-> n <= m \/ n == S m. +Proof NZle_succ_r. + +Theorem neq_succ_diag_l : forall n : N, S n ~= n. +Proof NZneq_succ_diag_l. + +Theorem neq_succ_diag_r : forall n : N, n ~= S n. +Proof NZneq_succ_diag_r. + +Theorem nlt_succ_diag_l : forall n : N, ~ S n < n. +Proof NZnlt_succ_diag_l. + +Theorem nle_succ_diag_l : forall n : N, ~ S n <= n. +Proof NZnle_succ_diag_l. + +Theorem le_succ_l : forall n m : N, S n <= m <-> n < m. +Proof NZle_succ_l. + +Theorem lt_succ_l : forall n m : N, S n < m -> n < m. +Proof NZlt_succ_l. + +Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m. +Proof NZsucc_lt_mono. + +Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m. +Proof NZsucc_le_mono. + +Theorem lt_asymm : forall n m : N, n < m -> ~ m < n. +Proof NZlt_asymm. + +Notation lt_ngt := lt_asymm (only parsing). + +Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p. +Proof NZlt_trans. + +Theorem le_trans : forall n m p : N, n <= m -> m <= p -> n <= p. +Proof NZle_trans. + +Theorem le_lt_trans : forall n m p : N, n <= m -> m < p -> n < p. +Proof NZle_lt_trans. + +Theorem lt_le_trans : forall n m p : N, n < m -> m <= p -> n < p. +Proof NZlt_le_trans. + +Theorem le_antisymm : forall n m : N, n <= m -> m <= n -> n == m. +Proof NZle_antisymm. + +(** Trichotomy, decidability, and double negation elimination *) + +Theorem lt_trichotomy : forall n m : N, n < m \/ n == m \/ m < n. +Proof NZlt_trichotomy. + +Notation lt_eq_gt_cases := lt_trichotomy (only parsing). + +Theorem lt_gt_cases : forall n m : N, n ~= m <-> n < m \/ n > m. +Proof NZlt_gt_cases. + +Theorem le_gt_cases : forall n m : N, n <= m \/ n > m. +Proof NZle_gt_cases. + +Theorem lt_ge_cases : forall n m : N, n < m \/ n >= m. +Proof NZlt_ge_cases. + +Theorem le_ge_cases : forall n m : N, n <= m \/ n >= m. +Proof NZle_ge_cases. + +Theorem le_ngt : forall n m : N, n <= m <-> ~ n > m. +Proof NZle_ngt. + +Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m. +Proof NZnlt_ge. + +Theorem lt_dec : forall n m : N, decidable (n < m). +Proof NZlt_dec. + +Theorem lt_dne : forall n m : N, ~ ~ n < m <-> n < m. +Proof NZlt_dne. + +Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m. +Proof NZnle_gt. + +Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m. +Proof NZlt_nge. + +Theorem le_dec : forall n m : N, decidable (n <= m). +Proof NZle_dec. + +Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m. +Proof NZle_dne. + +Theorem nlt_succ_r : forall n m : N, ~ m < S n <-> n < m. +Proof NZnlt_succ_r. + +Theorem lt_exists_pred : + forall z n : N, z < n -> exists k : N, n == S k /\ z <= k. +Proof NZlt_exists_pred. + +Theorem lt_succ_iter_r : + forall (n : nat) (m : N), m < NZsucc_iter (Datatypes.S n) m. +Proof NZlt_succ_iter_r. + +Theorem neq_succ_iter_l : + forall (n : nat) (m : N), NZsucc_iter (Datatypes.S n) m ~= m. +Proof NZneq_succ_iter_l. + +(** Stronger variant of induction with assumptions n >= 0 (n < 0) +in the induction step *) + +Theorem right_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + forall n : N, z <= n -> A n. +Proof NZright_induction. + +Theorem left_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, A z -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, n <= z -> A n. +Proof NZleft_induction. + +Theorem right_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, n <= z -> A n) -> + (forall n : N, z <= n -> A n -> A (S n)) -> + forall n : N, A n. +Proof NZright_induction'. + +Theorem left_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, z <= n -> A n) -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, A n. +Proof NZleft_induction'. + +Theorem strong_right_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> + forall n : N, z <= n -> A n. +Proof NZstrong_right_induction. + +Theorem strong_left_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> + forall n : N, n <= z -> A n. +Proof NZstrong_left_induction. + +Theorem strong_right_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, n <= z -> A n) -> + (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> + forall n : N, A n. +Proof NZstrong_right_induction'. + +Theorem strong_left_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, + (forall n : N, z <= n -> A n) -> + (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> + forall n : N, A n. +Proof NZstrong_left_induction'. + +Theorem order_induction : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, A n. +Proof NZorder_induction. + +Theorem order_induction' : + forall A : N -> Prop, predicate_wd Neq A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + (forall n : N, n <= z -> A n -> A (P n)) -> + forall n : N, A n. +Proof NZorder_induction'. + +(* We don't need order_induction_0 and order_induction'_0 (see NZOrder and +ZOrder) since they boil down to regular induction *) + +(** Elimintation principle for < *) + +Theorem lt_ind : + forall A : N -> Prop, predicate_wd Neq A -> + forall n : N, + A (S n) -> + (forall m : N, n < m -> A m -> A (S m)) -> + forall m : N, n < m -> A m. +Proof NZlt_ind. + +(** Elimintation principle for <= *) + +Theorem le_ind : + forall A : N -> Prop, predicate_wd Neq A -> + forall n : N, + A n -> + (forall m : N, n <= m -> A m -> A (S m)) -> + forall m : N, n <= m -> A m. +Proof NZle_ind. + +(** Well-founded relations *) + +Theorem lt_wf : forall z : N, well_founded (fun n m : N => z <= n /\ n < m). +Proof NZlt_wf. + +Theorem gt_wf : forall z : N, well_founded (fun n m : N => m < n /\ n <= z). +Proof NZgt_wf. + +Theorem lt_wf_0 : well_founded lt. +Proof. +assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)). +intros x y; split. +intro H; split; [apply le_0_l | assumption]. now intros [_ H]. +rewrite H; apply lt_wf. +(* does not work: +setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*) +Qed. + +(* Theorems that are true for natural numbers but not for integers *) + +(* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *) + +Theorem nlt_0_r : forall n : N, ~ n < 0. +Proof. +intro n; apply -> le_ngt. apply le_0_l. +Qed. + +Theorem nle_succ_0 : forall n : N, ~ (S n <= 0). +Proof. +intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r. +Qed. + +Theorem le_0_r : forall n : N, n <= 0 <-> n == 0. +Proof. +intros n; split; intro H. +le_elim H; [false_hyp H nlt_0_r | assumption]. +now apply eq_le_incl. +Qed. + +Theorem lt_0_succ : forall n : N, 0 < S n. +Proof. +induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r]. +Qed. + +Theorem neq_0_lt_0 : forall n : N, n ~= 0 <-> 0 < n. +Proof. +cases n. +split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. +intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. +Qed. + +Theorem eq_0_gt_0_cases : forall n : N, n == 0 \/ 0 < n. +Proof. +cases n. +now left. +intro; right; apply lt_0_succ. +Qed. + +Theorem zero_one : forall n : N, n == 0 \/ n == 1 \/ 1 < n. +Proof. +induct n. now left. +cases n. intros; right; now left. +intros n IH. destruct IH as [H | [H | H]]. +false_hyp H neq_succ_0. +right; right. rewrite H. apply lt_succ_diag_r. +right; right. now apply lt_lt_succ_r. +Qed. + +Theorem lt_1_r : forall n : N, n < 1 <-> n == 0. +Proof. +cases n. +split; intro; [reflexivity | apply lt_succ_diag_r]. +intros n. rewrite <- succ_lt_mono. +split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0]. +Qed. + +Theorem le_1_r : forall n : N, n <= 1 <-> n == 0 \/ n == 1. +Proof. +cases n. +split; intro; [now left | apply le_succ_diag_r]. +intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. +split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]]. +Qed. + +Theorem lt_lt_0 : forall n m : N, n < m -> 0 < m. +Proof. +intros n m; induct n. +trivial. +intros n IH H. apply IH; now apply lt_succ_l. +Qed. + +Theorem lt_1_l : forall n m p : N, n < m -> m < p -> 1 < p. +Proof. +intros n m p H1 H2. +apply le_lt_trans with m. apply <- le_succ_l. apply le_lt_trans with n. +apply le_0_l. assumption. assumption. +Qed. + +(** Elimination principlies for < and <= for relations *) + +Section RelElim. + +(* FIXME: Variable R : relation N. -- does not work *) + +Variable R : N -> N -> Prop. +Hypothesis R_wd : relation_wd Neq Neq R. + +Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. +Proof. apply R_wd. Qed. + +Theorem le_ind_rel : + (forall m : N, R 0 m) -> + (forall n m : N, n <= m -> R n m -> R (S n) (S m)) -> + forall n m : N, n <= m -> R n m. +Proof. +intros Base Step; induct n. +intros; apply Base. +intros n IH m H. elim H using le_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now apply eq_le_incl. +intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto. +Qed. + +Theorem lt_ind_rel : + (forall m : N, R 0 (S m)) -> + (forall n m : N, n < m -> R n m -> R (S n) (S m)) -> + forall n m : N, n < m -> R n m. +Proof. +intros Base Step; induct n. +intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. +rewrite H; apply Base. +intros n IH m H. elim H using lt_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now apply lt_succ_diag_r. +intros k H1 H2. apply lt_succ_l in H1. auto. +Qed. + +End RelElim. + +(** Predecessor and order *) + +Theorem succ_pred_pos : forall n : N, 0 < n -> S (P n) == n. +Proof. +intros n H; apply succ_pred; intro H1; rewrite H1 in H. +false_hyp H lt_irrefl. +Qed. + +Theorem le_pred_l : forall n : N, P n <= n. +Proof. +cases n. +rewrite pred_0; now apply eq_le_incl. +intros; rewrite pred_succ; apply le_succ_diag_r. +Qed. + +Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n. +Proof. +cases n. +intro H; elimtype False; now apply H. +intros; rewrite pred_succ; apply lt_succ_diag_r. +Qed. + +Theorem le_le_pred : forall n m : N, n <= m -> P n <= m. +Proof. +intros n m H; apply le_trans with n. apply le_pred_l. assumption. +Qed. + +Theorem lt_lt_pred : forall n m : N, n < m -> P n < m. +Proof. +intros n m H; apply le_lt_trans with n. apply le_pred_l. assumption. +Qed. + +Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *) +Proof. +intro n; cases m. +intro H; false_hyp H nlt_0_r. +intros m IH. rewrite pred_succ; now apply -> lt_succ_r. +Qed. + +Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *) +Proof. +intros n m; cases n. +rewrite pred_0; intro H; now apply lt_le_incl. +intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l. +Qed. + +Theorem lt_pred_lt : forall n m : N, n < P m -> n < m. +Proof. +intros n m H; apply lt_le_trans with (P m); [assumption | apply le_pred_l]. +Qed. + +Theorem le_pred_le : forall n m : N, n <= P m -> n <= m. +Proof. +intros n m H; apply le_trans with (P m); [assumption | apply le_pred_l]. +Qed. + +Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *) +Proof. +intros n m H; elim H using le_ind_rel. +solve_relation_wd. +intro; rewrite pred_0; apply le_0_l. +intros p q H1 _; now do 2 rewrite pred_succ. +Qed. + +Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m). +Proof. +intros n m H1; split; intro H2. +assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n. +now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ; +[apply <- succ_lt_mono | | |]. +assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n). +apply lt_le_trans with (P m). assumption. apply le_pred_l. +apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. +Qed. + +Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m. +Proof. +intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ. +Qed. + +Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) +Proof. +intros n m H. apply lt_le_pred. now apply -> le_succ_l. +Qed. + +Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m. (* Converse is false for n == m == 0 *) +Proof. +intros n m H. apply <- lt_succ_r. now apply lt_pred_le. +Qed. + +Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m. +Proof. +intros n m; cases n. +rewrite pred_0. split; intro H; apply le_0_l. +intro n. rewrite pred_succ. apply succ_le_mono. +Qed. + +End NOrderPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v new file mode 100644 index 00000000..031dbdea --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -0,0 +1,133 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NStrongRec.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +(** This file defined the strong (course-of-value, well-founded) recursion +and proves its properties *) + +Require Export NSub. + +Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NSubPropMod := NSubPropFunct NAxiomsMod. +Open Local Scope NatScope. + +Section StrongRecursion. + +Variable A : Set. +Variable Aeq : relation A. + +Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity). + +Hypothesis Aeq_equiv : equiv A Aeq. + +Add Relation A Aeq + reflexivity proved by (proj1 Aeq_equiv) + symmetry proved by (proj2 (proj2 Aeq_equiv)) + transitivity proved by (proj1 (proj2 Aeq_equiv)) +as Aeq_rel. + +Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A := +recursion + (fun _ : N => a) + (fun (m : N) (p : N -> A) (k : N) => f k p) + (S n) + n. + +Theorem strong_rec_wd : +forall a a' : A, a ==A a' -> + forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' -> + forall n n', n == n' -> + strong_rec a f n ==A strong_rec a' f' n'. +Proof. +intros a a' Eaa' f f' Eff' n n' Enn'. +(* First we prove that recursion (which is on type N -> A) returns +extensionally equal functions, and then we use the fact that n == n' *) +assert (H : fun_eq Neq Aeq + (recursion + (fun _ : N => a) + (fun (m : N) (p : N -> A) (k : N) => f k p) + (S n)) + (recursion + (fun _ : N => a') + (fun (m : N) (p : N -> A) (k : N) => f' k p) + (S n'))). +apply recursion_wd with (Aeq := fun_eq Neq Aeq). +unfold fun_eq; now intros. +unfold fun2_eq. intros y y' Eyy' p p' Epp'. unfold fun_eq. auto. +now rewrite Enn'. +unfold strong_rec. +now apply H. +Qed. + +(*Section FixPoint. + +Variable a : A. +Variable f : N -> (N -> A) -> A. + +Hypothesis f_wd : fun2_wd Neq (fun_eq Neq Aeq) Aeq f. + +Let g (n : N) : A := strong_rec a f n. + +Add Morphism g with signature Neq ==> Aeq as g_wd. +Proof. +intros n1 n2 H. unfold g. now apply strong_rec_wd. +Qed. + +Theorem NtoA_eq_symm : symmetric (N -> A) (fun_eq Neq Aeq). +Proof. +apply fun_eq_symm. +exact (proj2 (proj2 NZeq_equiv)). +exact (proj2 (proj2 Aeq_equiv)). +Qed. + +Theorem NtoA_eq_trans : transitive (N -> A) (fun_eq Neq Aeq). +Proof. +apply fun_eq_trans. +exact (proj1 NZeq_equiv). +exact (proj1 (proj2 NZeq_equiv)). +exact (proj1 (proj2 Aeq_equiv)). +Qed. + +Add Relation (N -> A) (fun_eq Neq Aeq) + symmetry proved by NtoA_eq_symm + transitivity proved by NtoA_eq_trans +as NtoA_eq_rel. + +Add Morphism f with signature Neq ==> (fun_eq Neq Aeq) ==> Aeq as f_morph. +Proof. +apply f_wd. +Qed. + +(* We need an assumption saying that for every n, the step function (f n h) +calls h only on the segment [0 ... n - 1]. This means that if h1 and h2 +coincide on values < n, then (f n h1) coincides with (f n h2) *) + +Hypothesis step_good : + forall (n : N) (h1 h2 : N -> A), + (forall m : N, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f n h1) (f n h2). + +(* Todo: +Theorem strong_rec_fixpoint : forall n : N, Aeq (g n) (f n g). +Proof. +apply induction. +unfold predicate_wd, fun_wd. +intros x y H. rewrite H. unfold fun_eq; apply g_wd. +reflexivity. +unfold g, strong_rec. +*) + +End FixPoint.*) +End StrongRecursion. + +Implicit Arguments strong_rec [A]. + +End NStrongRecPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v new file mode 100644 index 00000000..f67689dd --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -0,0 +1,180 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NSub.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NMulOrder. + +Module NSubPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NMulOrderPropMod := NMulOrderPropFunct NAxiomsMod. +Open Local Scope NatScope. + +Theorem sub_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2. +Proof NZsub_wd. + +Theorem sub_0_r : forall n : N, n - 0 == n. +Proof NZsub_0_r. + +Theorem sub_succ_r : forall n m : N, n - (S m) == P (n - m). +Proof NZsub_succ_r. + +Theorem sub_1_r : forall n : N, n - 1 == P n. +Proof. +intro n; rewrite sub_succ_r; now rewrite sub_0_r. +Qed. + +Theorem sub_0_l : forall n : N, 0 - n == 0. +Proof. +induct n. +apply sub_0_r. +intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0. +Qed. + +Theorem sub_succ : forall n m : N, S n - S m == n - m. +Proof. +intro n; induct m. +rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ. +intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r. +Qed. + +Theorem sub_diag : forall n : N, n - n == 0. +Proof. +induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. +Qed. + +Theorem sub_gt : forall n m : N, n > m -> n - m ~= 0. +Proof. +intros n m H; elim H using lt_ind_rel; clear n m H. +solve_relation_wd. +intro; rewrite sub_0_r; apply neq_succ_0. +intros; now rewrite sub_succ. +Qed. + +Theorem add_sub_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p. +Proof. +intros n m p; induct p. +intro; now do 2 rewrite sub_0_r. +intros p IH H. do 2 rewrite sub_succ_r. +rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). +rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l). +reflexivity. +Qed. + +Theorem sub_succ_l : forall n m : N, n <= m -> S m - n == S (m - n). +Proof. +intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)). +symmetry; now apply add_sub_assoc. +Qed. + +Theorem add_sub : forall n m : N, (n + m) - m == n. +Proof. +intros n m. rewrite <- add_sub_assoc by (apply le_refl). +rewrite sub_diag; now rewrite add_0_r. +Qed. + +Theorem sub_add : forall n m : N, n <= m -> (m - n) + n == m. +Proof. +intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption. +rewrite add_comm. apply add_sub. +Qed. + +Theorem add_sub_eq_l : forall n m p : N, m + p == n -> n - m == p. +Proof. +intros n m p H. symmetry. +assert (H1 : m + p - m == n - m) by now rewrite H. +rewrite add_comm in H1. now rewrite add_sub in H1. +Qed. + +Theorem add_sub_eq_r : forall n m p : N, m + p == n -> n - p == m. +Proof. +intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l. +Qed. + +(* This could be proved by adding m to both sides. Then the proof would +use add_sub_assoc and sub_0_le, which is proven below. *) + +Theorem add_sub_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. +Proof. +intros n m p H; double_induct n m. +intros m H1; rewrite sub_0_l in H1. symmetry in H1; false_hyp H1 H. +intro n; rewrite sub_0_r; now rewrite add_0_l. +intros n m IH H1. rewrite sub_succ in H1. apply IH in H1. +rewrite add_succ_l; now rewrite H1. +Qed. + +Theorem sub_add_distr : forall n m p : N, n - (m + p) == (n - m) - p. +Proof. +intros n m; induct p. +rewrite add_0_r; now rewrite sub_0_r. +intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH. +Qed. + +Theorem add_sub_swap : forall n m p : N, p <= n -> n + m - p == n - p + m. +Proof. +intros n m p H. +rewrite (add_comm n m). +rewrite <- add_sub_assoc by assumption. +now rewrite (add_comm m (n - p)). +Qed. + +(** Sub and order *) + +Theorem le_sub_l : forall n m : N, n - m <= n. +Proof. +intro n; induct m. +rewrite sub_0_r; now apply eq_le_incl. +intros m IH. rewrite sub_succ_r. +apply le_trans with (n - m); [apply le_pred_l | assumption]. +Qed. + +Theorem sub_0_le : forall n m : N, n - m == 0 <-> n <= m. +Proof. +double_induct n m. +intro m; split; intro; [apply le_0_l | apply sub_0_l]. +intro m; rewrite sub_0_r; split; intro H; +[false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. +intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ. +Qed. + +(** Sub and mul *) + +Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n. +Proof. +intros n m; cases m. +now rewrite pred_0, mul_0_r, sub_0_l. +intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc. +now rewrite sub_diag, add_0_r. +now apply eq_le_incl. +Qed. + +Theorem mul_sub_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. +Proof. +intros n m p; induct n. +now rewrite sub_0_l, mul_0_l, sub_0_l. +intros n IH. destruct (le_gt_cases m n) as [H | H]. +rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. +rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). +rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. +now apply <- add_cancel_l. +assert (H1 : S n <= m); [now apply <- le_succ_l |]. +setoid_replace (S n - m) with 0 by now apply <- sub_0_le. +setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r). +apply mul_0_l. +Qed. + +Theorem mul_sub_distr_l : forall n m p : N, p * (n - m) == p * n - p * m. +Proof. +intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m). +apply mul_sub_distr_r. +Qed. + +End NSubPropFunct. + diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v new file mode 100644 index 00000000..0574c09f --- /dev/null +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: BigN.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +(** * Natural numbers in base 2^31 *) + +(** +Author: Arnaud Spiwack +*) + +Require Export Int31. +Require Import CyclicAxioms. +Require Import Cyclic31. +Require Import NSig. +Require Import NSigNAxioms. +Require Import NMake. +Require Import NSub. + +Module BigN <: NType := NMake.Make Int31Cyclic. + +(** Module [BigN] implements [NAxiomsSig] *) + +Module Export BigNAxiomsMod := NSig_NAxioms BigN. +Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod. + +(** Notations about [BigN] *) + +Notation bigN := BigN.t. + +Delimit Scope bigN_scope with bigN. +Bind Scope bigN_scope with bigN. +Bind Scope bigN_scope with BigN.t. +Bind Scope bigN_scope with BigN.t_. + +Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *) +Infix "+" := BigN.add : bigN_scope. +Infix "-" := BigN.sub : bigN_scope. +Infix "*" := BigN.mul : bigN_scope. +Infix "/" := BigN.div : bigN_scope. +Infix "?=" := BigN.compare : bigN_scope. +Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. +Infix "<" := BigN.lt : bigN_scope. +Infix "<=" := BigN.le : bigN_scope. +Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. + +Open Scope bigN_scope. + +(** Example of reasoning about [BigN] *) + +Theorem succ_pred: forall q:bigN, + 0 < q -> BigN.succ (BigN.pred q) == q. +Proof. +intros; apply succ_pred. +intro H'; rewrite H' in H; discriminate. +Qed. + +(** [BigN] is a semi-ring *) + +Lemma BigNring : + semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq. +Proof. +constructor. +exact add_0_l. +exact add_comm. +exact add_assoc. +exact mul_1_l. +exact mul_0_l. +exact mul_comm. +exact mul_assoc. +exact mul_add_distr_r. +Qed. + +Add Ring BigNr : BigNring. + +(** Todo: tactic translating from [BigN] to [Z] + omega *) + +(** Todo: micromega *) diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml new file mode 100644 index 00000000..bd0fb5b1 --- /dev/null +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -0,0 +1,3166 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NMake_gen.ml 11136 2008-06-18 10:41:34Z herbelin $ i*) + +(*S NMake_gen.ml : this file generates NMake.v *) + + +(*s The two parameters that control the generation: *) + +let size = 6 (* how many times should we repeat the Z/nZ --> Z/2nZ + process before relying on a generic construct *) +let gen_proof = true (* should we generate proofs ? *) + + +(*s Some utilities *) + +let t = "t" +let c = "N" +let pz n = if n == 0 then "w_0" else "W0" +let rec gen2 n = if n == 0 then "1" else if n == 1 then "2" + else "2 * " ^ (gen2 (n - 1)) +let rec genxO n s = + if n == 0 then s else " (xO" ^ (genxO (n - 1) s) ^ ")" + +(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to + /dev/null, but for being compatible with earlier ocaml and not + relying on system-dependent stuff like open_out "/dev/null", + let's use instead a magical hack *) + +(* Standard printer, with a final newline *) +let pr s = Printf.printf (s^^"\n") +(* Printing to /dev/null *) +let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) + : ('a, out_channel, unit) format -> 'a) +(* Proof printer : prints iff gen_proof is true *) +let pp = if gen_proof then pr else pn +(* Printer for admitted parts : prints iff gen_proof is false *) +let pa = if not gen_proof then pr else pn +(* Same as before, but without the final newline *) +let pr0 = Printf.printf +let pp0 = if gen_proof then pr0 else pn + + +(*s The actual printing *) + +let _ = + + pr "(************************************************************************)"; + pr "(* v * The Coq Proof Assistant / The Coq Development Team *)"; + pr "(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)"; + pr "(* \\VV/ **************************************************************)"; + pr "(* // * This file is distributed under the terms of the *)"; + pr "(* * GNU Lesser General Public License Version 2.1 *)"; + pr "(************************************************************************)"; + pr "(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)"; + pr "(************************************************************************)"; + pr ""; + pr "(** * NMake *)"; + pr ""; + pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)"; + pr ""; + pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)"; + pr ""; + pr "Require Import BigNumPrelude."; + pr "Require Import ZArith."; + pr "Require Import CyclicAxioms."; + pr "Require Import DoubleType."; + pr "Require Import DoubleMul."; + pr "Require Import DoubleDivn1."; + pr "Require Import DoubleCyclic."; + pr "Require Import Nbasic."; + pr "Require Import Wf_nat."; + pr "Require Import StreamMemo."; + pr "Require Import NSig."; + pr ""; + pr "Module Make (Import W0:CyclicType) <: NType."; + pr ""; + + pr " Definition w0 := W0.w."; + for i = 1 to size do + pr " Definition w%i := zn2z w%i." i (i-1) + done; + pr ""; + + pr " Definition w0_op := W0.w_op."; + for i = 1 to 3 do + pr " Definition w%i_op := mk_zn2z_op w%i_op." i (i-1) + done; + for i = 4 to size + 3 do + pr " Definition w%i_op := mk_zn2z_op_karatsuba w%i_op." i (i-1) + done; + pr ""; + + pr " Section Make_op."; + pr " Variable mk : forall w', znz_op w' -> znz_op (zn2z w')."; + pr ""; + pr " Fixpoint make_op_aux (n:nat) : znz_op (word w%i (S n)):=" size; + pr " match n return znz_op (word w%i (S n)) with" size; + pr " | O => w%i_op" (size+1); + pr " | S n1 =>"; + pr " match n1 return znz_op (word w%i (S (S n1))) with" size; + pr " | O => w%i_op" (size+2); + pr " | S n2 =>"; + pr " match n2 return znz_op (word w%i (S (S (S n2)))) with" size; + pr " | O => w%i_op" (size+3); + pr " | S n3 => mk _ (mk _ (mk _ (make_op_aux n3)))"; + pr " end"; + pr " end"; + pr " end."; + pr ""; + pr " End Make_op."; + pr ""; + pr " Definition omake_op := make_op_aux mk_zn2z_op_karatsuba."; + pr ""; + pr ""; + pr " Definition make_op_list := dmemo_list _ omake_op."; + pr ""; + pr " Definition make_op n := dmemo_get _ omake_op n make_op_list."; + pr ""; + pr " Lemma make_op_omake: forall n, make_op n = omake_op n."; + pr " intros n; unfold make_op, make_op_list."; + pr " refine (dmemo_get_correct _ _ _)."; + pr " Qed."; + pr ""; + + pr " Inductive %s_ :=" t; + for i = 0 to size do + pr " | %s%i : w%i -> %s_" c i i t + done; + pr " | %sn : forall n, word w%i (S n) -> %s_." c size t; + pr ""; + pr " Definition %s := %s_." t t; + pr ""; + + pr " Definition w_0 := w0_op.(znz_0)."; + pr ""; + + for i = 0 to size do + pr " Definition one%i := w%i_op.(znz_1)." i i + done; + pr ""; + + + pr " Definition zero := %s0 w_0." c; + pr " Definition one := %s0 one0." c; + pr ""; + + pr " Definition to_Z x :="; + pr " match x with"; + for i = 0 to size do + pr " | %s%i wx => w%i_op.(znz_to_Z) wx" c i i + done; + pr " | %sn n wx => (make_op n).(znz_to_Z) wx" c; + pr " end."; + pr ""; + + pr " Open Scope Z_scope."; + pr " Notation \"[ x ]\" := (to_Z x)."; + pr ""; + + pr " Definition to_N x := Zabs_N (to_Z x)."; + pr ""; + + pr " Definition eq x y := (to_Z x = to_Z y)."; + pr ""; + + pp " (* Regular make op (no karatsuba) *)"; + pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : "; + pp " znz_op (word ww n) :="; + pp " match n return znz_op (word ww n) with "; + pp " O => ww_op"; + pp " | S n1 => mk_zn2z_op (nmake_op ww ww_op n1) "; + pp " end."; + pp ""; + pp " (* Simplification by rewriting for nmake_op *)"; + pp " Theorem nmake_op_S: forall ww (w_op: znz_op ww) x, "; + pp " nmake_op _ w_op (S x) = mk_zn2z_op (nmake_op _ w_op x)."; + pp " auto."; + pp " Qed."; + pp ""; + + + pr " (* Eval and extend functions for each level *)"; + for i = 0 to size do + pp " Let nmake_op%i := nmake_op _ w%i_op." i i; + pp " Let eval%in n := znz_to_Z (nmake_op%i n)." i i; + if i == 0 then + pr " Let extend%i := DoubleBase.extend (WW w_0)." i + else + pr " Let extend%i := DoubleBase.extend (WW (W0: w%i))." i i; + done; + pr ""; + + + pp " Theorem digits_doubled:forall n ww (w_op: znz_op ww), "; + pp " znz_digits (nmake_op _ w_op n) = "; + pp " DoubleBase.double_digits (znz_digits w_op) n."; + pp " Proof."; + pp " intros n; elim n; auto; clear n."; + pp " intros n Hrec ww ww_op; simpl DoubleBase.double_digits."; + pp " rewrite <- Hrec; auto."; + pp " Qed."; + pp ""; + pp " Theorem nmake_double: forall n ww (w_op: znz_op ww), "; + pp " znz_to_Z (nmake_op _ w_op n) ="; + pp " @DoubleBase.double_to_Z _ (znz_digits w_op) (znz_to_Z w_op) n."; + pp " Proof."; + pp " intros n; elim n; auto; clear n."; + pp " intros n Hrec ww ww_op; simpl DoubleBase.double_to_Z; unfold zn2z_to_Z."; + pp " rewrite <- Hrec; auto."; + pp " unfold DoubleBase.double_wB; rewrite <- digits_doubled; auto."; + pp " Qed."; + pp ""; + + + pp " Theorem digits_nmake:forall n ww (w_op: znz_op ww), "; + pp " znz_digits (nmake_op _ w_op (S n)) = "; + pp " xO (znz_digits (nmake_op _ w_op n))."; + pp " Proof."; + pp " auto."; + pp " Qed."; + pp ""; + + + pp " Theorem znz_nmake_op: forall ww ww_op n xh xl,"; + pp " znz_to_Z (nmake_op ww ww_op (S n)) (WW xh xl) ="; + pp " znz_to_Z (nmake_op ww ww_op n) xh *"; + pp " base (znz_digits (nmake_op ww ww_op n)) +"; + pp " znz_to_Z (nmake_op ww ww_op n) xl."; + pp " Proof."; + pp " auto."; + pp " Qed."; + pp ""; + + pp " Theorem make_op_S: forall n,"; + pp " make_op (S n) = mk_zn2z_op_karatsuba (make_op n)."; + pp " intro n."; + pp " do 2 rewrite make_op_omake."; + pp " pattern n; apply lt_wf_ind; clear n."; + pp " intros n; case n; clear n."; + pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 2); + pp " intros n; case n; clear n."; + pp " intros _; unfold omake_op, make_op_aux, w%i_op; apply refl_equal." (size + 3); + pp " intros n; case n; clear n."; + pp " intros _; unfold omake_op, make_op_aux, w%i_op, w%i_op; apply refl_equal." (size + 3) (size + 2); + pp " intros n Hrec."; + pp " change (omake_op (S (S (S (S n))))) with"; + pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op (S n)))))."; + pp " change (omake_op (S (S (S n)))) with"; + pp " (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (mk_zn2z_op_karatsuba (omake_op n))))."; + pp " rewrite Hrec; auto with arith."; + pp " Qed."; + pp " "; + + + for i = 1 to size + 2 do + pp " Let znz_to_Z_%i: forall x y," i; + pp " znz_to_Z w%i_op (WW x y) = " i; + pp " znz_to_Z w%i_op x * base (znz_digits w%i_op) + znz_to_Z w%i_op y." (i-1) (i-1) (i-1); + pp " Proof."; + pp " auto."; + pp " Qed. "; + pp ""; + done; + + pp " Let znz_to_Z_n: forall n x y,"; + pp " znz_to_Z (make_op (S n)) (WW x y) = "; + pp " znz_to_Z (make_op n) x * base (znz_digits (make_op n)) + znz_to_Z (make_op n) y."; + pp " Proof."; + pp " intros n x y; rewrite make_op_S; auto."; + pp " Qed. "; + pp ""; + + pp " Let w0_spec: znz_spec w0_op := W0.w_spec."; + for i = 1 to 3 do + pp " Let w%i_spec: znz_spec w%i_op := mk_znz2_spec w%i_spec." i i (i-1) + done; + for i = 4 to size + 3 do + pp " Let w%i_spec : znz_spec w%i_op := mk_znz2_karatsuba_spec w%i_spec." i i (i-1) + done; + pp ""; + + pp " Let wn_spec: forall n, znz_spec (make_op n)."; + pp " intros n; elim n; clear n."; + pp " exact w%i_spec." (size + 1); + pp " intros n Hrec; rewrite make_op_S."; + pp " exact (mk_znz2_karatsuba_spec Hrec)."; + pp " Qed."; + pp ""; + + for i = 0 to size do + pr " Definition w%i_eq0 := w%i_op.(znz_eq0)." i i; + pr " Let spec_w%i_eq0: forall x, if w%i_eq0 x then [%s%i x] = 0 else True." i i c i; + pa " Admitted."; + pp " Proof."; + pp " intros x; unfold w%i_eq0, to_Z; generalize (spec_eq0 w%i_spec x);" i i; + pp " case znz_eq0; auto."; + pp " Qed."; + pr ""; + done; + pr ""; + + + for i = 0 to size do + pp " Theorem digits_w%i: znz_digits w%i_op = znz_digits (nmake_op _ w0_op %i)." i i i; + if i == 0 then + pp " auto." + else + pp " rewrite digits_nmake; rewrite <- digits_w%i; auto." (i - 1); + pp " Qed."; + pp ""; + pp " Let spec_double_eval%in: forall n, eval%in n = DoubleBase.double_to_Z (znz_digits w%i_op) (znz_to_Z w%i_op) n." i i i i; + pp " Proof."; + pp " intros n; exact (nmake_double n w%i w%i_op)." i i; + pp " Qed."; + pp ""; + done; + + for i = 0 to size do + for j = 0 to (size - i) do + pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i j (i + j) i j; + pp " Proof."; + if j == 0 then + if i == 0 then + pp " auto." + else + begin + pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1); + pp " auto."; + pp " unfold nmake_op; auto."; + end + else + begin + pp " apply trans_equal with (xO (znz_digits w%i_op))." (i + j -1); + pp " auto."; + pp " rewrite digits_nmake."; + pp " rewrite digits_w%in%i." i (j - 1); + pp " auto."; + end; + pp " Qed."; + pp ""; + pp " Let spec_eval%in%i: forall x, [%s%i x] = eval%in %i x." i j c (i + j) i j; + pp " Proof."; + if j == 0 then + pp " intros x; rewrite spec_double_eval%in; unfold DoubleBase.double_to_Z, to_Z; auto." i + else + begin + pp " intros x; case x."; + pp " auto."; + pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (i + j); + pp " rewrite digits_w%in%i." i (j - 1); + pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (j - 1); + pp " unfold eval%in, nmake_op%i." i i; + pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (j - 1); + end; + pp " Qed."; + if i + j <> size then + begin + pp " Let spec_extend%in%i: forall x, [%s%i x] = [%s%i (extend%i %i x)]." i (i + j + 1) c i c (i + j + 1) i j; + if j == 0 then + begin + pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." i (i + j); + pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1); + pp " rewrite (spec_0 w%i_spec); auto." (i + j); + end + else + begin + pp " intros x; change (extend%i %i x) with (WW (znz_0 w%i_op) (extend%i %i x))." i j (i + j) i (j - 1); + pp " unfold to_Z; rewrite znz_to_Z_%i." (i + j + 1); + pp " rewrite (spec_0 w%i_spec)." (i + j); + pp " generalize (spec_extend%in%i x); unfold to_Z." i (i + j); + pp " intros HH; rewrite <- HH; auto."; + end; + pp " Qed."; + pp ""; + end; + done; + + pp " Theorem digits_w%in%i: znz_digits w%i_op = znz_digits (nmake_op _ w%i_op %i)." i (size - i + 1) (size + 1) i (size - i + 1); + pp " Proof."; + pp " apply trans_equal with (xO (znz_digits w%i_op))." size; + pp " auto."; + pp " rewrite digits_nmake."; + pp " rewrite digits_w%in%i." i (size - i); + pp " auto."; + pp " Qed."; + pp ""; + + pp " Let spec_eval%in%i: forall x, [%sn 0 x] = eval%in %i x." i (size - i + 1) c i (size - i + 1); + pp " Proof."; + pp " intros x; case x."; + pp " auto."; + pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 1); + pp " rewrite digits_w%in%i." i (size - i); + pp " generalize (spec_eval%in%i); unfold to_Z; intros HH; repeat rewrite HH." i (size - i); + pp " unfold eval%in, nmake_op%i." i i; + pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size - i); + pp " Qed."; + pp ""; + + pp " Let spec_eval%in%i: forall x, [%sn 1 x] = eval%in %i x." i (size - i + 2) c i (size - i + 2); + pp " intros x; case x."; + pp " auto."; + pp " intros xh xl; unfold to_Z; rewrite znz_to_Z_%i." (size + 2); + pp " rewrite digits_w%in%i." i (size + 1 - i); + pp " generalize (spec_eval%in%i); unfold to_Z; change (make_op 0) with (w%i_op); intros HH; repeat rewrite HH." i (size + 1 - i) (size + 1); + pp " unfold eval%in, nmake_op%i." i i; + pp " rewrite (znz_nmake_op _ w%i_op %i); auto." i (size + 1 - i); + pp " Qed."; + pp ""; + done; + + pp " Let digits_w%in: forall n," size; + pp " znz_digits (make_op n) = znz_digits (nmake_op _ w%i_op (S n))." size; + pp " intros n; elim n; clear n."; + pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; + pp " rewrite nmake_op_S; apply sym_equal; auto."; + pp " intros n Hrec."; + pp " replace (znz_digits (make_op (S n))) with (xO (znz_digits (make_op n)))."; + pp " rewrite Hrec."; + pp " rewrite nmake_op_S; apply sym_equal; auto."; + pp " rewrite make_op_S; apply sym_equal; auto."; + pp " Qed."; + pp ""; + + pp " Let spec_eval%in: forall n x, [%sn n x] = eval%in (S n) x." size c size; + pp " intros n; elim n; clear n."; + pp " exact spec_eval%in1." size; + pp " intros n Hrec x; case x; clear x."; + pp " unfold to_Z, eval%in, nmake_op%i." size size; + pp " rewrite make_op_S; rewrite nmake_op_S; auto."; + pp " intros xh xl."; + pp " unfold to_Z in Hrec |- *."; + pp " rewrite znz_to_Z_n."; + pp " rewrite digits_w%in." size; + pp " repeat rewrite Hrec."; + pp " unfold eval%in, nmake_op%i." size size; + pp " apply sym_equal; rewrite nmake_op_S; auto."; + pp " Qed."; + pp ""; + + pp " Let spec_extend%in: forall n x, [%s%i x] = [%sn n (extend%i n x)]." size c size c size ; + pp " intros n; elim n; clear n."; + pp " intros x; change (extend%i 0 x) with (WW (znz_0 w%i_op) x)." size size; + pp " unfold to_Z."; + pp " change (make_op 0) with w%i_op." (size + 1); + pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto." (size + 1) size; + pp " intros n Hrec x."; + pp " change (extend%i (S n) x) with (WW W0 (extend%i n x))." size size; + pp " unfold to_Z in Hrec |- *; rewrite znz_to_Z_n; auto."; + pp " rewrite <- Hrec."; + pp " replace (znz_to_Z (make_op n) W0) with 0; auto."; + pp " case n; auto; intros; rewrite make_op_S; auto."; + pp " Qed."; + pp ""; + + pr " Theorem spec_pos: forall x, 0 <= [x]."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; clear x."; + for i = 0 to size do + pp " intros x; case (spec_to_Z w%i_spec x); auto." i; + done; + pp " intros n x; case (spec_to_Z (wn_spec n) x); auto."; + pp " Qed."; + pr ""; + + pp " Let spec_extendn_0: forall n wx, [%sn n (extend n _ wx)] = [%sn 0 wx]." c c; + pp " intros n; elim n; auto."; + pp " intros n1 Hrec wx; simpl extend; rewrite <- Hrec; auto."; + pp " unfold to_Z."; + pp " case n1; auto; intros n2; repeat rewrite make_op_S; auto."; + pp " Qed."; + pp " Hint Rewrite spec_extendn_0: extr."; + pp ""; + pp " Let spec_extendn0_0: forall n wx, [%sn (S n) (WW W0 wx)] = [%sn n wx]." c c; + pp " Proof."; + pp " intros n x; unfold to_Z."; + pp " rewrite znz_to_Z_n."; + pp " rewrite <- (Zplus_0_l (znz_to_Z (make_op n) x))."; + pp " apply (f_equal2 Zplus); auto."; + pp " case n; auto."; + pp " intros n1; rewrite make_op_S; auto."; + pp " Qed."; + pp " Hint Rewrite spec_extendn_0: extr."; + pp ""; + pp " Let spec_extend_tr: forall m n (w: word _ (S n)),"; + pp " [%sn (m + n) (extend_tr w m)] = [%sn n w]." c c; + pp " Proof."; + pp " induction m; auto."; + pp " intros n x; simpl extend_tr."; + pp " simpl plus; rewrite spec_extendn0_0; auto."; + pp " Qed."; + pp " Hint Rewrite spec_extend_tr: extr."; + pp ""; + pp " Let spec_cast_l: forall n m x1,"; + pp " [%sn (Max.max n m)" c; + pp " (castm (diff_r n m) (extend_tr x1 (snd (diff n m))))] ="; + pp " [%sn n x1]." c; + pp " Proof."; + pp " intros n m x1; case (diff_r n m); simpl castm."; + pp " rewrite spec_extend_tr; auto."; + pp " Qed."; + pp " Hint Rewrite spec_cast_l: extr."; + pp ""; + pp " Let spec_cast_r: forall n m x1,"; + pp " [%sn (Max.max n m)" c; + pp " (castm (diff_l n m) (extend_tr x1 (fst (diff n m))))] ="; + pp " [%sn m x1]." c; + pp " Proof."; + pp " intros n m x1; case (diff_l n m); simpl castm."; + pp " rewrite spec_extend_tr; auto."; + pp " Qed."; + pp " Hint Rewrite spec_cast_r: extr."; + pp ""; + + + pr " Section LevelAndIter."; + pr ""; + pr " Variable res: Type."; + pr " Variable xxx: res."; + pr " Variable P: Z -> Z -> res -> Prop."; + pr " (* Abstraction function for each level *)"; + for i = 0 to size do + pr " Variable f%i: w%i -> w%i -> res." i i i; + pr " Variable f%in: forall n, w%i -> word w%i (S n) -> res." i i i; + pr " Variable fn%i: forall n, word w%i (S n) -> w%i -> res." i i i; + pp " Variable Pf%i: forall x y, P [%s%i x] [%s%i y] (f%i x y)." i c i c i i; + if i == size then + begin + pp " Variable Pf%in: forall n x y, P [%s%i x] (eval%in (S n) y) (f%in n x y)." i c i i i; + pp " Variable Pfn%i: forall n x y, P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i i c i i; + end + else + begin + pp " Variable Pf%in: forall n x y, Z_of_nat n <= %i -> P [%s%i x] (eval%in (S n) y) (f%in n x y)." i (size - i) c i i i; + pp " Variable Pfn%i: forall n x y, Z_of_nat n <= %i -> P (eval%in (S n) x) [%s%i y] (fn%i n x y)." i (size - i) i c i i; + end; + pr ""; + done; + pr " Variable fnn: forall n, word w%i (S n) -> word w%i (S n) -> res." size size; + pp " Variable Pfnn: forall n x y, P [%sn n x] [%sn n y] (fnn n x y)." c c; + pr " Variable fnm: forall n m, word w%i (S n) -> word w%i (S m) -> res." size size; + pp " Variable Pfnm: forall n m x y, P [%sn n x] [%sn m y] (fnm n m x y)." c c; + pr ""; + pr " (* Special zero functions *)"; + pr " Variable f0t: t_ -> res."; + pp " Variable Pf0t: forall x, P 0 [x] (f0t x)."; + pr " Variable ft0: t_ -> res."; + pp " Variable Pft0: forall x, P [x] 0 (ft0 x)."; + pr ""; + + + pr " (* We level the two arguments before applying *)"; + pr " (* the functions at each leval *)"; + pr " Definition same_level (x y: t_): res :="; + pr0 " Eval lazy zeta beta iota delta ["; + for i = 0 to size do + pr0 "extend%i " i; + done; + pr ""; + pr " DoubleBase.extend DoubleBase.extend_aux"; + pr " ] in"; + pr " match x, y with"; + for i = 0 to size do + for j = 0 to i - 1 do + pr " | %s%i wx, %s%i wy => f%i wx (extend%i %i wy)" c i c j i j (i - j -1); + done; + pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i; + for j = i + 1 to size do + pr " | %s%i wx, %s%i wy => f%i (extend%i %i wx) wy" c i c j j i (j - i - 1); + done; + if i == size then + pr " | %s%i wx, %sn m wy => fnn m (extend%i m wx) wy" c size c size + else + pr " | %s%i wx, %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c i c size i (size - i - 1); + done; + for i = 0 to size do + if i == size then + pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n wy)" c c size size + else + pr " | %sn n wx, %s%i wy => fnn n wx (extend%i n (extend%i %i wy))" c c i size i (size - i - 1); + done; + pr " | %sn n wx, Nn m wy =>" c; + pr " let mn := Max.max n m in"; + pr " let d := diff n m in"; + pr " fnn mn"; + pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; + pr " (castm (diff_l n m) (extend_tr wy (fst d)))"; + pr " end."; + pr ""; + + pp " Lemma spec_same_level: forall x y, P [x] [y] (same_level x y)."; + pp " Proof."; + pp " intros x; case x; clear x; unfold same_level."; + for i = 0 to size do + pp " intros x y; case y; clear y."; + for j = 0 to i - 1 do + pp " intros y; rewrite spec_extend%in%i; apply Pf%i." j i i; + done; + pp " intros y; apply Pf%i." i; + for j = i + 1 to size do + pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j; + done; + if i == size then + pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size + else + pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size; + done; + pp " intros n x y; case y; clear y."; + for i = 0 to size do + if i == size then + pp " intros y; rewrite (spec_extend%in n); apply Pfnn." size + else + pp " intros y; rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; + done; + pp " intros m y; rewrite <- (spec_cast_l n m x); "; + pp " rewrite <- (spec_cast_r n m y); apply Pfnn."; + pp " Qed."; + pp ""; + + pr " (* We level the two arguments before applying *)"; + pr " (* the functions at each level (special zero case) *)"; + pr " Definition same_level0 (x y: t_): res :="; + pr0 " Eval lazy zeta beta iota delta ["; + for i = 0 to size do + pr0 "extend%i " i; + done; + pr ""; + pr " DoubleBase.extend DoubleBase.extend_aux"; + pr " ] in"; + pr " match x with"; + for i = 0 to size do + pr " | %s%i wx =>" c i; + if i == 0 then + pr " if w0_eq0 wx then f0t y else"; + pr " match y with"; + for j = 0 to i - 1 do + pr " | %s%i wy =>" c j; + if j == 0 then + pr " if w0_eq0 wy then ft0 x else"; + pr " f%i wx (extend%i %i wy)" i j (i - j -1); + done; + pr " | %s%i wy => f%i wx wy" c i i; + for j = i + 1 to size do + pr " | %s%i wy => f%i (extend%i %i wx) wy" c j j i (j - i - 1); + done; + if i == size then + pr " | %sn m wy => fnn m (extend%i m wx) wy" c size + else + pr " | %sn m wy => fnn m (extend%i m (extend%i %i wx)) wy" c size i (size - i - 1); + pr" end"; + done; + pr " | %sn n wx =>" c; + pr " match y with"; + for i = 0 to size do + pr " | %s%i wy =>" c i; + if i == 0 then + pr " if w0_eq0 wy then ft0 x else"; + if i == size then + pr " fnn n wx (extend%i n wy)" size + else + pr " fnn n wx (extend%i n (extend%i %i wy))" size i (size - i - 1); + done; + pr " | %sn m wy =>" c; + pr " let mn := Max.max n m in"; + pr " let d := diff n m in"; + pr " fnn mn"; + pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; + pr " (castm (diff_l n m) (extend_tr wy (fst d)))"; + pr " end"; + pr " end."; + pr ""; + + pp " Lemma spec_same_level0: forall x y, P [x] [y] (same_level0 x y)."; + pp " Proof."; + pp " intros x; case x; clear x; unfold same_level0."; + for i = 0 to size do + pp " intros x."; + if i == 0 then + begin + pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H."; + pp " intros y; rewrite H; apply Pf0t."; + pp " clear H."; + end; + pp " intros y; case y; clear y."; + for j = 0 to i - 1 do + pp " intros y."; + if j == 0 then + begin + pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; + pp " rewrite H; apply Pft0."; + pp " clear H."; + end; + pp " rewrite spec_extend%in%i; apply Pf%i." j i i; + done; + pp " intros y; apply Pf%i." i; + for j = i + 1 to size do + pp " intros y; rewrite spec_extend%in%i; apply Pf%i." i j j; + done; + if i == size then + pp " intros m y; rewrite (spec_extend%in m); apply Pfnn." size + else + pp " intros m y; rewrite spec_extend%in%i; rewrite (spec_extend%in m); apply Pfnn." i size size; + done; + pp " intros n x y; case y; clear y."; + for i = 0 to size do + pp " intros y."; + if i = 0 then + begin + pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; + pp " rewrite H; apply Pft0."; + pp " clear H."; + end; + if i == size then + pp " rewrite (spec_extend%in n); apply Pfnn." size + else + pp " rewrite spec_extend%in%i; rewrite (spec_extend%in n); apply Pfnn." i size size; + done; + pp " intros m y; rewrite <- (spec_cast_l n m x); "; + pp " rewrite <- (spec_cast_r n m y); apply Pfnn."; + pp " Qed."; + pp ""; + + pr " (* We iter the smaller argument with the bigger *)"; + pr " Definition iter (x y: t_): res := "; + pr0 " Eval lazy zeta beta iota delta ["; + for i = 0 to size do + pr0 "extend%i " i; + done; + pr ""; + pr " DoubleBase.extend DoubleBase.extend_aux"; + pr " ] in"; + pr " match x, y with"; + for i = 0 to size do + for j = 0 to i - 1 do + pr " | %s%i wx, %s%i wy => fn%i %i wx wy" c i c j j (i - j - 1); + done; + pr " | %s%i wx, %s%i wy => f%i wx wy" c i c i i; + for j = i + 1 to size do + pr " | %s%i wx, %s%i wy => f%in %i wx wy" c i c j i (j - i - 1); + done; + if i == size then + pr " | %s%i wx, %sn m wy => f%in m wx wy" c size c size + else + pr " | %s%i wx, %sn m wy => f%in m (extend%i %i wx) wy" c i c size i (size - i - 1); + done; + for i = 0 to size do + if i == size then + pr " | %sn n wx, %s%i wy => fn%i n wx wy" c c size size + else + pr " | %sn n wx, %s%i wy => fn%i n wx (extend%i %i wy)" c c i size i (size - i - 1); + done; + pr " | %sn n wx, %sn m wy => fnm n m wx wy" c c; + pr " end."; + pr ""; + + pp " Ltac zg_tac := try"; + pp " (red; simpl Zcompare; auto;"; + pp " let t := fresh \"H\" in (intros t; discriminate t))."; + pp " Lemma spec_iter: forall x y, P [x] [y] (iter x y)."; + pp " Proof."; + pp " intros x; case x; clear x; unfold iter."; + for i = 0 to size do + pp " intros x y; case y; clear y."; + for j = 0 to i - 1 do + pp " intros y; rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1); + done; + pp " intros y; apply Pf%i." i; + for j = i + 1 to size do + pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1); + done; + if i == size then + pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size + else + pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size; + done; + pp " intros n x y; case y; clear y."; + for i = 0 to size do + if i == size then + pp " intros y; rewrite spec_eval%in; apply Pfn%i." size size + else + pp " intros y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size; + done; + pp " intros m y; apply Pfnm."; + pp " Qed."; + pp ""; + + + pr " (* We iter the smaller argument with the bigger (zero case) *)"; + pr " Definition iter0 (x y: t_): res :="; + pr0 " Eval lazy zeta beta iota delta ["; + for i = 0 to size do + pr0 "extend%i " i; + done; + pr ""; + pr " DoubleBase.extend DoubleBase.extend_aux"; + pr " ] in"; + pr " match x with"; + for i = 0 to size do + pr " | %s%i wx =>" c i; + if i == 0 then + pr " if w0_eq0 wx then f0t y else"; + pr " match y with"; + for j = 0 to i - 1 do + pr " | %s%i wy =>" c j; + if j == 0 then + pr " if w0_eq0 wy then ft0 x else"; + pr " fn%i %i wx wy" j (i - j - 1); + done; + pr " | %s%i wy => f%i wx wy" c i i; + for j = i + 1 to size do + pr " | %s%i wy => f%in %i wx wy" c j i (j - i - 1); + done; + if i == size then + pr " | %sn m wy => f%in m wx wy" c size + else + pr " | %sn m wy => f%in m (extend%i %i wx) wy" c size i (size - i - 1); + pr " end"; + done; + pr " | %sn n wx =>" c; + pr " match y with"; + for i = 0 to size do + pr " | %s%i wy =>" c i; + if i == 0 then + pr " if w0_eq0 wy then ft0 x else"; + if i == size then + pr " fn%i n wx wy" size + else + pr " fn%i n wx (extend%i %i wy)" size i (size - i - 1); + done; + pr " | %sn m wy => fnm n m wx wy" c; + pr " end"; + pr " end."; + pr ""; + + pp " Lemma spec_iter0: forall x y, P [x] [y] (iter0 x y)."; + pp " Proof."; + pp " intros x; case x; clear x; unfold iter0."; + for i = 0 to size do + pp " intros x."; + if i == 0 then + begin + pp " generalize (spec_w0_eq0 x); case w0_eq0; intros H."; + pp " intros y; rewrite H; apply Pf0t."; + pp " clear H."; + end; + pp " intros y; case y; clear y."; + for j = 0 to i - 1 do + pp " intros y."; + if j == 0 then + begin + pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; + pp " rewrite H; apply Pft0."; + pp " clear H."; + end; + pp " rewrite spec_eval%in%i; apply (Pfn%i %i); zg_tac." j (i - j) j (i - j - 1); + done; + pp " intros y; apply Pf%i." i; + for j = i + 1 to size do + pp " intros y; rewrite spec_eval%in%i; apply (Pf%in %i); zg_tac." i (j - i) i (j - i - 1); + done; + if i == size then + pp " intros m y; rewrite spec_eval%in; apply Pf%in." size size + else + pp " intros m y; rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pf%in." i size size size; + done; + pp " intros n x y; case y; clear y."; + for i = 0 to size do + pp " intros y."; + if i = 0 then + begin + pp " generalize (spec_w0_eq0 y); case w0_eq0; intros H."; + pp " rewrite H; apply Pft0."; + pp " clear H."; + end; + if i == size then + pp " rewrite spec_eval%in; apply Pfn%i." size size + else + pp " rewrite spec_extend%in%i; rewrite spec_eval%in; apply Pfn%i." i size size size; + done; + pp " intros m y; apply Pfnm."; + pp " Qed."; + pp ""; + + + pr " End LevelAndIter."; + pr ""; + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Reduction *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + pr " Definition reduce_0 (x:w) := %s0 x." c; + pr " Definition reduce_1 :="; + pr " Eval lazy beta iota delta[reduce_n1] in"; + pr " reduce_n1 _ _ zero w0_eq0 %s0 %s1." c c; + for i = 2 to size do + pr " Definition reduce_%i :=" i; + pr " Eval lazy beta iota delta[reduce_n1] in"; + pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i %s%i." + (i-1) (i-1) c i + done; + pr " Definition reduce_%i :=" (size+1); + pr " Eval lazy beta iota delta[reduce_n1] in"; + pr " reduce_n1 _ _ zero w%i_eq0 reduce_%i (%sn 0)." + size size c; + + pr " Definition reduce_n n := "; + pr " Eval lazy beta iota delta[reduce_n] in"; + pr " reduce_n _ _ zero reduce_%i %sn n." (size + 1) c; + pr ""; + + pp " Let spec_reduce_0: forall x, [reduce_0 x] = [%s0 x]." c; + pp " Proof."; + pp " intros x; unfold to_Z, reduce_0."; + pp " auto."; + pp " Qed."; + pp " "; + + for i = 1 to size + 1 do + if i == size + 1 then + pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%sn 0 x]." i i c + else + pp " Let spec_reduce_%i: forall x, [reduce_%i x] = [%s%i x]." i i c i; + pp " Proof."; + pp " intros x; case x; unfold reduce_%i." i; + pp " exact (spec_0 w0_spec)."; + pp " intros x1 y1."; + pp " generalize (spec_w%i_eq0 x1); " (i - 1); + pp " case w%i_eq0; intros H1; auto." (i - 1); + if i <> 1 then + pp " rewrite spec_reduce_%i." (i - 1); + pp " unfold to_Z; rewrite znz_to_Z_%i." i; + pp " unfold to_Z in H1; rewrite H1; auto."; + pp " Qed."; + pp " "; + done; + + pp " Let spec_reduce_n: forall n x, [reduce_n n x] = [%sn n x]." c; + pp " Proof."; + pp " intros n; elim n; simpl reduce_n."; + pp " intros x; rewrite <- spec_reduce_%i; auto." (size + 1); + pp " intros n1 Hrec x; case x."; + pp " unfold to_Z; rewrite make_op_S; auto."; + pp " exact (spec_0 w0_spec)."; + pp " intros x1 y1; case x1; auto."; + pp " rewrite Hrec."; + pp " rewrite spec_extendn0_0; auto."; + pp " Qed."; + pp " "; + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Successor *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_succ_c := w%i_op.(znz_succ_c)." i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_succ := w%i_op.(znz_succ)." i i + done; + pr ""; + + pr " Definition succ x :="; + pr " match x with"; + for i = 0 to size-1 do + pr " | %s%i wx =>" c i; + pr " match w%i_succ_c wx with" i; + pr " | C0 r => %s%i r" c i; + pr " | C1 r => %s%i (WW one%i r)" c (i+1) i; + pr " end"; + done; + pr " | %s%i wx =>" c size; + pr " match w%i_succ_c wx with" size; + pr " | C0 r => %s%i r" c size; + pr " | C1 r => %sn 0 (WW one%i r)" c size ; + pr " end"; + pr " | %sn n wx =>" c; + pr " let op := make_op n in"; + pr " match op.(znz_succ_c) wx with"; + pr " | C0 r => %sn n r" c; + pr " | C1 r => %sn (S n) (WW op.(znz_1) r)" c; + pr " end"; + pr " end."; + pr ""; + + pr " Theorem spec_succ: forall n, [succ n] = [n] + 1."; + pa " Admitted."; + pp " Proof."; + pp " intros n; case n; unfold succ, to_Z."; + for i = 0 to size do + pp " intros n1; generalize (spec_succ_c w%i_spec n1);" i; + pp " unfold succ, to_Z, w%i_succ_c; case znz_succ_c; auto." i; + pp " intros ww H; rewrite <- H."; + pp " (rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1); + pp " apply f_equal2 with (f := Zplus); auto;"; + pp " apply f_equal2 with (f := Zmult); auto;"; + pp " exact (spec_1 w%i_spec))." i; + done; + pp " intros k n1; generalize (spec_succ_c (wn_spec k) n1)."; + pp " unfold succ, to_Z; case znz_succ_c; auto."; + pp " intros ww H; rewrite <- H."; + pp " (rewrite (znz_to_Z_n k); unfold interp_carry;"; + pp " apply f_equal2 with (f := Zplus); auto;"; + pp " apply f_equal2 with (f := Zmult); auto;"; + pp " exact (spec_1 (wn_spec k)))."; + pp " Qed."; + pr ""; + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Adddition *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_add_c := znz_add_c w%i_op." i i; + pr " Definition w%i_add x y :=" i; + pr " match w%i_add_c x y with" i; + pr " | C0 r => %s%i r" c i; + if i == size then + pr " | C1 r => %sn 0 (WW one%i r)" c size + else + pr " | C1 r => %s%i (WW one%i r)" c (i + 1) i; + pr " end."; + pr ""; + done ; + pr " Definition addn n (x y : word w%i (S n)) :=" size; + pr " let op := make_op n in"; + pr " match op.(znz_add_c) x y with"; + pr " | C0 r => %sn n r" c; + pr " | C1 r => %sn (S n) (WW op.(znz_1) r) end." c; + pr ""; + + + for i = 0 to size do + pp " Let spec_w%i_add: forall x y, [w%i_add x y] = [%s%i x] + [%s%i y]." i i c i c i; + pp " Proof."; + pp " intros n m; unfold to_Z, w%i_add, w%i_add_c." i i; + pp " generalize (spec_add_c w%i_spec n m); case znz_add_c; auto." i; + pp " intros ww H; rewrite <- H."; + pp " rewrite znz_to_Z_%i; unfold interp_carry;" (i + 1); + pp " apply f_equal2 with (f := Zplus); auto;"; + pp " apply f_equal2 with (f := Zmult); auto;"; + pp " exact (spec_1 w%i_spec)." i; + pp " Qed."; + pp " Hint Rewrite spec_w%i_add: addr." i; + pp ""; + done; + pp " Let spec_wn_add: forall n x y, [addn n x y] = [%sn n x] + [%sn n y]." c c; + pp " Proof."; + pp " intros k n m; unfold to_Z, addn."; + pp " generalize (spec_add_c (wn_spec k) n m); case znz_add_c; auto."; + pp " intros ww H; rewrite <- H."; + pp " rewrite (znz_to_Z_n k); unfold interp_carry;"; + pp " apply f_equal2 with (f := Zplus); auto;"; + pp " apply f_equal2 with (f := Zmult); auto;"; + pp " exact (spec_1 (wn_spec k))."; + pp " Qed."; + pp " Hint Rewrite spec_wn_add: addr."; + + pr " Definition add := Eval lazy beta delta [same_level] in"; + pr0 " (same_level t_ "; + for i = 0 to size do + pr0 "w%i_add " i; + done; + pr "addn)."; + pr ""; + + pr " Theorem spec_add: forall x y, [add x y] = [x] + [y]."; + pa " Admitted."; + pp " Proof."; + pp " unfold add."; + pp " generalize (spec_same_level t_ (fun x y res => [res] = x + y))."; + pp " unfold same_level; intros HH; apply HH; clear HH."; + for i = 0 to size do + pp " exact spec_w%i_add." i; + done; + pp " exact spec_wn_add."; + pp " Qed."; + pr ""; + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Predecessor *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_pred_c := w%i_op.(znz_pred_c)." i i + done; + pr ""; + + pr " Definition pred x :="; + pr " match x with"; + for i = 0 to size do + pr " | %s%i wx =>" c i; + pr " match w%i_pred_c wx with" i; + pr " | C0 r => reduce_%i r" i; + pr " | C1 r => zero"; + pr " end"; + done; + pr " | %sn n wx =>" c; + pr " let op := make_op n in"; + pr " match op.(znz_pred_c) wx with"; + pr " | C0 r => reduce_n n r"; + pr " | C1 r => zero"; + pr " end"; + pr " end."; + pr ""; + + pr " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; unfold pred."; + for i = 0 to size do + pp " intros x1 H1; unfold w%i_pred_c; " i; + pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i; + pp " rewrite spec_reduce_%i; auto." i; + pp " unfold interp_carry; unfold to_Z."; + pp " case (spec_to_Z w%i_spec x1); intros HH1 HH2." i; + pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4 HH5." i; + pp " assert (znz_to_Z w%i_op x1 - 1 < 0); auto with zarith." i; + pp " unfold to_Z in H1; auto with zarith."; + done; + pp " intros n x1 H1; "; + pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1."; + pp " rewrite spec_reduce_n; auto."; + pp " unfold interp_carry; unfold to_Z."; + pp " case (spec_to_Z (wn_spec n) x1); intros HH1 HH2."; + pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4 HH5."; + pp " assert (znz_to_Z (make_op n) x1 - 1 < 0); auto with zarith."; + pp " unfold to_Z in H1; auto with zarith."; + pp " Qed."; + pp " "; + + pp " Let spec_pred0: forall x, [x] = 0 -> [pred x] = 0."; + pp " Proof."; + pp " intros x; case x; unfold pred."; + for i = 0 to size do + pp " intros x1 H1; unfold w%i_pred_c; " i; + pp " generalize (spec_pred_c w%i_spec x1); case znz_pred_c; intros y1." i; + pp " unfold interp_carry; unfold to_Z."; + pp " unfold to_Z in H1; auto with zarith."; + pp " case (spec_to_Z w%i_spec y1); intros HH3 HH4; auto with zarith." i; + pp " intros; exact (spec_0 w0_spec)."; + done; + pp " intros n x1 H1; "; + pp " generalize (spec_pred_c (wn_spec n) x1); case znz_pred_c; intros y1."; + pp " unfold interp_carry; unfold to_Z."; + pp " unfold to_Z in H1; auto with zarith."; + pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith."; + pp " intros; exact (spec_0 w0_spec)."; + pp " Qed."; + pr " "; + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Subtraction *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_sub_c := w%i_op.(znz_sub_c)." i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_sub x y :=" i; + pr " match w%i_sub_c x y with" i; + pr " | C0 r => reduce_%i r" i; + pr " | C1 r => zero"; + pr " end." + done; + pr ""; + + pr " Definition subn n (x y : word w%i (S n)) :=" size; + pr " let op := make_op n in"; + pr " match op.(znz_sub_c) x y with"; + pr " | C0 r => %sn n r" c; + pr " | C1 r => N0 w_0"; + pr " end."; + pr ""; + + for i = 0 to size do + pp " Let spec_w%i_sub: forall x y, [%s%i y] <= [%s%i x] -> [w%i_sub x y] = [%s%i x] - [%s%i y]." i c i c i i c i c i; + pp " Proof."; + pp " intros n m; unfold w%i_sub, w%i_sub_c." i i; + pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i; + if i == 0 then + pp " intros x; auto." + else + pp " intros x; try rewrite spec_reduce_%i; auto." i; + pp " unfold interp_carry; unfold zero, w_0, to_Z."; + pp " rewrite (spec_0 w0_spec)."; + pp " case (spec_to_Z w%i_spec x); intros; auto with zarith." i; + pp " Qed."; + pp ""; + done; + + pp " Let spec_wn_sub: forall n x y, [%sn n y] <= [%sn n x] -> [subn n x y] = [%sn n x] - [%sn n y]." c c c c; + pp " Proof."; + pp " intros k n m; unfold subn."; + pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; "; + pp " intros x; auto."; + pp " unfold interp_carry, to_Z."; + pp " case (spec_to_Z (wn_spec k) x); intros; auto with zarith."; + pp " Qed."; + pp ""; + + pr " Definition sub := Eval lazy beta delta [same_level] in"; + pr0 " (same_level t_ "; + for i = 0 to size do + pr0 "w%i_sub " i; + done; + pr "subn)."; + pr ""; + + pr " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y]."; + pa " Admitted."; + pp " Proof."; + pp " unfold sub."; + pp " generalize (spec_same_level t_ (fun x y res => y <= x -> [res] = x - y))."; + pp " unfold same_level; intros HH; apply HH; clear HH."; + for i = 0 to size do + pp " exact spec_w%i_sub." i; + done; + pp " exact spec_wn_sub."; + pp " Qed."; + pr ""; + + for i = 0 to size do + pp " Let spec_w%i_sub0: forall x y, [%s%i x] < [%s%i y] -> [w%i_sub x y] = 0." i c i c i i; + pp " Proof."; + pp " intros n m; unfold w%i_sub, w%i_sub_c." i i; + pp " generalize (spec_sub_c w%i_spec n m); case znz_sub_c; " i; + pp " intros x; unfold interp_carry."; + pp " unfold to_Z; case (spec_to_Z w%i_spec x); intros; auto with zarith." i; + pp " intros; unfold to_Z, zero, w_0; rewrite (spec_0 w0_spec); auto."; + pp " Qed."; + pp ""; + done; + + pp " Let spec_wn_sub0: forall n x y, [%sn n x] < [%sn n y] -> [subn n x y] = 0." c c; + pp " Proof."; + pp " intros k n m; unfold subn."; + pp " generalize (spec_sub_c (wn_spec k) n m); case znz_sub_c; "; + pp " intros x; unfold interp_carry."; + pp " unfold to_Z; case (spec_to_Z (wn_spec k) x); intros; auto with zarith."; + pp " intros; unfold to_Z, w_0; rewrite (spec_0 (w0_spec)); auto."; + pp " Qed."; + pp ""; + + pr " Theorem spec_sub0: forall x y, [x] < [y] -> [sub x y] = 0."; + pa " Admitted."; + pp " Proof."; + pp " unfold sub."; + pp " generalize (spec_same_level t_ (fun x y res => x < y -> [res] = 0))."; + pp " unfold same_level; intros HH; apply HH; clear HH."; + for i = 0 to size do + pp " exact spec_w%i_sub0." i; + done; + pp " exact spec_wn_sub0."; + pp " Qed."; + pr ""; + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Comparison *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition compare_%i := w%i_op.(znz_compare)." i i; + pr " Definition comparen_%i :=" i; + pr " compare_mn_1 w%i w%i %s compare_%i (compare_%i %s) compare_%i." i i (pz i) i i (pz i) i + done; + pr ""; + + pr " Definition comparenm n m wx wy :="; + pr " let mn := Max.max n m in"; + pr " let d := diff n m in"; + pr " let op := make_op mn in"; + pr " op.(znz_compare)"; + pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; + pr " (castm (diff_l n m) (extend_tr wy (fst d)))."; + pr ""; + + pr " Definition compare := Eval lazy beta delta [iter] in "; + pr " (iter _ "; + for i = 0 to size do + pr " compare_%i" i; + pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pr " (fun n => comparen_%i (S n))" i; + done; + pr " comparenm)."; + pr ""; + + pr " Definition lt n m := compare n m = Lt."; + pr " Definition le n m := compare n m <> Gt."; + pr " Definition min n m := match compare n m with Gt => m | _ => n end."; + pr " Definition max n m := match compare n m with Lt => m | _ => n end."; + pr ""; + + for i = 0 to size do + pp " Let spec_compare_%i: forall x y," i; + pp " match compare_%i x y with " i; + pp " Eq => [%s%i x] = [%s%i y]" c i c i; + pp " | Lt => [%s%i x] < [%s%i y]" c i c i; + pp " | Gt => [%s%i x] > [%s%i y]" c i c i; + pp " end."; + pp " Proof."; + pp " unfold compare_%i, to_Z; exact (spec_compare w%i_spec)." i i; + pp " Qed."; + pp ""; + + pp " Let spec_comparen_%i:" i; + pp " forall (n : nat) (x : word w%i n) (y : w%i)," i i; + pp " match comparen_%i n x y with" i; + pp " | Eq => eval%in n x = [%s%i y]" i c i; + pp " | Lt => eval%in n x < [%s%i y]" i c i; + pp " | Gt => eval%in n x > [%s%i y]" i c i; + pp " end."; + pp " intros n x y."; + pp " unfold comparen_%i, to_Z; rewrite spec_double_eval%in." i i; + pp " apply spec_compare_mn_1."; + pp " exact (spec_0 w%i_spec)." i; + pp " intros x1; exact (spec_compare w%i_spec %s x1)." i (pz i); + pp " exact (spec_to_Z w%i_spec)." i; + pp " exact (spec_compare w%i_spec)." i; + pp " exact (spec_compare w%i_spec)." i; + pp " exact (spec_to_Z w%i_spec)." i; + pp " Qed."; + pp ""; + done; + + pp " Let spec_opp_compare: forall c (u v: Z),"; + pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->"; + pp " match opp_compare c with Eq => v = u | Lt => v < u | Gt => v > u end."; + pp " Proof."; + pp " intros c u v; case c; unfold opp_compare; auto with zarith."; + pp " Qed."; + pp ""; + + + pr " Theorem spec_compare: forall x y,"; + pr " match compare x y with "; + pr " Eq => [x] = [y]"; + pr " | Lt => [x] < [y]"; + pr " | Gt => [x] > [y]"; + pr " end."; + pa " Admitted."; + pp " Proof."; + pp " refine (spec_iter _ (fun x y res => "; + pp " match res with "; + pp " Eq => x = y"; + pp " | Lt => x < y"; + pp " | Gt => x > y"; + pp " end)"; + for i = 0 to size do + pp " compare_%i" i; + pp " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pp " (fun n => comparen_%i (S n)) _ _ _" i; + done; + pp " comparenm _)."; + + for i = 0 to size - 1 do + pp " exact spec_compare_%i." i; + pp " intros n x y H;apply spec_opp_compare; apply spec_comparen_%i." i; + pp " intros n x y H; exact (spec_comparen_%i (S n) x y)." i; + done; + pp " exact spec_compare_%i." size; + pp " intros n x y;apply spec_opp_compare; apply spec_comparen_%i." size; + pp " intros n; exact (spec_comparen_%i (S n))." size; + pp " intros n m x y; unfold comparenm."; + pp " rewrite <- (spec_cast_l n m x); rewrite <- (spec_cast_r n m y)."; + pp " unfold to_Z; apply (spec_compare (wn_spec (Max.max n m)))."; + pp " Qed."; + pr ""; + + pr " Definition eq_bool x y :="; + pr " match compare x y with"; + pr " | Eq => true"; + pr " | _ => false"; + pr " end."; + pr ""; + + + pr " Theorem spec_eq_bool: forall x y,"; + pr " if eq_bool x y then [x] = [y] else [x] <> [y]."; + pa " Admitted."; + pp " Proof."; + pp " intros x y; unfold eq_bool."; + pp " generalize (spec_compare x y); case compare; auto with zarith."; + pp " Qed."; + pr ""; + + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Multiplication *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_mul_c := w%i_op.(znz_mul_c)." i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_mul_add :=" i; + pr " Eval lazy beta delta [w_mul_add] in"; + pr " @w_mul_add w%i %s w%i_succ w%i_add_c w%i_mul_c." i (pz i) i i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_0W := znz_0W w%i_op." i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_WW := znz_WW w%i_op." i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_mul_add_n1 :=" i; + pr " @double_mul_add_n1 w%i %s w%i_WW w%i_0W w%i_mul_add." i (pz i) i i i + done; + pr ""; + + for i = 0 to size - 1 do + pr " Let to_Z%i n :=" i; + pr " match n return word w%i (S n) -> t_ with" i; + for j = 0 to size - i do + if (i + j) == size then + begin + pr " | %i%s => fun x => %sn 0 x" j "%nat" c; + pr " | %i%s => fun x => %sn 1 x" (j + 1) "%nat" c + end + else + pr " | %i%s => fun x => %s%i x" j "%nat" c (i + j + 1) + done; + pr " | _ => fun _ => N0 w_0"; + pr " end."; + pr ""; + done; + + + for i = 0 to size - 1 do + pp "Theorem to_Z%i_spec:" i; + pp " forall n x, Z_of_nat n <= %i -> [to_Z%i n x] = znz_to_Z (nmake_op _ w%i_op (S n)) x." (size + 1 - i) i i; + for j = 1 to size + 2 - i do + pp " intros n; case n; clear n."; + pp " unfold to_Z%i." i; + pp " intros x H; rewrite spec_eval%in%i; auto." i j; + done; + pp " intros n x."; + pp " repeat rewrite inj_S; unfold Zsucc; auto with zarith."; + pp " Qed."; + pp ""; + done; + + + for i = 0 to size do + pr " Definition w%i_mul n x y :=" i; + pr " let (w,r) := w%i_mul_add_n1 (S n) x y %s in" i (pz i); + if i == size then + begin + pr " if w%i_eq0 w then %sn n r" i c; + pr " else %sn (S n) (WW (extend%i n w) r)." c i; + end + else + begin + pr " if w%i_eq0 w then to_Z%i n r" i i; + pr " else to_Z%i (S n) (WW (extend%i n w) r)." i i; + end; + pr ""; + done; + + pr " Definition mulnm n m x y :="; + pr " let mn := Max.max n m in"; + pr " let d := diff n m in"; + pr " let op := make_op mn in"; + pr " reduce_n (S mn) (op.(znz_mul_c)"; + pr " (castm (diff_r n m) (extend_tr x (snd d)))"; + pr " (castm (diff_l n m) (extend_tr y (fst d))))."; + pr ""; + + pr " Definition mul := Eval lazy beta delta [iter0] in "; + pr " (iter0 t_ "; + for i = 0 to size do + pr " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i; + pr " (fun n x y => w%i_mul n y x)" i; + pr " w%i_mul" i; + done; + pr " mulnm"; + pr " (fun _ => N0 w_0)"; + pr " (fun _ => N0 w_0)"; + pr " )."; + pr ""; + for i = 0 to size do + pp " Let spec_w%i_mul_add: forall x y z," i; + pp " let (q,r) := w%i_mul_add x y z in" i; + pp " znz_to_Z w%i_op q * (base (znz_digits w%i_op)) + znz_to_Z w%i_op r =" i i i; + pp " znz_to_Z w%i_op x * znz_to_Z w%i_op y + znz_to_Z w%i_op z :=" i i i ; + pp " (spec_mul_add w%i_spec)." i; + pp ""; + done; + + for i = 0 to size do + pp " Theorem spec_w%i_mul_add_n1: forall n x y z," i; + pp " let (q,r) := w%i_mul_add_n1 n x y z in" i; + pp " znz_to_Z w%i_op q * (base (znz_digits (nmake_op _ w%i_op n))) +" i i; + pp " znz_to_Z (nmake_op _ w%i_op n) r =" i; + pp " znz_to_Z (nmake_op _ w%i_op n) x * znz_to_Z w%i_op y +" i i; + pp " znz_to_Z w%i_op z." i; + pp " Proof."; + pp " intros n x y z; unfold w%i_mul_add_n1." i; + pp " rewrite nmake_double."; + pp " rewrite digits_doubled."; + pp " change (base (DoubleBase.double_digits (znz_digits w%i_op) n)) with" i; + pp " (DoubleBase.double_wB (znz_digits w%i_op) n)." i; + pp " apply spec_double_mul_add_n1; auto."; + if i == 0 then pp " exact (spec_0 w%i_spec)." i; + pp " exact (spec_WW w%i_spec)." i; + pp " exact (spec_0W w%i_spec)." i; + pp " exact (spec_mul_add w%i_spec)." i; + pp " Qed."; + pp ""; + done; + + pp " Lemma nmake_op_WW: forall ww ww1 n x y,"; + pp " znz_to_Z (nmake_op ww ww1 (S n)) (WW x y) ="; + pp " znz_to_Z (nmake_op ww ww1 n) x * base (znz_digits (nmake_op ww ww1 n)) +"; + pp " znz_to_Z (nmake_op ww ww1 n) y."; + pp " auto."; + pp " Qed."; + pp ""; + + for i = 0 to size do + pp " Lemma extend%in_spec: forall n x1," i; + pp " znz_to_Z (nmake_op _ w%i_op (S n)) (extend%i n x1) = " i i; + pp " znz_to_Z w%i_op x1." i; + pp " Proof."; + pp " intros n1 x2; rewrite nmake_double."; + pp " unfold extend%i." i; + pp " rewrite DoubleBase.spec_extend; auto."; + if i == 0 then + pp " intros l; simpl; unfold w_0; rewrite (spec_0 w0_spec); ring."; + pp " Qed."; + pp ""; + done; + + pp " Lemma spec_muln:"; + pp " forall n (x: word _ (S n)) y,"; + pp " [%sn (S n) (znz_mul_c (make_op n) x y)] = [%sn n x] * [%sn n y]." c c c; + pp " Proof."; + pp " intros n x y; unfold to_Z."; + pp " rewrite <- (spec_mul_c (wn_spec n))."; + pp " rewrite make_op_S."; + pp " case znz_mul_c; auto."; + pp " Qed."; + + pr " Theorem spec_mul: forall x y, [mul x y] = [x] * [y]."; + pa " Admitted."; + pp " Proof."; + for i = 0 to size do + pp " assert(F%i: " i; + pp " forall n x y,"; + if i <> size then + pp0 " Z_of_nat n <= %i -> " (size - i); + pp " [w%i_mul n x y] = eval%in (S n) x * [%s%i y])." i i c i; + if i == size then + pp " intros n x y; unfold w%i_mul." i + else + pp " intros n x y H; unfold w%i_mul." i; + pp " generalize (spec_w%i_mul_add_n1 (S n) x y %s)." i (pz i); + pp " case w%i_mul_add_n1; intros x1 y1." i; + pp " change (znz_to_Z (nmake_op _ w%i_op (S n)) x) with (eval%in (S n) x)." i i; + pp " change (znz_to_Z w%i_op y) with ([%s%i y])." i c i; + if i == 0 then + pp " unfold w_0; rewrite (spec_0 w0_spec); rewrite Zplus_0_r." + else + pp " change (znz_to_Z w%i_op W0) with 0; rewrite Zplus_0_r." i; + pp " intros H1; rewrite <- H1; clear H1."; + pp " generalize (spec_w%i_eq0 x1); case w%i_eq0; intros HH." i i; + pp " unfold to_Z in HH; rewrite HH."; + if i == size then + begin + pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i; auto." i i i; + pp " rewrite spec_eval%in; unfold eval%in, nmake_op%i." i i i + end + else + begin + pp " rewrite to_Z%i_spec; auto with zarith." i; + pp " rewrite to_Z%i_spec; try (rewrite inj_S; auto with zarith)." i + end; + pp " rewrite nmake_op_WW; rewrite extend%in_spec; auto." i; + done; + pp " refine (spec_iter0 t_ (fun x y res => [res] = x * y)"; + for i = 0 to size do + pp " (fun x y => reduce_%i (w%i_mul_c x y)) " (i + 1) i; + pp " (fun n x y => w%i_mul n y x)" i; + pp " w%i_mul _ _ _" i; + done; + pp " mulnm _"; + pp " (fun _ => N0 w_0) _"; + pp " (fun _ => N0 w_0) _"; + pp " )."; + for i = 0 to size do + pp " intros x y; rewrite spec_reduce_%i." (i + 1); + pp " unfold w%i_mul_c, to_Z." i; + pp " generalize (spec_mul_c w%i_spec x y)." i; + pp " intros HH; rewrite <- HH; clear HH; auto."; + if i == size then + begin + pp " intros n x y; rewrite F%i; auto with zarith." i; + pp " intros n x y; rewrite F%i; auto with zarith. " i; + end + else + begin + pp " intros n x y H; rewrite F%i; auto with zarith." i; + pp " intros n x y H; rewrite F%i; auto with zarith. " i; + end; + done; + pp " intros n m x y; unfold mulnm."; + pp " rewrite spec_reduce_n."; + pp " rewrite <- (spec_cast_l n m x)."; + pp " rewrite <- (spec_cast_r n m y)."; + pp " rewrite spec_muln; rewrite spec_cast_l; rewrite spec_cast_r; auto."; + pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring."; + pp " intros x; unfold to_Z, w_0; rewrite (spec_0 w0_spec); ring."; + pp " Qed."; + pr ""; + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Square *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_square_c := w%i_op.(znz_square_c)." i i + done; + pr ""; + + pr " Definition square x :="; + pr " match x with"; + pr " | %s0 wx => reduce_1 (w0_square_c wx)" c; + for i = 1 to size - 1 do + pr " | %s%i wx => %s%i (w%i_square_c wx)" c i c (i+1) i + done; + pr " | %s%i wx => %sn 0 (w%i_square_c wx)" c size c size; + pr " | %sn n wx =>" c; + pr " let op := make_op n in"; + pr " %sn (S n) (op.(znz_square_c) wx)" c; + pr " end."; + pr ""; + + pr " Theorem spec_square: forall x, [square x] = [x] * [x]."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; unfold square; clear x."; + pp " intros x; rewrite spec_reduce_1; unfold to_Z."; + pp " exact (spec_square_c w%i_spec x)." 0; + for i = 1 to size do + pp " intros x; unfold to_Z."; + pp " exact (spec_square_c w%i_spec x)." i; + done; + pp " intros n x; unfold to_Z."; + pp " rewrite make_op_S."; + pp " exact (spec_square_c (wn_spec n) x)."; + pp "Qed."; + pr ""; + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Power *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + pr " Fixpoint power_pos (x:%s) (p:positive) {struct p} : %s :=" t t; + pr " match p with"; + pr " | xH => x"; + pr " | xO p => square (power_pos x p)"; + pr " | xI p => mul (square (power_pos x p)) x"; + pr " end."; + pr ""; + + pr " Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n."; + pa " Admitted."; + pp " Proof."; + pp " intros x n; generalize x; elim n; clear n x; simpl power_pos."; + pp " intros; rewrite spec_mul; rewrite spec_square; rewrite H."; + pp " rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith."; + pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith."; + pp " rewrite Zpower_2; rewrite Zpower_1_r; auto."; + pp " intros; rewrite spec_square; rewrite H."; + pp " rewrite Zpos_xO; auto with zarith."; + pp " rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith."; + pp " rewrite Zpower_2; auto."; + pp " intros; rewrite Zpower_1_r; auto."; + pp " Qed."; + pp ""; + pr ""; + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Square root *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_sqrt := w%i_op.(znz_sqrt)." i i + done; + pr ""; + + pr " Definition sqrt x :="; + pr " match x with"; + for i = 0 to size do + pr " | %s%i wx => reduce_%i (w%i_sqrt wx)" c i i i; + done; + pr " | %sn n wx =>" c; + pr " let op := make_op n in"; + pr " reduce_n n (op.(znz_sqrt) wx)"; + pr " end."; + pr ""; + + pr " Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2."; + pa " Admitted."; + pp " Proof."; + pp " intros x; unfold sqrt; case x; clear x."; + for i = 0 to size do + pp " intros x; rewrite spec_reduce_%i; exact (spec_sqrt w%i_spec x)." i i; + done; + pp " intros n x; rewrite spec_reduce_n; exact (spec_sqrt (wn_spec n) x)."; + pp " Qed."; + pr ""; + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Division *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_div_gt := w%i_op.(znz_div_gt)." i i + done; + pr ""; + + pp " Let spec_divn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; + pp " (spec_double_divn1 "; + pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; + pp " (znz_WW ww_op) ww_op.(znz_head0)"; + pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; + pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; + pp " (spec_to_Z ww_spec) "; + pp " (spec_zdigits ww_spec)"; + pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; + pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) "; + pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; + pp ""; + + for i = 0 to size do + pr " Definition w%i_divn1 n x y :=" i; + pr " let (u, v) :="; + pr " double_divn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; + pr " (znz_WW w%i_op) w%i_op.(znz_head0)" i i; + pr " w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i; + pr " w%i_op.(znz_compare) w%i_op.(znz_sub) (S n) x y in" i i; + if i == size then + pr " (%sn _ u, %s%i v)." c c i + else + pr " (to_Z%i _ u, %s%i v)." i c i; + done; + pr ""; + + for i = 0 to size do + pp " Lemma spec_get_end%i: forall n x y," i; + pp " eval%in n x <= [%s%i y] -> " i c i; + pp " [%s%i (DoubleBase.get_low %s n x)] = eval%in n x." c i (pz i) i; + pp " Proof."; + pp " intros n x y H."; + pp " rewrite spec_double_eval%in; unfold to_Z." i; + pp " apply DoubleBase.spec_get_low."; + pp " exact (spec_0 w%i_spec)." i; + pp " exact (spec_to_Z w%i_spec)." i; + pp " apply Zle_lt_trans with [%s%i y]; auto." c i; + pp " rewrite <- spec_double_eval%in; auto." i; + pp " unfold to_Z; case (spec_to_Z w%i_spec y); auto." i; + pp " Qed."; + pp ""; + done; + + for i = 0 to size do + pr " Let div_gt%i x y := let (u,v) := (w%i_div_gt x y) in (reduce_%i u, reduce_%i v)." i i i i; + done; + pr ""; + + + pr " Let div_gtnm n m wx wy :="; + pr " let mn := Max.max n m in"; + pr " let d := diff n m in"; + pr " let op := make_op mn in"; + pr " let (q, r):= op.(znz_div_gt)"; + pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; + pr " (castm (diff_l n m) (extend_tr wy (fst d))) in"; + pr " (reduce_n mn q, reduce_n mn r)."; + pr ""; + + pr " Definition div_gt := Eval lazy beta delta [iter] in"; + pr " (iter _ "; + for i = 0 to size do + pr " div_gt%i" i; + pr " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); + pr " w%i_divn1" i; + done; + pr " div_gtnm)."; + pr ""; + + pr " Theorem spec_div_gt: forall x y,"; + pr " [x] > [y] -> 0 < [y] ->"; + pr " let (q,r) := div_gt x y in"; + pr " [q] = [x] / [y] /\\ [r] = [x] mod [y]."; + pa " Admitted."; + pp " Proof."; + pp " assert (FO:"; + pp " forall x y, [x] > [y] -> 0 < [y] ->"; + pp " let (q,r) := div_gt x y in"; + pp " [x] = [q] * [y] + [r] /\\ 0 <= [r] < [y])."; + pp " refine (spec_iter (t_*t_) (fun x y res => x > y -> 0 < y ->"; + pp " let (q,r) := res in"; + pp " x = [q] * y + [r] /\\ 0 <= [r] < y)"; + for i = 0 to size do + pp " div_gt%i" i; + pp " (fun n x y => div_gt%i x (DoubleBase.get_low %s (S n) y))" i (pz i); + pp " w%i_divn1 _ _ _" i; + done; + pp " div_gtnm _)."; + for i = 0 to size do + pp " intros x y H1 H2; unfold div_gt%i, w%i_div_gt." i i; + pp " generalize (spec_div_gt w%i_spec x y H1 H2); case znz_div_gt." i; + pp " intros xx yy; repeat rewrite spec_reduce_%i; auto." i; + if i == size then + pp " intros n x y H2 H3; unfold div_gt%i, w%i_div_gt." i i + else + pp " intros n x y H1 H2 H3; unfold div_gt%i, w%i_div_gt." i i; + pp " generalize (spec_div_gt w%i_spec x " i; + pp " (DoubleBase.get_low %s (S n) y))." (pz i); + pp0 " "; + for j = 0 to i do + pp0 "unfold w%i; " (i-j); + done; + pp "case znz_div_gt."; + pp " intros xx yy H4; repeat rewrite spec_reduce_%i." i; + pp " generalize (spec_get_end%i (S n) y x); unfold to_Z; intros H5." i; + pp " unfold to_Z in H2; rewrite H5 in H4; auto with zarith."; + if i == size then + pp " intros n x y H2 H3." + else + pp " intros n x y H1 H2 H3."; + pp " generalize"; + pp " (spec_divn1 w%i w%i_op w%i_spec (S n) x y H3)." i i i; + pp0 " unfold w%i_divn1; " i; + for j = 0 to i do + pp0 "unfold w%i; " (i-j); + done; + pp "case double_divn1."; + pp " intros xx yy H4."; + if i == size then + begin + pp " repeat rewrite <- spec_double_eval%in in H4; auto." i; + pp " rewrite spec_eval%in; auto." i; + end + else + begin + pp " rewrite to_Z%i_spec; auto with zarith." i; + pp " repeat rewrite <- spec_double_eval%in in H4; auto." i; + end; + done; + pp " intros n m x y H1 H2; unfold div_gtnm."; + pp " generalize (spec_div_gt (wn_spec (Max.max n m))"; + pp " (castm (diff_r n m)"; + pp " (extend_tr x (snd (diff n m))))"; + pp " (castm (diff_l n m)"; + pp " (extend_tr y (fst (diff n m)))))."; + pp " case znz_div_gt."; + pp " intros xx yy HH."; + pp " repeat rewrite spec_reduce_n."; + pp " rewrite <- (spec_cast_l n m x)."; + pp " rewrite <- (spec_cast_r n m y)."; + pp " unfold to_Z; apply HH."; + pp " rewrite <- (spec_cast_l n m x) in H1; auto."; + pp " rewrite <- (spec_cast_r n m y) in H1; auto."; + pp " rewrite <- (spec_cast_r n m y) in H2; auto."; + pp " intros x y H1 H2; generalize (FO x y H1 H2); case div_gt."; + pp " intros q r (H3, H4); split."; + pp " apply (Zdiv_unique [x] [y] [q] [r]); auto."; + pp " rewrite Zmult_comm; auto."; + pp " apply (Zmod_unique [x] [y] [q] [r]); auto."; + pp " rewrite Zmult_comm; auto."; + pp " Qed."; + pr ""; + + pr " Definition div_eucl x y :="; + pr " match compare x y with"; + pr " | Eq => (one, zero)"; + pr " | Lt => (zero, x)"; + pr " | Gt => div_gt x y"; + pr " end."; + pr ""; + + pr " Theorem spec_div_eucl: forall x y,"; + pr " 0 < [y] ->"; + pr " let (q,r) := div_eucl x y in"; + pr " ([q], [r]) = Zdiv_eucl [x] [y]."; + pa " Admitted."; + pp " Proof."; + pp " assert (F0: [zero] = 0)."; + pp " exact (spec_0 w0_spec)."; + pp " assert (F1: [one] = 1)."; + pp " exact (spec_1 w0_spec)."; + pp " intros x y H; generalize (spec_compare x y);"; + pp " unfold div_eucl; case compare; try rewrite F0;"; + pp " try rewrite F1; intros; auto with zarith."; + pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))"; + pp " (Z_mod_same [y] (Zlt_gt _ _ H));"; + pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto."; + pp " assert (F2: 0 <= [x] < [y])."; + pp " generalize (spec_pos x); auto."; + pp " generalize (Zdiv_small _ _ F2)"; + pp " (Zmod_small _ _ F2);"; + pp " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto."; + pp " generalize (spec_div_gt _ _ H0 H); auto."; + pp " unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt."; + pp " intros a b c d (H1, H2); subst; auto."; + pp " Qed."; + pr ""; + + pr " Definition div x y := fst (div_eucl x y)."; + pr ""; + + pr " Theorem spec_div:"; + pr " forall x y, 0 < [y] -> [div x y] = [x] / [y]."; + pa " Admitted."; + pp " Proof."; + pp " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);"; + pp " case div_eucl; simpl fst."; + pp " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; "; + pp " injection H; auto."; + pp " Qed."; + pr ""; + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Modulo *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + for i = 0 to size do + pr " Definition w%i_mod_gt := w%i_op.(znz_mod_gt)." i i + done; + pr ""; + + for i = 0 to size do + pr " Definition w%i_modn1 :=" i; + pr " double_modn1 w%i_op.(znz_zdigits) w%i_op.(znz_0)" i i; + pr " w%i_op.(znz_head0) w%i_op.(znz_add_mul_div) w%i_op.(znz_div21)" i i i; + pr " w%i_op.(znz_compare) w%i_op.(znz_sub)." i i; + done; + pr ""; + + pr " Let mod_gtnm n m wx wy :="; + pr " let mn := Max.max n m in"; + pr " let d := diff n m in"; + pr " let op := make_op mn in"; + pr " reduce_n mn (op.(znz_mod_gt)"; + pr " (castm (diff_r n m) (extend_tr wx (snd d)))"; + pr " (castm (diff_l n m) (extend_tr wy (fst d))))."; + pr ""; + + pr " Definition mod_gt := Eval lazy beta delta[iter] in"; + pr " (iter _ "; + for i = 0 to size do + pr " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; + pr " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); + pr " (fun n x y => reduce_%i (w%i_modn1 (S n) x y))" i i; + done; + pr " mod_gtnm)."; + pr ""; + + pp " Let spec_modn1 ww (ww_op: znz_op ww) (ww_spec: znz_spec ww_op) := "; + pp " (spec_double_modn1 "; + pp " ww_op.(znz_zdigits) ww_op.(znz_0)"; + pp " (znz_WW ww_op) ww_op.(znz_head0)"; + pp " ww_op.(znz_add_mul_div) ww_op.(znz_div21)"; + pp " ww_op.(znz_compare) ww_op.(znz_sub) (znz_to_Z ww_op)"; + pp " (spec_to_Z ww_spec) "; + pp " (spec_zdigits ww_spec)"; + pp " (spec_0 ww_spec) (spec_WW ww_spec) (spec_head0 ww_spec)"; + pp " (spec_add_mul_div ww_spec) (spec_div21 ww_spec) "; + pp " (CyclicAxioms.spec_compare ww_spec) (CyclicAxioms.spec_sub ww_spec))."; + pp ""; + + pr " Theorem spec_mod_gt:"; + pr " forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y]."; + pa " Admitted."; + pp " Proof."; + pp " refine (spec_iter _ (fun x y res => x > y -> 0 < y ->"; + pp " [res] = x mod y)"; + for i = 0 to size do + pp " (fun x y => reduce_%i (w%i_mod_gt x y))" i i; + pp " (fun n x y => reduce_%i (w%i_mod_gt x (DoubleBase.get_low %s (S n) y)))" i i (pz i); + pp " (fun n x y => reduce_%i (w%i_modn1 (S n) x y)) _ _ _" i i; + done; + pp " mod_gtnm _)."; + for i = 0 to size do + pp " intros x y H1 H2; rewrite spec_reduce_%i." i; + pp " exact (spec_mod_gt w%i_spec x y H1 H2)." i; + if i == size then + pp " intros n x y H2 H3; rewrite spec_reduce_%i." i + else + pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i; + pp " unfold w%i_mod_gt." i; + pp " rewrite <- (spec_get_end%i (S n) y x); auto with zarith." i; + pp " unfold to_Z; apply (spec_mod_gt w%i_spec); auto." i; + pp " rewrite <- (spec_get_end%i (S n) y x) in H2; auto with zarith." i; + pp " rewrite <- (spec_get_end%i (S n) y x) in H3; auto with zarith." i; + if i == size then + pp " intros n x y H2 H3; rewrite spec_reduce_%i." i + else + pp " intros n x y H1 H2 H3; rewrite spec_reduce_%i." i; + pp " unfold w%i_modn1, to_Z; rewrite spec_double_eval%in." i i; + pp " apply (spec_modn1 _ _ w%i_spec); auto." i; + done; + pp " intros n m x y H1 H2; unfold mod_gtnm."; + pp " repeat rewrite spec_reduce_n."; + pp " rewrite <- (spec_cast_l n m x)."; + pp " rewrite <- (spec_cast_r n m y)."; + pp " unfold to_Z; apply (spec_mod_gt (wn_spec (Max.max n m)))."; + pp " rewrite <- (spec_cast_l n m x) in H1; auto."; + pp " rewrite <- (spec_cast_r n m y) in H1; auto."; + pp " rewrite <- (spec_cast_r n m y) in H2; auto."; + pp " Qed."; + pr ""; + + pr " Definition modulo x y := "; + pr " match compare x y with"; + pr " | Eq => zero"; + pr " | Lt => x"; + pr " | Gt => mod_gt x y"; + pr " end."; + pr ""; + + pr " Theorem spec_modulo:"; + pr " forall x y, 0 < [y] -> [modulo x y] = [x] mod [y]."; + pa " Admitted."; + pp " Proof."; + pp " assert (F0: [zero] = 0)."; + pp " exact (spec_0 w0_spec)."; + pp " assert (F1: [one] = 1)."; + pp " exact (spec_1 w0_spec)."; + pp " intros x y H; generalize (spec_compare x y);"; + pp " unfold modulo; case compare; try rewrite F0;"; + pp " try rewrite F1; intros; try split; auto with zarith."; + pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith."; + pp " apply sym_equal; apply Zmod_small; auto with zarith."; + pp " generalize (spec_pos x); auto with zarith."; + pp " apply spec_mod_gt; auto."; + pp " Qed."; + pr ""; + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Gcd *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + pr " Definition digits x :="; + pr " match x with"; + for i = 0 to size do + pr " | %s%i _ => w%i_op.(znz_digits)" c i i; + done; + pr " | %sn n _ => (make_op n).(znz_digits)" c; + pr " end."; + pr ""; + + pr " Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x)."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; clear x."; + for i = 0 to size do + pp " intros x; unfold to_Z, digits;"; + pp " generalize (spec_to_Z w%i_spec x); unfold base; intros H; exact H." i; + done; + pp " intros n x; unfold to_Z, digits;"; + pp " generalize (spec_to_Z (wn_spec n) x); unfold base; intros H; exact H."; + pp " Qed."; + pr ""; + + pr " Definition gcd_gt_body a b cont :="; + pr " match compare b zero with"; + pr " | Gt =>"; + pr " let r := mod_gt a b in"; + pr " match compare r zero with"; + pr " | Gt => cont r (mod_gt b r)"; + pr " | _ => b"; + pr " end"; + pr " | _ => a"; + pr " end."; + pr ""; + + pp " Theorem Zspec_gcd_gt_body: forall a b cont p,"; + pp " [a] > [b] -> [a] < 2 ^ p ->"; + pp " (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] ->"; + pp " Zis_gcd [a1] [b1] [cont a1 b1]) -> "; + pp " Zis_gcd [a] [b] [gcd_gt_body a b cont]."; + pp " Proof."; + pp " assert (F1: [zero] = 0)."; + pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto."; + pp " intros a b cont p H2 H3 H4; unfold gcd_gt_body."; + pp " generalize (spec_compare b zero); case compare; try rewrite F1."; + pp " intros HH; rewrite HH; apply Zis_gcd_0."; + pp " intros HH; absurd (0 <= [b]); auto with zarith."; + pp " case (spec_digits b); auto with zarith."; + pp " intros H5; generalize (spec_compare (mod_gt a b) zero); "; + pp " case compare; try rewrite F1."; + pp " intros H6; rewrite <- (Zmult_1_r [b])."; + pp " rewrite (Z_div_mod_eq [a] [b]); auto with zarith."; + pp " rewrite <- spec_mod_gt; auto with zarith."; + pp " rewrite H6; rewrite Zplus_0_r."; + pp " apply Zis_gcd_mult; apply Zis_gcd_1."; + pp " intros; apply False_ind."; + pp " case (spec_digits (mod_gt a b)); auto with zarith."; + pp " intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith."; + pp " apply DoubleDiv.Zis_gcd_mod; auto with zarith."; + pp " rewrite <- spec_mod_gt; auto with zarith."; + pp " assert (F2: [b] > [mod_gt a b])."; + pp " case (Z_mod_lt [a] [b]); auto with zarith."; + pp " repeat rewrite <- spec_mod_gt; auto with zarith."; + pp " assert (F3: [mod_gt a b] > [mod_gt b (mod_gt a b)])."; + pp " case (Z_mod_lt [b] [mod_gt a b]); auto with zarith."; + pp " rewrite <- spec_mod_gt; auto with zarith."; + pp " repeat rewrite <- spec_mod_gt; auto with zarith."; + pp " apply H4; auto with zarith."; + pp " apply Zmult_lt_reg_r with 2; auto with zarith."; + pp " apply Zle_lt_trans with ([b] + [mod_gt a b]); auto with zarith."; + pp " apply Zle_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith."; + pp " apply Zplus_le_compat_r."; + pp " pattern [b] at 1; rewrite <- (Zmult_1_l [b])."; + pp " apply Zmult_le_compat_r; auto with zarith."; + pp " case (Zle_lt_or_eq 0 ([a]/[b])); auto with zarith."; + pp " intros HH; rewrite (Z_div_mod_eq [a] [b]) in H2;"; + pp " try rewrite <- HH in H2; auto with zarith."; + pp " case (Z_mod_lt [a] [b]); auto with zarith."; + pp " rewrite Zmult_comm; rewrite spec_mod_gt; auto with zarith."; + pp " rewrite <- Z_div_mod_eq; auto with zarith."; + pp " pattern 2 at 2; rewrite <- (Zpower_1_r 2)."; + pp " rewrite <- Zpower_exp; auto with zarith."; + pp " ring_simplify (p - 1 + 1); auto."; + pp " case (Zle_lt_or_eq 0 p); auto with zarith."; + pp " generalize H3; case p; simpl Zpower; auto with zarith."; + pp " intros HH; generalize H3; rewrite <- HH; simpl Zpower; auto with zarith."; + pp " Qed."; + pp ""; + + pr " Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t :="; + pr " gcd_gt_body a b"; + pr " (fun a b =>"; + pr " match p with"; + pr " | xH => cont a b"; + pr " | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b"; + pr " | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b"; + pr " end)."; + pr ""; + + pp " Theorem Zspec_gcd_gt_aux: forall p n a b cont,"; + pp " [a] > [b] -> [a] < 2 ^ (Zpos p + n) ->"; + pp " (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] ->"; + pp " Zis_gcd [a1] [b1] [cont a1 b1]) ->"; + pp " Zis_gcd [a] [b] [gcd_gt_aux p cont a b]."; + pp " intros p; elim p; clear p."; + pp " intros p Hrec n a b cont H2 H3 H4."; + pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xI p) + n); auto."; + pp " intros a1 b1 H6 H7."; + pp " apply Hrec with (Zpos p + n); auto."; + pp " replace (Zpos p + (Zpos p + n)) with"; + pp " (Zpos (xI p) + n - 1); auto."; + pp " rewrite Zpos_xI; ring."; + pp " intros a2 b2 H9 H10."; + pp " apply Hrec with n; auto."; + pp " intros p Hrec n a b cont H2 H3 H4."; + pp " unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xO p) + n); auto."; + pp " intros a1 b1 H6 H7."; + pp " apply Hrec with (Zpos p + n - 1); auto."; + pp " replace (Zpos p + (Zpos p + n - 1)) with"; + pp " (Zpos (xO p) + n - 1); auto."; + pp " rewrite Zpos_xO; ring."; + pp " intros a2 b2 H9 H10."; + pp " apply Hrec with (n - 1); auto."; + pp " replace (Zpos p + (n - 1)) with"; + pp " (Zpos p + n - 1); auto with zarith."; + pp " intros a3 b3 H12 H13; apply H4; auto with zarith."; + pp " apply Zlt_le_trans with (1 := H12)."; + pp " case (Zle_or_lt 1 n); intros HH."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " apply Zle_trans with 0; auto with zarith."; + pp " assert (HH1: n - 1 < 0); auto with zarith."; + pp " generalize HH1; case (n - 1); auto with zarith."; + pp " intros p1 HH2; discriminate."; + pp " intros n a b cont H H2 H3."; + pp " simpl gcd_gt_aux."; + pp " apply Zspec_gcd_gt_body with (n + 1); auto with zarith."; + pp " rewrite Zplus_comm; auto."; + pp " intros a1 b1 H5 H6; apply H3; auto."; + pp " replace n with (n + 1 - 1); auto; try ring."; + pp " Qed."; + pp ""; + + pr " Definition gcd_cont a b :="; + pr " match compare one b with"; + pr " | Eq => one"; + pr " | _ => a"; + pr " end."; + pr ""; + + pr " Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b."; + pr ""; + + pr " Theorem spec_gcd_gt: forall a b,"; + pr " [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b]."; + pa " Admitted."; + pp " Proof."; + pp " intros a b H2."; + pp " case (spec_digits (gcd_gt a b)); intros H3 H4."; + pp " case (spec_digits a); intros H5 H6."; + pp " apply sym_equal; apply Zis_gcd_gcd; auto with zarith."; + pp " unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith."; + pp " intros a1 a2; rewrite Zpower_0_r."; + pp " case (spec_digits a2); intros H7 H8;"; + pp " intros; apply False_ind; auto with zarith."; + pp " Qed."; + pr ""; + + pr " Definition gcd a b :="; + pr " match compare a b with"; + pr " | Eq => a"; + pr " | Lt => gcd_gt b a"; + pr " | Gt => gcd_gt a b"; + pr " end."; + pr ""; + + pr " Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b]."; + pa " Admitted."; + pp " Proof."; + pp " intros a b."; + pp " case (spec_digits a); intros H1 H2."; + pp " case (spec_digits b); intros H3 H4."; + pp " unfold gcd; generalize (spec_compare a b); case compare."; + pp " intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto."; + pp " apply Zis_gcd_refl."; + pp " intros; apply trans_equal with (Zgcd [b] [a])."; + pp " apply spec_gcd_gt; auto with zarith."; + pp " apply Zis_gcd_gcd; auto with zarith."; + pp " apply Zgcd_is_pos."; + pp " apply Zis_gcd_sym; apply Zgcd_is_gcd."; + pp " intros; apply spec_gcd_gt; auto."; + pp " Qed."; + pr ""; + + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Conversion *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + pr " Definition pheight p := "; + pr " Peano.pred (nat_of_P (get_height w0_op.(znz_digits) (plength p)))."; + pr ""; + + pr " Theorem pheight_correct: forall p, "; + pr " Zpos p < 2 ^ (Zpos (znz_digits w0_op) * 2 ^ (Z_of_nat (pheight p)))."; + pr " Proof."; + pr " intros p; unfold pheight."; + pr " assert (F1: forall x, Z_of_nat (Peano.pred (nat_of_P x)) = Zpos x - 1)."; + pr " intros x."; + pr " assert (Zsucc (Z_of_nat (Peano.pred (nat_of_P x))) = Zpos x); auto with zarith."; + pr " rewrite <- inj_S."; + pr " rewrite <- (fun x => S_pred x 0); auto with zarith."; + pr " rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto."; + pr " apply lt_le_trans with 1%snat; auto with zarith." "%"; + pr " exact (le_Pmult_nat x 1)."; + pr " rewrite F1; clear F1."; + pr " assert (F2:= (get_height_correct (znz_digits w0_op) (plength p)))."; + pr " apply Zlt_le_trans with (Zpos (Psucc p))."; + pr " rewrite Zpos_succ_morphism; auto with zarith."; + pr " apply Zle_trans with (1 := plength_pred_correct (Psucc p))."; + pr " rewrite Ppred_succ."; + pr " apply Zpower_le_monotone; auto with zarith."; + pr " Qed."; + pr ""; + + pr " Definition of_pos x :="; + pr " let h := pheight x in"; + pr " match h with"; + for i = 0 to size do + pr " | %i%snat => reduce_%i (snd (w%i_op.(znz_of_pos) x))" i "%" i i; + done; + pr " | _ =>"; + pr " let n := minus h %i in" (size + 1); + pr " reduce_n n (snd ((make_op n).(znz_of_pos) x))"; + pr " end."; + pr ""; + + pr " Theorem spec_of_pos: forall x,"; + pr " [of_pos x] = Zpos x."; + pa " Admitted."; + pp " Proof."; + pp " assert (F := spec_more_than_1_digit w0_spec)."; + pp " intros x; unfold of_pos; case_eq (pheight x)."; + for i = 0 to size do + if i <> 0 then + pp " intros n; case n; clear n."; + pp " intros H1; rewrite spec_reduce_%i; unfold to_Z." i; + pp " apply (znz_of_pos_correct w%i_spec)." i; + pp " apply Zlt_le_trans with (1 := pheight_correct x)."; + pp " rewrite H1; simpl Z_of_nat; change (2^%i) with (%s)." i (gen2 i); + pp " unfold base."; + pp " apply Zpower_le_monotone; split; auto with zarith."; + if i <> 0 then + begin + pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc."; + pp " repeat rewrite <- Zpos_xO."; + pp " refine (Zle_refl _)."; + end; + done; + pp " intros n."; + pp " intros H1; rewrite spec_reduce_n; unfold to_Z."; + pp " simpl minus; rewrite <- minus_n_O."; + pp " apply (znz_of_pos_correct (wn_spec n))."; + pp " apply Zlt_le_trans with (1 := pheight_correct x)."; + pp " unfold base."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " split; auto with zarith."; + pp " rewrite H1."; + pp " elim n; clear n H1."; + pp " simpl Z_of_nat; change (2^%i) with (%s)." (size + 1) (gen2 (size + 1)); + pp " rewrite Zmult_comm; repeat rewrite <- Zmult_assoc."; + pp " repeat rewrite <- Zpos_xO."; + pp " refine (Zle_refl _)."; + pp " intros n Hrec."; + pp " rewrite make_op_S."; + pp " change (@znz_digits (word _ (S (S n))) (mk_zn2z_op_karatsuba (make_op n))) with"; + pp " (xO (znz_digits (make_op n)))."; + pp " rewrite (fun x y => (Zpos_xO (@znz_digits x y)))."; + pp " rewrite inj_S; unfold Zsucc."; + pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith."; + pp " rewrite Zpower_1_r."; + pp " assert (tmp: forall x y z, x * (y * z) = y * (x * z));"; + pp " [intros; ring | rewrite tmp; clear tmp]."; + pp " apply Zmult_le_compat_l; auto with zarith."; + pp " Qed."; + pr ""; + + pr " Definition of_N x :="; + pr " match x with"; + pr " | BinNat.N0 => zero"; + pr " | Npos p => of_pos p"; + pr " end."; + pr ""; + + pr " Theorem spec_of_N: forall x,"; + pr " [of_N x] = Z_of_N x."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x."; + pp " simpl of_N."; + pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto."; + pp " intros p; exact (spec_of_pos p)."; + pp " Qed."; + pr ""; + + pr " (***************************************************************)"; + pr " (* *)"; + pr " (* Shift *)"; + pr " (* *)"; + pr " (***************************************************************)"; + pr ""; + + (* Head0 *) + pr " Definition head0 w := match w with"; + for i = 0 to size do + pr " | %s%i w=> reduce_%i (w%i_op.(znz_head0) w)" c i i i; + done; + pr " | %sn n w=> reduce_n n ((make_op n).(znz_head0) w)" c; + pr " end."; + pr ""; + + pr " Theorem spec_head00: forall x, [x] = 0 ->[head0 x] = Zpos (digits x)."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; unfold head0; clear x."; + for i = 0 to size do + pp " intros x; rewrite spec_reduce_%i; exact (spec_head00 w%i_spec x)." i i; + done; + pp " intros n x; rewrite spec_reduce_n; exact (spec_head00 (wn_spec n) x)."; + pp " Qed."; + pr " "; + + pr " Theorem spec_head0: forall x, 0 < [x] ->"; + pr " 2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x)."; + pa " Admitted."; + pp " Proof."; + pp " assert (F0: forall x, (x - 1) + 1 = x)."; + pp " intros; ring. "; + pp " intros x; case x; unfold digits, head0; clear x."; + for i = 0 to size do + pp " intros x Hx; rewrite spec_reduce_%i." i; + pp " assert (F1:= spec_more_than_1_digit w%i_spec)." i; + pp " generalize (spec_head0 w%i_spec x Hx)." i; + pp " unfold base."; + pp " pattern (Zpos (znz_digits w%i_op)) at 1; " i; + pp " rewrite <- (fun x => (F0 (Zpos x)))."; + pp " rewrite Zpower_exp; auto with zarith."; + pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith."; + done; + pp " intros n x Hx; rewrite spec_reduce_n."; + pp " assert (F1:= spec_more_than_1_digit (wn_spec n))."; + pp " generalize (spec_head0 (wn_spec n) x Hx)."; + pp " unfold base."; + pp " pattern (Zpos (znz_digits (make_op n))) at 1; "; + pp " rewrite <- (fun x => (F0 (Zpos x)))."; + pp " rewrite Zpower_exp; auto with zarith."; + pp " rewrite Zpower_1_r; rewrite Z_div_mult; auto with zarith."; + pp " Qed."; + pr ""; + + + (* Tail0 *) + pr " Definition tail0 w := match w with"; + for i = 0 to size do + pr " | %s%i w=> reduce_%i (w%i_op.(znz_tail0) w)" c i i i; + done; + pr " | %sn n w=> reduce_n n ((make_op n).(znz_tail0) w)" c; + pr " end."; + pr ""; + + + pr " Theorem spec_tail00: forall x, [x] = 0 ->[tail0 x] = Zpos (digits x)."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; unfold tail0; clear x."; + for i = 0 to size do + pp " intros x; rewrite spec_reduce_%i; exact (spec_tail00 w%i_spec x)." i i; + done; + pp " intros n x; rewrite spec_reduce_n; exact (spec_tail00 (wn_spec n) x)."; + pp " Qed."; + pr " "; + + + pr " Theorem spec_tail0: forall x,"; + pr " 0 < [x] -> exists y, 0 <= y /\\ [x] = (2 * y + 1) * 2 ^ [tail0 x]."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; clear x; unfold tail0."; + for i = 0 to size do + pp " intros x Hx; rewrite spec_reduce_%i; exact (spec_tail0 w%i_spec x Hx)." i i; + done; + pp " intros n x Hx; rewrite spec_reduce_n; exact (spec_tail0 (wn_spec n) x Hx)."; + pp " Qed."; + pr ""; + + + (* Number of digits *) + pr " Definition %sdigits x :=" c; + pr " match x with"; + pr " | %s0 _ => %s0 w0_op.(znz_zdigits)" c c; + for i = 1 to size do + pr " | %s%i _ => reduce_%i w%i_op.(znz_zdigits)" c i i i; + done; + pr " | %sn n _ => reduce_n n (make_op n).(znz_zdigits)" c; + pr " end."; + pr ""; + + pr " Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x)."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; clear x; unfold Ndigits, digits."; + for i = 0 to size do + pp " intros _; try rewrite spec_reduce_%i; exact (spec_zdigits w%i_spec)." i i; + done; + pp " intros n _; try rewrite spec_reduce_n; exact (spec_zdigits (wn_spec n))."; + pp " Qed."; + pr ""; + + + (* Shiftr *) + for i = 0 to size do + pr " Definition shiftr%i n x := w%i_op.(znz_add_mul_div) (w%i_op.(znz_sub) w%i_op.(znz_zdigits) n) w%i_op.(znz_0) x." i i i i i; + done; + pr " Definition shiftrn n p x := (make_op n).(znz_add_mul_div) ((make_op n).(znz_sub) (make_op n).(znz_zdigits) p) (make_op n).(znz_0) x."; + pr ""; + + pr " Definition shiftr := Eval lazy beta delta [same_level] in "; + pr " same_level _ (fun n x => %s0 (shiftr0 n x))" c; + for i = 1 to size do + pr " (fun n x => reduce_%i (shiftr%i n x))" i i; + done; + pr " (fun n p x => reduce_n n (shiftrn n p x))."; + pr ""; + + + pr " Theorem spec_shiftr: forall n x,"; + pr " [n] <= [Ndigits x] -> [shiftr n x] = [x] / 2 ^ [n]."; + pa " Admitted."; + pp " Proof."; + pp " assert (F0: forall x y, x - (x - y) = y)."; + pp " intros; ring."; + pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z)."; + pp " intros x y z HH HH1 HH2."; + pp " split; auto with zarith."; + pp " apply Zle_lt_trans with (2 := HH2); auto with zarith."; + pp " apply Zdiv_le_upper_bound; auto with zarith."; + pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith."; + pp " apply Zmult_le_compat_l; auto."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " rewrite Zpower_0_r; ring."; + pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x)."; + pp " intros xx y HH HH1."; + pp " split; auto with zarith."; + pp " apply Zle_lt_trans with xx; auto with zarith."; + pp " apply Zpower2_lt_lin; auto with zarith."; + pp " assert (F4: forall ww ww1 ww2 "; + pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)"; + pp " xx yy xx1 yy1,"; + pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_zdigits ww1_op) ->"; + pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->"; + pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->"; + pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->"; + pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->"; + pp " znz_to_Z ww_op"; + pp " (znz_add_mul_div ww_op (znz_sub ww_op (znz_zdigits ww_op) yy1)"; + pp " (znz_0 ww_op) xx1) = znz_to_Z ww1_op xx / 2 ^ znz_to_Z ww2_op yy)."; + pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy."; + pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2."; + pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4."; + pp " rewrite <- Hx."; + pp " rewrite <- Hy."; + pp " generalize (spec_add_mul_div Hw"; + pp " (znz_0 ww_op) xx1"; + pp " (znz_sub ww_op (znz_zdigits ww_op) "; + pp " yy1)"; + pp " )."; + pp " rewrite (spec_0 Hw)."; + pp " rewrite Zmult_0_l; rewrite Zplus_0_l."; + pp " rewrite (CyclicAxioms.spec_sub Hw)."; + pp " rewrite Zmod_small; auto with zarith."; + pp " rewrite (spec_zdigits Hw)."; + pp " rewrite F0."; + pp " rewrite Zmod_small; auto with zarith."; + pp " unfold base; rewrite (spec_zdigits Hw) in Hl1 |- *;"; + pp " auto with zarith."; + pp " assert (F5: forall n m, (n <= m)%snat ->" "%"; + pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m)))."; + pp " intros n m HH; elim HH; clear m HH; auto with zarith."; + pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec)."; + pp " rewrite make_op_S."; + pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end."; + pp " rewrite Zpos_xO."; + pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith."; + pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size; + pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0)))."; + pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; + pp " rewrite Zpos_xO."; + pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size; + pp " apply F5; auto with arith."; + pp " intros x; case x; clear x; unfold shiftr, same_level."; + for i = 0 to size do + pp " intros x y; case y; clear y."; + for j = 0 to i - 1 do + pp " intros y; unfold shiftr%i, Ndigits." i; + pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; + pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i; + pp " rewrite (spec_zdigits w%i_spec)." i; + pp " rewrite (spec_zdigits w%i_spec)." j; + pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)")); + pp " repeat rewrite (fun x => Zpos_xO (xO x))."; + pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; + pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j; + pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i; + + done; + pp " intros y; unfold shiftr%i, Ndigits." i; + pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i; + pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i; + for j = i + 1 to size do + pp " intros y; unfold shiftr%i, Ndigits." j; + pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; + pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i; + pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j; + done; + if i == size then + begin + pp " intros m y; unfold shiftrn, Ndigits."; + pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; + pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size; + pp " try (apply sym_equal; exact (spec_extend%in m x))." size; + end + else + begin + pp " intros m y; unfold shiftrn, Ndigits."; + pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; + pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i; + pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i; + pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size; + end + done; + pp " intros n x y; case y; clear y;"; + pp " intros y; unfold shiftrn, Ndigits; try rewrite spec_reduce_n."; + for i = 0 to size do + pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i; + pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i; + pp " rewrite (spec_zdigits w%i_spec)." i; + pp " rewrite (spec_zdigits (wn_spec n))."; + pp " apply Zle_trans with (2 := F6 n)."; + pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)")); + pp " repeat rewrite (fun x => Zpos_xO (xO x))."; + pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; + pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i; + if i == size then + pp " change ([Nn n (extend%i n y)] = [N%i y])." size i + else + pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i; + pp " rewrite <- (spec_extend%in n); auto." size; + if i <> size then + pp " try (rewrite <- spec_extend%in%i; auto)." i size; + done; + pp " generalize y; clear y; intros m y."; + pp " rewrite spec_reduce_n; unfold to_Z; intros H1."; + pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith."; + pp " rewrite (spec_zdigits (wn_spec m))."; + pp " rewrite (spec_zdigits (wn_spec (Max.max n m)))."; + pp " apply F5; auto with arith."; + pp " exact (spec_cast_r n m y)."; + pp " exact (spec_cast_l n m x)."; + pp " Qed."; + pr ""; + + pr " Definition safe_shiftr n x := "; + pr " match compare n (Ndigits x) with"; + pr " | Lt => shiftr n x "; + pr " | _ => %s0 w_0" c; + pr " end."; + pr ""; + + + pr " Theorem spec_safe_shiftr: forall n x,"; + pr " [safe_shiftr n x] = [x] / 2 ^ [n]."; + pa " Admitted."; + pp " Proof."; + pp " intros n x; unfold safe_shiftr;"; + pp " generalize (spec_compare n (Ndigits x)); case compare; intros H."; + pp " apply trans_equal with (1 := spec_0 w0_spec)."; + pp " apply sym_equal; apply Zdiv_small; rewrite H."; + pp " rewrite spec_Ndigits; exact (spec_digits x)."; + pp " rewrite <- spec_shiftr; auto with zarith."; + pp " apply trans_equal with (1 := spec_0 w0_spec)."; + pp " apply sym_equal; apply Zdiv_small."; + pp " rewrite spec_Ndigits in H; case (spec_digits x); intros H1 H2."; + pp " split; auto."; + pp " apply Zlt_le_trans with (1 := H2)."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " Qed."; + pr ""; + + pr ""; + + (* Shiftl *) + for i = 0 to size do + pr " Definition shiftl%i n x := w%i_op.(znz_add_mul_div) n x w%i_op.(znz_0)." i i i + done; + pr " Definition shiftln n p x := (make_op n).(znz_add_mul_div) p x (make_op n).(znz_0)."; + pr " Definition shiftl := Eval lazy beta delta [same_level] in"; + pr " same_level _ (fun n x => %s0 (shiftl0 n x))" c; + for i = 1 to size do + pr " (fun n x => reduce_%i (shiftl%i n x))" i i; + done; + pr " (fun n p x => reduce_n n (shiftln n p x))."; + pr ""; + pr ""; + + + pr " Theorem spec_shiftl: forall n x,"; + pr " [n] <= [head0 x] -> [shiftl n x] = [x] * 2 ^ [n]."; + pa " Admitted."; + pp " Proof."; + pp " assert (F0: forall x y, x - (x - y) = y)."; + pp " intros; ring."; + pp " assert (F2: forall x y z, 0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z)."; + pp " intros x y z HH HH1 HH2."; + pp " split; auto with zarith."; + pp " apply Zle_lt_trans with (2 := HH2); auto with zarith."; + pp " apply Zdiv_le_upper_bound; auto with zarith."; + pp " pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith."; + pp " apply Zmult_le_compat_l; auto."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " rewrite Zpower_0_r; ring."; + pp " assert (F3: forall x y, 0 <= y -> y <= x -> 0 <= x - y < 2 ^ x)."; + pp " intros xx y HH HH1."; + pp " split; auto with zarith."; + pp " apply Zle_lt_trans with xx; auto with zarith."; + pp " apply Zpower2_lt_lin; auto with zarith."; + pp " assert (F4: forall ww ww1 ww2 "; + pp " (ww_op: znz_op ww) (ww1_op: znz_op ww1) (ww2_op: znz_op ww2)"; + pp " xx yy xx1 yy1,"; + pp " znz_to_Z ww2_op yy <= znz_to_Z ww1_op (znz_head0 ww1_op xx) ->"; + pp " znz_to_Z ww1_op (znz_zdigits ww1_op) <= znz_to_Z ww_op (znz_zdigits ww_op) ->"; + pp " znz_spec ww_op -> znz_spec ww1_op -> znz_spec ww2_op ->"; + pp " znz_to_Z ww_op xx1 = znz_to_Z ww1_op xx ->"; + pp " znz_to_Z ww_op yy1 = znz_to_Z ww2_op yy ->"; + pp " znz_to_Z ww_op"; + pp " (znz_add_mul_div ww_op yy1"; + pp " xx1 (znz_0 ww_op)) = znz_to_Z ww1_op xx * 2 ^ znz_to_Z ww2_op yy)."; + pp " intros ww ww1 ww2 ww_op ww1_op ww2_op xx yy xx1 yy1 Hl Hl1 Hw Hw1 Hw2 Hx Hy."; + pp " case (spec_to_Z Hw xx1); auto with zarith; intros HH1 HH2."; + pp " case (spec_to_Z Hw yy1); auto with zarith; intros HH3 HH4."; + pp " rewrite <- Hx."; + pp " rewrite <- Hy."; + pp " generalize (spec_add_mul_div Hw xx1 (znz_0 ww_op) yy1)."; + pp " rewrite (spec_0 Hw)."; + pp " assert (F1: znz_to_Z ww1_op (znz_head0 ww1_op xx) <= Zpos (znz_digits ww1_op))."; + pp " case (Zle_lt_or_eq _ _ HH1); intros HH5."; + pp " apply Zlt_le_weak."; + pp " case (CyclicAxioms.spec_head0 Hw1 xx)."; + pp " rewrite <- Hx; auto."; + pp " intros _ Hu; unfold base in Hu."; + pp " case (Zle_or_lt (Zpos (znz_digits ww1_op))"; + pp " (znz_to_Z ww1_op (znz_head0 ww1_op xx))); auto; intros H1."; + pp " absurd (2 ^ (Zpos (znz_digits ww1_op)) <= 2 ^ (znz_to_Z ww1_op (znz_head0 ww1_op xx)))."; + pp " apply Zlt_not_le."; + pp " case (spec_to_Z Hw1 xx); intros HHx3 HHx4."; + pp " rewrite <- (Zmult_1_r (2 ^ znz_to_Z ww1_op (znz_head0 ww1_op xx)))."; + pp " apply Zle_lt_trans with (2 := Hu)."; + pp " apply Zmult_le_compat_l; auto with zarith."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith."; + pp " rewrite Zdiv_0_l; auto with zarith."; + pp " rewrite Zplus_0_r."; + pp " case (Zle_lt_or_eq _ _ HH1); intros HH5."; + pp " rewrite Zmod_small; auto with zarith."; + pp " intros HH; apply HH."; + pp " rewrite Hy; apply Zle_trans with (1:= Hl)."; + pp " rewrite <- (spec_zdigits Hw). "; + pp " apply Zle_trans with (2 := Hl1); auto."; + pp " rewrite (spec_zdigits Hw1); auto with zarith."; + pp " split; auto with zarith ."; + pp " apply Zlt_le_trans with (base (znz_digits ww1_op))."; + pp " rewrite Hx."; + pp " case (CyclicAxioms.spec_head0 Hw1 xx); auto."; + pp " rewrite <- Hx; auto."; + pp " intros _ Hu; rewrite Zmult_comm in Hu."; + pp " apply Zle_lt_trans with (2 := Hu)."; + pp " apply Zmult_le_compat_l; auto with zarith."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " unfold base; apply Zpower_le_monotone; auto with zarith."; + pp " split; auto with zarith."; + pp " rewrite <- (spec_zdigits Hw); auto with zarith."; + pp " rewrite <- (spec_zdigits Hw1); auto with zarith."; + pp " rewrite <- HH5."; + pp " rewrite Zmult_0_l."; + pp " rewrite Zmod_small; auto with zarith."; + pp " intros HH; apply HH."; + pp " rewrite Hy; apply Zle_trans with (1 := Hl)."; + pp " rewrite (CyclicAxioms.spec_head00 Hw1 xx); auto with zarith."; + pp " rewrite <- (spec_zdigits Hw); auto with zarith."; + pp " rewrite <- (spec_zdigits Hw1); auto with zarith."; + pp " assert (F5: forall n m, (n <= m)%snat ->" "%"; + pp " Zpos (znz_digits (make_op n)) <= Zpos (znz_digits (make_op m)))."; + pp " intros n m HH; elim HH; clear m HH; auto with zarith."; + pp " intros m HH Hrec; apply Zle_trans with (1 := Hrec)."; + pp " rewrite make_op_S."; + pp " match goal with |- Zpos ?Y <= ?X => change X with (Zpos (xO Y)) end."; + pp " rewrite Zpos_xO."; + pp " assert (0 <= Zpos (znz_digits (make_op n))); auto with zarith."; + pp " assert (F6: forall n, Zpos (znz_digits w%i_op) <= Zpos (znz_digits (make_op n)))." size; + pp " intros n ; apply Zle_trans with (Zpos (znz_digits (make_op 0)))."; + pp " change (znz_digits (make_op 0)) with (xO (znz_digits w%i_op))." size; + pp " rewrite Zpos_xO."; + pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." size; + pp " apply F5; auto with arith."; + pp " intros x; case x; clear x; unfold shiftl, same_level."; + for i = 0 to size do + pp " intros x y; case y; clear y."; + for j = 0 to i - 1 do + pp " intros y; unfold shiftl%i, head0." i; + pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; + pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i j i; + pp " rewrite (spec_zdigits w%i_spec)." i; + pp " rewrite (spec_zdigits w%i_spec)." j; + pp " change (znz_digits w%i_op) with %s." i (genxO (i - j) (" (znz_digits w"^(string_of_int j)^"_op)")); + pp " repeat rewrite (fun x => Zpos_xO (xO x))."; + pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; + pp " assert (0 <= Zpos (znz_digits w%i_op)); auto with zarith." j; + pp " try (apply sym_equal; exact (spec_extend%in%i y))." j i; + done; + pp " intros y; unfold shiftl%i, head0." i; + pp " repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i; + pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." i i i; + for j = i + 1 to size do + pp " intros y; unfold shiftl%i, head0." j; + pp " repeat rewrite spec_reduce_%i; repeat rewrite spec_reduce_%i; unfold to_Z; intros H1." i j; + pp " apply F4 with (3:=w%i_spec)(4:=w%i_spec)(5:=w%i_spec); auto with zarith." j j i; + pp " try (apply sym_equal; exact (spec_extend%in%i x))." i j; + done; + if i == size then + begin + pp " intros m y; unfold shiftln, head0."; + pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; + pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." size; + pp " try (apply sym_equal; exact (spec_extend%in m x))." size; + end + else + begin + pp " intros m y; unfold shiftln, head0."; + pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; + pp " apply F4 with (3:=(wn_spec m))(4:=wn_spec m)(5:=w%i_spec); auto with zarith." i; + pp " change ([Nn m (extend%i m (extend%i %i x))] = [N%i x])." size i (size - i - 1) i; + pp " rewrite <- (spec_extend%in m); rewrite <- spec_extend%in%i; auto." size i size; + end + done; + pp " intros n x y; case y; clear y;"; + pp " intros y; unfold shiftln, head0; try rewrite spec_reduce_n."; + for i = 0 to size do + pp " try rewrite spec_reduce_%i; unfold to_Z; intros H1." i; + pp " apply F4 with (3:=(wn_spec n))(4:=w%i_spec)(5:=wn_spec n); auto with zarith." i; + pp " rewrite (spec_zdigits w%i_spec)." i; + pp " rewrite (spec_zdigits (wn_spec n))."; + pp " apply Zle_trans with (2 := F6 n)."; + pp " change (znz_digits w%i_op) with %s." size (genxO (size - i) ("(znz_digits w" ^ (string_of_int i) ^ "_op)")); + pp " repeat rewrite (fun x => Zpos_xO (xO x))."; + pp " repeat rewrite (fun x y => Zpos_xO (@znz_digits x y))."; + pp " assert (H: 0 <= Zpos (znz_digits w%i_op)); auto with zarith." i; + if i == size then + pp " change ([Nn n (extend%i n y)] = [N%i y])." size i + else + pp " change ([Nn n (extend%i n (extend%i %i y))] = [N%i y])." size i (size - i - 1) i; + pp " rewrite <- (spec_extend%in n); auto." size; + if i <> size then + pp " try (rewrite <- spec_extend%in%i; auto)." i size; + done; + pp " generalize y; clear y; intros m y."; + pp " repeat rewrite spec_reduce_n; unfold to_Z; intros H1."; + pp " apply F4 with (3:=(wn_spec (Max.max n m)))(4:=wn_spec m)(5:=wn_spec n); auto with zarith."; + pp " rewrite (spec_zdigits (wn_spec m))."; + pp " rewrite (spec_zdigits (wn_spec (Max.max n m)))."; + pp " apply F5; auto with arith."; + pp " exact (spec_cast_r n m y)."; + pp " exact (spec_cast_l n m x)."; + pp " Qed."; + pr ""; + + (* Double size *) + pr " Definition double_size w := match w with"; + for i = 0 to size-1 do + pr " | %s%i x => %s%i (WW (znz_0 w%i_op) x)" c i c (i + 1) i; + done; + pr " | %s%i x => %sn 0 (WW (znz_0 w%i_op) x)" c size c size; + pr " | %sn n x => %sn (S n) (WW (znz_0 (make_op n)) x)" c c; + pr " end."; + pr ""; + + pr " Theorem spec_double_size_digits: "; + pr " forall x, digits (double_size x) = xO (digits x)."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; unfold double_size, digits; clear x; auto."; + pp " intros n x; rewrite make_op_S; auto."; + pp " Qed."; + pr ""; + + + pr " Theorem spec_double_size: forall x, [double_size x] = [x]."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; unfold double_size; clear x."; + for i = 0 to size do + pp " intros x; unfold to_Z, make_op; "; + pp " rewrite znz_to_Z_%i; rewrite (spec_0 w%i_spec); auto with zarith." (i + 1) i; + done; + pp " intros n x; unfold to_Z;"; + pp " generalize (znz_to_Z_n n); simpl word."; + pp " intros HH; rewrite HH; clear HH."; + pp " generalize (spec_0 (wn_spec n)); simpl word."; + pp " intros HH; rewrite HH; clear HH; auto with zarith."; + pp " Qed."; + pr ""; + + + pr " Theorem spec_double_size_head0: "; + pr " forall x, 2 * [head0 x] <= [head0 (double_size x)]."; + pa " Admitted."; + pp " Proof."; + pp " intros x."; + pp " assert (F1:= spec_pos (head0 x))."; + pp " assert (F2: 0 < Zpos (digits x))."; + pp " red; auto."; + pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH."; + pp " generalize HH; rewrite <- (spec_double_size x); intros HH1."; + pp " case (spec_head0 x HH); intros _ HH2."; + pp " case (spec_head0 _ HH1)."; + pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x)."; + pp " intros HH3 _."; + pp " case (Zle_or_lt ([head0 (double_size x)]) (2 * [head0 x])); auto; intros HH4."; + pp " absurd (2 ^ (2 * [head0 x] )* [x] < 2 ^ [head0 (double_size x)] * [x]); auto."; + pp " apply Zle_not_lt."; + pp " apply Zmult_le_compat_r; auto with zarith."; + pp " apply Zpower_le_monotone; auto; auto with zarith."; + pp " generalize (spec_pos (head0 (double_size x))); auto with zarith."; + pp " assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1))."; + pp " case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5."; + pp " apply Zmult_le_reg_r with (2 ^ 1); auto with zarith."; + pp " rewrite <- (fun x y z => Zpower_exp x (y - z)); auto with zarith."; + pp " assert (tmp: forall x, x - 1 + 1 = x); [intros; ring | rewrite tmp; clear tmp]."; + pp " apply Zle_trans with (2 := Zlt_le_weak _ _ HH2)."; + pp " apply Zmult_le_compat_l; auto with zarith."; + pp " rewrite Zpower_1_r; auto with zarith."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " split; auto with zarith. "; + pp " case (Zle_or_lt (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6."; + pp " absurd (2 ^ Zpos (digits x) <= 2 ^ [head0 x] * [x]); auto with zarith."; + pp " rewrite <- HH5; rewrite Zmult_1_r."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " rewrite (Zmult_comm 2)."; + pp " rewrite Zpower_mult; auto with zarith."; + pp " rewrite Zpower_2."; + pp " apply Zlt_le_trans with (2 := HH3)."; + pp " rewrite <- Zmult_assoc."; + pp " replace (Zpos (xO (digits x)) - 1) with"; + pp " ((Zpos (digits x) - 1) + (Zpos (digits x)))."; + pp " rewrite Zpower_exp; auto with zarith."; + pp " apply Zmult_lt_compat2; auto with zarith."; + pp " split; auto with zarith."; + pp " apply Zmult_lt_0_compat; auto with zarith."; + pp " rewrite Zpos_xO; ring."; + pp " apply Zlt_le_weak; auto."; + pp " repeat rewrite spec_head00; auto."; + pp " rewrite spec_double_size_digits."; + pp " rewrite Zpos_xO; auto with zarith."; + pp " rewrite spec_double_size; auto."; + pp " Qed."; + pr ""; + + pr " Theorem spec_double_size_head0_pos: "; + pr " forall x, 0 < [head0 (double_size x)]."; + pa " Admitted."; + pp " Proof."; + pp " intros x."; + pp " assert (F: 0 < Zpos (digits x))."; + pp " red; auto."; + pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0."; + pp " case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1."; + pp " apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith."; + pp " case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3."; + pp " generalize F3; rewrite <- (spec_double_size x); intros F4."; + pp " absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x)))."; + pp " apply Zle_not_lt."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " split; auto with zarith."; + pp " rewrite Zpos_xO; auto with zarith."; + pp " case (spec_head0 x F3)."; + pp " rewrite <- F1; rewrite Zpower_0_r; rewrite Zmult_1_l; intros _ HH."; + pp " apply Zle_lt_trans with (2 := HH)."; + pp " case (spec_head0 _ F4)."; + pp " rewrite (spec_double_size x); rewrite (spec_double_size_digits x)."; + pp " rewrite <- F0; rewrite Zpower_0_r; rewrite Zmult_1_l; auto."; + pp " generalize F1; rewrite (spec_head00 _ (sym_equal F3)); auto with zarith."; + pp " Qed."; + pr ""; + + + (* Safe shiftl *) + + pr " Definition safe_shiftl_aux_body cont n x :="; + pr " match compare n (head0 x) with"; + pr " Gt => cont n (double_size x)"; + pr " | _ => shiftl n x"; + pr " end."; + pr ""; + + pr " Theorem spec_safe_shift_aux_body: forall n p x cont,"; + pr " 2^ Zpos p <= [head0 x] ->"; + pr " (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->"; + pr " [cont n x] = [x] * 2 ^ [n]) ->"; + pr " [safe_shiftl_aux_body cont n x] = [x] * 2 ^ [n]."; + pa " Admitted."; + pp " Proof."; + pp " intros n p x cont H1 H2; unfold safe_shiftl_aux_body."; + pp " generalize (spec_compare n (head0 x)); case compare; intros H."; + pp " apply spec_shiftl; auto with zarith."; + pp " apply spec_shiftl; auto with zarith."; + pp " rewrite H2."; + pp " rewrite spec_double_size; auto."; + pp " rewrite Zplus_comm; rewrite Zpower_exp; auto with zarith."; + pp " apply Zle_trans with (2 := spec_double_size_head0 x)."; + pp " rewrite Zpower_1_r; apply Zmult_le_compat_l; auto with zarith."; + pp " Qed."; + pr ""; + + pr " Fixpoint safe_shiftl_aux p cont n x {struct p} :="; + pr " safe_shiftl_aux_body "; + pr " (fun n x => match p with"; + pr " | xH => cont n x"; + pr " | xO p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x"; + pr " | xI p => safe_shiftl_aux p (safe_shiftl_aux p cont) n x"; + pr " end) n x."; + pr ""; + + pr " Theorem spec_safe_shift_aux: forall p q n x cont,"; + pr " 2 ^ (Zpos q) <= [head0 x] ->"; + pr " (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->"; + pr " [cont n x] = [x] * 2 ^ [n]) -> "; + pr " [safe_shiftl_aux p cont n x] = [x] * 2 ^ [n]."; + pa " Admitted."; + pp " Proof."; + pp " intros p; elim p; unfold safe_shiftl_aux; fold safe_shiftl_aux; clear p."; + pp " intros p Hrec q n x cont H1 H2."; + pp " apply spec_safe_shift_aux_body with (q); auto."; + pp " intros x1 H3; apply Hrec with (q + 1)%spositive; auto." "%"; + pp " intros x2 H4; apply Hrec with (p + q + 1)%spositive; auto." "%"; + pp " rewrite <- Pplus_assoc."; + pp " rewrite Zpos_plus_distr; auto."; + pp " intros x3 H5; apply H2."; + pp " rewrite Zpos_xI."; + pp " replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1));"; + pp " auto."; + pp " repeat rewrite Zpos_plus_distr; ring."; + pp " intros p Hrec q n x cont H1 H2."; + pp " apply spec_safe_shift_aux_body with (q); auto."; + pp " intros x1 H3; apply Hrec with (q); auto."; + pp " apply Zle_trans with (2 := H3); auto with zarith."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " intros x2 H4; apply Hrec with (p + q)%spositive; auto." "%"; + pp " intros x3 H5; apply H2."; + pp " rewrite (Zpos_xO p)."; + pp " replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q));"; + pp " auto."; + pp " repeat rewrite Zpos_plus_distr; ring."; + pp " intros q n x cont H1 H2."; + pp " apply spec_safe_shift_aux_body with (q); auto."; + pp " rewrite Zplus_comm; auto."; + pp " Qed."; + pr ""; + + + pr " Definition safe_shiftl n x :="; + pr " safe_shiftl_aux_body"; + pr " (safe_shiftl_aux_body"; + pr " (safe_shiftl_aux (digits n) shiftl)) n x."; + pr ""; + + pr " Theorem spec_safe_shift: forall n x,"; + pr " [safe_shiftl n x] = [x] * 2 ^ [n]."; + pa " Admitted."; + pp " Proof."; + pp " intros n x; unfold safe_shiftl, safe_shiftl_aux_body."; + pp " generalize (spec_compare n (head0 x)); case compare; intros H."; + pp " apply spec_shiftl; auto with zarith."; + pp " apply spec_shiftl; auto with zarith."; + pp " rewrite <- (spec_double_size x)."; + pp " generalize (spec_compare n (head0 (double_size x))); case compare; intros H1."; + pp " apply spec_shiftl; auto with zarith."; + pp " apply spec_shiftl; auto with zarith."; + pp " rewrite <- (spec_double_size (double_size x))."; + pp " apply spec_safe_shift_aux with 1%spositive." "%"; + pp " apply Zle_trans with (2 := spec_double_size_head0 (double_size x))."; + pp " replace (2 ^ 1) with (2 * 1)."; + pp " apply Zmult_le_compat_l; auto with zarith."; + pp " generalize (spec_double_size_head0_pos x); auto with zarith."; + pp " rewrite Zpower_1_r; ring."; + pp " intros x1 H2; apply spec_shiftl."; + pp " apply Zle_trans with (2 := H2)."; + pp " apply Zle_trans with (2 ^ Zpos (digits n)); auto with zarith."; + pp " case (spec_digits n); auto with zarith."; + pp " apply Zpower_le_monotone; auto with zarith."; + pp " Qed."; + pr ""; + + (* even *) + pr " Definition is_even x :="; + pr " match x with"; + for i = 0 to size do + pr " | %s%i wx => w%i_op.(znz_is_even) wx" c i i + done; + pr " | %sn n wx => (make_op n).(znz_is_even) wx" c; + pr " end."; + pr ""; + + + pr " Theorem spec_is_even: forall x,"; + pr " if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1."; + pa " Admitted."; + pp " Proof."; + pp " intros x; case x; unfold is_even, to_Z; clear x."; + for i = 0 to size do + pp " intros x; exact (spec_is_even w%i_spec x)." i; + done; + pp " intros n x; exact (spec_is_even (wn_spec n) x)."; + pp " Qed."; + pr ""; + + pr " Theorem spec_0: [zero] = 0."; + pa " Admitted."; + pp " Proof."; + pp " exact (spec_0 w0_spec)."; + pp " Qed."; + pr ""; + + pr " Theorem spec_1: [one] = 1."; + pa " Admitted."; + pp " Proof."; + pp " exact (spec_1 w0_spec)."; + pp " Qed."; + pr ""; + + pr "End Make."; + pr ""; + diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v new file mode 100644 index 00000000..ae2cfd30 --- /dev/null +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -0,0 +1,514 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: Nbasic.v 10964 2008-05-22 11:08:13Z letouzey $ i*) + +Require Import ZArith. +Require Import BigNumPrelude. +Require Import Max. +Require Import DoubleType. +Require Import DoubleBase. +Require Import CyclicAxioms. +Require Import DoubleCyclic. + +(* To compute the necessary height *) + +Fixpoint plength (p: positive) : positive := + match p with + xH => xH + | xO p1 => Psucc (plength p1) + | xI p1 => Psucc (plength p1) + end. + +Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z. +assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z). +intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z. +rewrite Zpower_exp; auto with zarith. +rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. +intros p; elim p; simpl plength; auto. +intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI. +assert (tmp: (forall p, 2 * p = p + p)%Z); + try repeat rewrite tmp; auto with zarith. +intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1). +assert (tmp: (forall p, 2 * p = p + p)%Z); + try repeat rewrite tmp; auto with zarith. +rewrite Zpower_1_r; auto with zarith. +Qed. + +Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z. +intros p; case (Psucc_pred p); intros H1. +subst; simpl plength. +rewrite Zpower_1_r; auto with zarith. +pattern p at 1; rewrite <- H1. +rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. +generalize (plength_correct (Ppred p)); auto with zarith. +Qed. + +Definition Pdiv p q := + match Zdiv (Zpos p) (Zpos q) with + Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with + Z0 => q1 + | _ => (Psucc q1) + end + | _ => xH + end. + +Theorem Pdiv_le: forall p q, + Zpos p <= Zpos q * Zpos (Pdiv p q). +intros p q. +unfold Pdiv. +assert (H1: Zpos q > 0); auto with zarith. +assert (H1b: Zpos p >= 0); auto with zarith. +generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b). +generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv. + intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl. +case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith. +intros q1 H2. +replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q). + 2: pattern (Zpos p) at 2; rewrite H2; auto with zarith. +generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; + case Zmod. + intros HH _; rewrite HH; auto with zarith. + intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism. + unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith. + intros r1 _ (HH,_); case HH; auto. +intros q1 HH; rewrite HH. +unfold Zge; simpl Zcompare; intros HH1; case HH1; auto. +Qed. + +Definition is_one p := match p with xH => true | _ => false end. + +Theorem is_one_one: forall p, is_one p = true -> p = xH. +intros p; case p; auto; intros p1 H1; discriminate H1. +Qed. + +Definition get_height digits p := + let r := Pdiv p digits in + if is_one r then xH else Psucc (plength (Ppred r)). + +Theorem get_height_correct: + forall digits N, + Zpos N <= Zpos digits * (2 ^ (Zpos (get_height digits N) -1)). +intros digits N. +unfold get_height. +assert (H1 := Pdiv_le N digits). +case_eq (is_one (Pdiv N digits)); intros H2. +rewrite (is_one_one _ H2) in H1. +rewrite Zmult_1_r in H1. +change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto. +clear H2. +apply Zle_trans with (1 := H1). +apply Zmult_le_compat_l; auto with zarith. +rewrite Zpos_succ_morphism; unfold Zsucc. +rewrite Zplus_comm; rewrite Zminus_plus. +apply plength_pred_correct. +Qed. + +Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n. + fix zn2z_word_comm 2. + intros w n; case n. + reflexivity. + intros n0;simpl. + case (zn2z_word_comm w n0). + reflexivity. +Defined. + +Fixpoint extend (n:nat) {struct n} : forall w:Type, zn2z w -> word w (S n) := + match n return forall w:Type, zn2z w -> word w (S n) with + | O => fun w x => x + | S m => + let aux := extend m in + fun w x => WW W0 (aux w x) + end. + +Section ExtendMax. + +Open Scope nat_scope. + +Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat := + match n return (n + S m = S (n + m))%nat with + | 0 => refl_equal (S m) + | S n1 => + let v := S (S n1 + m) in + eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m) + end. + +Fixpoint plusn0 n : n + 0 = n := + match n return (n + 0 = n) with + | 0 => refl_equal 0 + | S n1 => + let v := S n1 in + eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1) + end. + + Fixpoint diff (m n: nat) {struct m}: nat * nat := + match m, n with + O, n => (O, n) + | m, O => (m, O) + | S m1, S n1 => diff m1 n1 + end. + +Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n := + match m return fst (diff m n) + n = max m n with + | 0 => + match n return (n = max 0 n) with + | 0 => refl_equal _ + | S n0 => refl_equal _ + end + | S m1 => + match n return (fst (diff (S m1) n) + n = max (S m1) n) + with + | 0 => plusn0 _ + | S n1 => + let v := fst (diff m1 n1) + n1 in + let v1 := fst (diff m1 n1) + S n1 in + eq_ind v (fun n => v1 = S n) + (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _)) + _ (diff_l _ _) + end + end. + +Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n := + match m return (snd (diff m n) + m = max m n) with + | 0 => + match n return (snd (diff 0 n) + 0 = max 0 n) with + | 0 => refl_equal _ + | S _ => plusn0 _ + end + | S m => + match n return (snd (diff (S m) n) + S m = max (S m) n) with + | 0 => refl_equal (snd (diff (S m) 0) + S m) + | S n1 => + let v := S (max m n1) in + eq_ind_r (fun n => n = v) + (eq_ind_r (fun n => S n = v) + (refl_equal v) (diff_r _ _)) (plusnS _ _) + end + end. + + Variable w: Type. + + Definition castm (m n: nat) (H: m = n) (x: word w (S m)): + (word w (S n)) := + match H in (_ = y) return (word w (S y)) with + | refl_equal => x + end. + +Variable m: nat. +Variable v: (word w (S m)). + +Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) := + match n return (word w (S (n + m))) with + | O => v + | S n1 => WW W0 (extend_tr n1) + end. + +End ExtendMax. + +Implicit Arguments extend_tr[w m]. +Implicit Arguments castm[w m n]. + + + +Section Reduce. + + Variable w : Type. + Variable nT : Type. + Variable N0 : nT. + Variable eq0 : w -> bool. + Variable reduce_n : w -> nT. + Variable zn2z_to_Nt : zn2z w -> nT. + + Definition reduce_n1 (x:zn2z w) := + match x with + | W0 => N0 + | WW xh xl => + if eq0 xh then reduce_n xl + else zn2z_to_Nt x + end. + +End Reduce. + +Section ReduceRec. + + Variable w : Type. + Variable nT : Type. + Variable N0 : nT. + Variable reduce_1n : zn2z w -> nT. + Variable c : forall n, word w (S n) -> nT. + + Fixpoint reduce_n (n:nat) : word w (S n) -> nT := + match n return word w (S n) -> nT with + | O => reduce_1n + | S m => fun x => + match x with + | W0 => N0 + | WW xh xl => + match xh with + | W0 => @reduce_n m xl + | _ => @c (S m) x + end + end + end. + +End ReduceRec. + +Definition opp_compare cmp := + match cmp with + | Lt => Gt + | Eq => Eq + | Gt => Lt + end. + +Section CompareRec. + + Variable wm w : Type. + Variable w_0 : w. + Variable compare : w -> w -> comparison. + Variable compare0_m : wm -> comparison. + Variable compare_m : wm -> w -> comparison. + + Fixpoint compare0_mn (n:nat) : word wm n -> comparison := + match n return word wm n -> comparison with + | O => compare0_m + | S m => fun x => + match x with + | W0 => Eq + | WW xh xl => + match compare0_mn m xh with + | Eq => compare0_mn m xl + | r => Lt + end + end + end. + + Variable wm_base: positive. + Variable wm_to_Z: wm -> Z. + Variable w_to_Z: w -> Z. + Variable w_to_Z_0: w_to_Z w_0 = 0. + Variable spec_compare0_m: forall x, + match compare0_m x with + Eq => w_to_Z w_0 = wm_to_Z x + | Lt => w_to_Z w_0 < wm_to_Z x + | Gt => w_to_Z w_0 > wm_to_Z x + end. + Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base. + + Let double_to_Z := double_to_Z wm_base wm_to_Z. + Let double_wB := double_wB wm_base. + + Lemma base_xO: forall n, base (xO n) = (base n)^2. + Proof. + intros n1; unfold base. + rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. + Qed. + + Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n := + (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos). + + + Lemma spec_compare0_mn: forall n x, + match compare0_mn n x with + Eq => 0 = double_to_Z n x + | Lt => 0 < double_to_Z n x + | Gt => 0 > double_to_Z n x + end. + Proof. + intros n; elim n; clear n; auto. + intros x; generalize (spec_compare0_m x); rewrite w_to_Z_0; auto. + intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto. + intros xh xl. + generalize (Hrec xh); case compare0_mn; auto. + generalize (Hrec xl); case compare0_mn; auto. + simpl double_to_Z; intros H1 H2; rewrite H1; rewrite <- H2; auto. + simpl double_to_Z; intros H1 H2; rewrite <- H2; auto. + case (double_to_Z_pos n xl); auto with zarith. + intros H1; simpl double_to_Z. + set (u := DoubleBase.double_wB wm_base n). + case (double_to_Z_pos n xl); intros H2 H3. + assert (0 < u); auto with zarith. + unfold u, DoubleBase.double_wB, base; auto with zarith. + change 0 with (0 + 0); apply Zplus_lt_le_compat; auto with zarith. + apply Zmult_lt_0_compat; auto with zarith. + case (double_to_Z_pos n xh); auto with zarith. + Qed. + + Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := + match n return word wm n -> w -> comparison with + | O => compare_m + | S m => fun x y => + match x with + | W0 => compare w_0 y + | WW xh xl => + match compare0_mn m xh with + | Eq => compare_mn_1 m xl y + | r => Gt + end + end + end. + + Variable spec_compare: forall x y, + match compare x y with + Eq => w_to_Z x = w_to_Z y + | Lt => w_to_Z x < w_to_Z y + | Gt => w_to_Z x > w_to_Z y + end. + Variable spec_compare_m: forall x y, + match compare_m x y with + Eq => wm_to_Z x = w_to_Z y + | Lt => wm_to_Z x < w_to_Z y + | Gt => wm_to_Z x > w_to_Z y + end. + Variable wm_base_lt: forall x, + 0 <= w_to_Z x < base (wm_base). + + Let double_wB_lt: forall n x, + 0 <= w_to_Z x < (double_wB n). + Proof. + intros n x; elim n; simpl; auto; clear n. + intros n (H0, H); split; auto. + apply Zlt_le_trans with (1:= H). + unfold double_wB, DoubleBase.double_wB; simpl. + rewrite base_xO. + set (u := base (double_digits wm_base n)). + assert (0 < u). + unfold u, base; auto with zarith. + replace (u^2) with (u * u); simpl; auto with zarith. + apply Zle_trans with (1 * u); auto with zarith. + unfold Zpower_pos; simpl; ring. + Qed. + + + Lemma spec_compare_mn_1: forall n x y, + match compare_mn_1 n x y with + Eq => double_to_Z n x = w_to_Z y + | Lt => double_to_Z n x < w_to_Z y + | Gt => double_to_Z n x > w_to_Z y + end. + Proof. + intros n; elim n; simpl; auto; clear n. + intros n Hrec x; case x; clear x; auto. + intros y; generalize (spec_compare w_0 y); rewrite w_to_Z_0; case compare; auto. + intros xh xl y; simpl; generalize (spec_compare0_mn n xh); case compare0_mn; intros H1b. + rewrite <- H1b; rewrite Zmult_0_l; rewrite Zplus_0_l; auto. + apply Hrec. + apply Zlt_gt. + case (double_wB_lt n y); intros _ H0. + apply Zlt_le_trans with (1:= H0). + fold double_wB. + case (double_to_Z_pos n xl); intros H1 H2. + apply Zle_trans with (double_to_Z n xh * double_wB n); auto with zarith. + apply Zle_trans with (1 * double_wB n); auto with zarith. + case (double_to_Z_pos n xh); auto with zarith. + Qed. + +End CompareRec. + + +Section AddS. + + Variable w wm : Type. + Variable incr : wm -> carry wm. + Variable addr : w -> wm -> carry wm. + Variable injr : w -> zn2z wm. + + Variable w_0 u: w. + Fixpoint injs (n:nat): word w (S n) := + match n return (word w (S n)) with + O => WW w_0 u + | S n1 => (WW W0 (injs n1)) + end. + + Definition adds x y := + match y with + W0 => C0 (injr x) + | WW hy ly => match addr x ly with + C0 z => C0 (WW hy z) + | C1 z => match incr hy with + C0 z1 => C0 (WW z1 z) + | C1 z1 => C1 (WW z1 z) + end + end + end. + +End AddS. + + + Lemma spec_opp: forall u x y, + match u with + | Eq => y = x + | Lt => y < x + | Gt => y > x + end -> + match opp_compare u with + | Eq => x = y + | Lt => x < y + | Gt => x > y + end. + Proof. + intros u x y; case u; simpl; auto with zarith. + Qed. + + Fixpoint length_pos x := + match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end. + + Theorem length_pos_lt: forall x y, + (length_pos x < length_pos y)%nat -> Zpos x < Zpos y. + Proof. + intros x; elim x; clear x; [intros x1 Hrec | intros x1 Hrec | idtac]; + intros y; case y; clear y; intros y1 H || intros H; simpl length_pos; + try (rewrite (Zpos_xI x1) || rewrite (Zpos_xO x1)); + try (rewrite (Zpos_xI y1) || rewrite (Zpos_xO y1)); + try (inversion H; fail); + try (assert (Zpos x1 < Zpos y1); [apply Hrec; apply lt_S_n | idtac]; auto with zarith); + assert (0 < Zpos y1); auto with zarith; red; auto. + Qed. + + Theorem cancel_app: forall A B (f g: A -> B) x, f = g -> f x = g x. + Proof. + intros A B f g x H; rewrite H; auto. + Qed. + + + Section SimplOp. + + Variable w: Type. + + Theorem digits_zop: forall w (x: znz_op w), + znz_digits (mk_zn2z_op x) = xO (znz_digits x). + intros ww x; auto. + Qed. + + Theorem digits_kzop: forall w (x: znz_op w), + znz_digits (mk_zn2z_op_karatsuba x) = xO (znz_digits x). + intros ww x; auto. + Qed. + + Theorem make_zop: forall w (x: znz_op w), + znz_to_Z (mk_zn2z_op x) = + fun z => match z with + W0 => 0 + | WW xh xl => znz_to_Z x xh * base (znz_digits x) + + znz_to_Z x xl + end. + intros ww x; auto. + Qed. + + Theorem make_kzop: forall w (x: znz_op w), + znz_to_Z (mk_zn2z_op_karatsuba x) = + fun z => match z with + W0 => 0 + | WW xh xl => znz_to_Z x xh * base (znz_digits x) + + znz_to_Z x xl + end. + intros ww x; auto. + Qed. + + End SimplOp. diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v new file mode 100644 index 00000000..fc2bd2df --- /dev/null +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -0,0 +1,267 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NBinDefs.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import BinPos. +Require Export BinNat. +Require Import NSub. + +Open Local Scope N_scope. + +(** Implementation of [NAxiomsSig] module type via [BinNat.N] *) + +Module NBinaryAxiomsMod <: NAxiomsSig. +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := N. +Definition NZeq := @eq N. +Definition NZ0 := N0. +Definition NZsucc := Nsucc. +Definition NZpred := Npred. +Definition NZadd := Nplus. +Definition NZsub := Nminus. +Definition NZmul := Nmult. + +Theorem NZeq_equiv : equiv N NZeq. +Proof (eq_equiv N). + +Add Relation N NZeq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) +as NZeq_rel. + +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Proof. +congruence. +Qed. + +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Proof. +congruence. +Qed. + +Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Proof. +congruence. +Qed. + +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. +Proof. +congruence. +Qed. + +Theorem NZinduction : + forall A : NZ -> Prop, predicate_wd NZeq A -> + A N0 -> (forall n, A n <-> A (NZsucc n)) -> forall n : NZ, A n. +Proof. +intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS. +Qed. + +Theorem NZpred_succ : forall n : NZ, NZpred (NZsucc n) = n. +Proof. +destruct n as [| p]; simpl. reflexivity. +case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ). +intro H; false_hyp H Psucc_not_one. +Qed. + +Theorem NZadd_0_l : forall n : NZ, N0 + n = n. +Proof. +reflexivity. +Qed. + +Theorem NZadd_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m). +Proof. +destruct n; destruct m. +simpl in |- *; reflexivity. +unfold NZsucc, NZadd, Nsucc, Nplus. rewrite <- Pplus_one_succ_l; reflexivity. +simpl in |- *; reflexivity. +simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. +Qed. + +Theorem NZsub_0_r : forall n : NZ, n - N0 = n. +Proof. +now destruct n. +Qed. + +Theorem NZsub_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m). +Proof. +destruct n as [| p]; destruct m as [| q]; try reflexivity. +now destruct p. +simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. +now destruct (Pminus_mask p q) as [| r |]; [| destruct r |]. +Qed. + +Theorem NZmul_0_l : forall n : NZ, N0 * n = N0. +Proof. +destruct n; reflexivity. +Qed. + +Theorem NZmul_succ_l : forall n m : NZ, (NZsucc n) * m = n * m + m. +Proof. +destruct n as [| n]; destruct m as [| m]; simpl; try reflexivity. +now rewrite Pmult_Sn_m, Pplus_comm. +Qed. + +End NZAxiomsMod. + +Definition NZlt := Nlt. +Definition NZle := Nle. +Definition NZmin := Nmin. +Definition NZmax := Nmax. + +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. +Proof. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. +Proof. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. +Proof. +congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m. +Proof. +intros n m. unfold Nle, Nlt. rewrite <- Ncompare_eq_correct. +destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now right. +now elim H1. destruct H1; discriminate. +Qed. + +Theorem NZlt_irrefl : forall n : NZ, ~ n < n. +Proof. +intro n; unfold Nlt; now rewrite Ncompare_refl. +Qed. + +Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m. +Proof. +intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl; +split; intro H; try reflexivity; try discriminate. +destruct p; simpl; intros; discriminate. elimtype False; now apply H. +apply -> Pcompare_p_Sq in H. destruct H as [H | H]. +now rewrite H. now rewrite H, Pcompare_refl. +apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1. +right; now apply Pcompare_Eq_eq. now left. elimtype False; now apply H. +Qed. + +Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n. +Proof. +unfold NZmin, Nmin, Nle; intros n m H. +destruct (n ?= m); try reflexivity. now elim H. +Qed. + +Theorem NZmin_r : forall n m : N, m <= n -> NZmin n m = m. +Proof. +unfold NZmin, Nmin, Nle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +now apply -> Ncompare_eq_correct. +rewrite <- Ncompare_antisym, H1 in H; elim H; auto. +Qed. + +Theorem NZmax_l : forall n m : N, m <= n -> NZmax n m = n. +Proof. +unfold NZmax, Nmax, Nle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +symmetry; now apply -> Ncompare_eq_correct. +rewrite <- Ncompare_antisym, H1 in H; elim H; auto. +Qed. + +Theorem NZmax_r : forall n m : N, n <= m -> NZmax n m = m. +Proof. +unfold NZmax, Nmax, Nle; intros n m H. +destruct (n ?= m); try reflexivity. now elim H. +Qed. + +End NZOrdAxiomsMod. + +Definition recursion (A : Type) (a : A) (f : N -> A -> A) (n : N) := + Nrect (fun _ => A) a f n. +Implicit Arguments recursion [A]. + +Theorem pred_0 : Npred N0 = N0. +Proof. +reflexivity. +Qed. + +Theorem recursion_wd : +forall (A : Type) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' -> + forall x x' : N, x = x' -> + Aeq (recursion a f x) (recursion a' f' x'). +Proof. +unfold fun2_wd, NZeq, fun2_eq. +intros A Aeq a a' Eaa' f f' Eff'. +intro x; pattern x; apply Nrect. +intros x' H; now rewrite <- H. +clear x. +intros x IH x' H; rewrite <- H. +unfold recursion in *. do 2 rewrite Nrect_step. +now apply Eff'; [| apply IH]. +Qed. + +Theorem recursion_0 : + forall (A : Type) (a : A) (f : N -> A -> A), recursion a f N0 = a. +Proof. +intros A a f; unfold recursion; now rewrite Nrect_base. +Qed. + +Theorem recursion_succ : + forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A), + Aeq a a -> fun2_wd NZeq Aeq Aeq f -> + forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)). +Proof. +unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect. +rewrite Nrect_step; rewrite Nrect_base; now apply f_wd. +clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|]. +now rewrite Nrect_step. +Qed. + +End NBinaryAxiomsMod. + +Module Export NBinarySubPropMod := NSubPropFunct NBinaryAxiomsMod. + +(* Some fun comparing the efficiency of the generic log defined +by strong (course-of-value) recursion and the log defined by recursion +on notation *) +(* Time Eval compute in (log 100000). *) (* 98 sec *) + +(* +Fixpoint binposlog (p : positive) : N := +match p with +| xH => 0 +| xO p' => Nsucc (binposlog p') +| xI p' => Nsucc (binposlog p') +end. + +Definition binlog (n : N) : N := +match n with +| 0 => 0 +| Npos p => binposlog p +end. +*) +(* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *) + diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v new file mode 100644 index 00000000..2c99128d --- /dev/null +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NBinary.v 10934 2008-05-15 21:58:20Z letouzey $ i*) + +Require Export NBinDefs. +Require Export NArithRing. + diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v new file mode 100644 index 00000000..1c83da45 --- /dev/null +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -0,0 +1,220 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NPeano.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import Arith. +Require Import Min. +Require Import Max. +Require Import NSub. + +Module NPeanoAxiomsMod <: NAxiomsSig. +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := nat. +Definition NZeq := (@eq nat). +Definition NZ0 := 0. +Definition NZsucc := S. +Definition NZpred := pred. +Definition NZadd := plus. +Definition NZsub := minus. +Definition NZmul := mult. + +Theorem NZeq_equiv : equiv nat NZeq. +Proof (eq_equiv nat). + +Add Relation nat NZeq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) +as NZeq_rel. + +(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZeq" +then the theorem generated for succ_wd below is forall x, succ x = succ x, +which does not match the axioms in NAxiomsSig *) + +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Proof. +congruence. +Qed. + +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Proof. +congruence. +Qed. + +Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Proof. +congruence. +Qed. + +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. +Proof. +congruence. +Qed. + +Theorem NZinduction : + forall A : nat -> Prop, predicate_wd (@eq nat) A -> + A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n. +Proof. +intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS. +Qed. + +Theorem NZpred_succ : forall n : nat, pred (S n) = n. +Proof. +reflexivity. +Qed. + +Theorem NZadd_0_l : forall n : nat, 0 + n = n. +Proof. +reflexivity. +Qed. + +Theorem NZadd_succ_l : forall n m : nat, (S n) + m = S (n + m). +Proof. +reflexivity. +Qed. + +Theorem NZsub_0_r : forall n : nat, n - 0 = n. +Proof. +intro n; now destruct n. +Qed. + +Theorem NZsub_succ_r : forall n m : nat, n - (S m) = pred (n - m). +Proof. +intros n m; induction n m using nat_double_ind; simpl; auto. apply NZsub_0_r. +Qed. + +Theorem NZmul_0_l : forall n : nat, 0 * n = 0. +Proof. +reflexivity. +Qed. + +Theorem NZmul_succ_l : forall n m : nat, S n * m = n * m + m. +Proof. +intros n m; now rewrite plus_comm. +Qed. + +End NZAxiomsMod. + +Definition NZlt := lt. +Definition NZle := le. +Definition NZmin := min. +Definition NZmax := max. + +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. +Proof. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. +Proof. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. +Proof. +congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m. +Proof. +intros n m; split. +apply le_lt_or_eq. +intro H; destruct H as [H | H]. +now apply lt_le_weak. rewrite H; apply le_refl. +Qed. + +Theorem NZlt_irrefl : forall n : nat, ~ (n < n). +Proof. +exact lt_irrefl. +Qed. + +Theorem NZlt_succ_r : forall n m : nat, n < S m <-> n <= m. +Proof. +intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm]. +Qed. + +Theorem NZmin_l : forall n m : nat, n <= m -> NZmin n m = n. +Proof. +exact min_l. +Qed. + +Theorem NZmin_r : forall n m : nat, m <= n -> NZmin n m = m. +Proof. +exact min_r. +Qed. + +Theorem NZmax_l : forall n m : nat, m <= n -> NZmax n m = n. +Proof. +exact max_l. +Qed. + +Theorem NZmax_r : forall n m : nat, n <= m -> NZmax n m = m. +Proof. +exact max_r. +Qed. + +End NZOrdAxiomsMod. + +Definition recursion : forall A : Type, A -> (nat -> A -> A) -> nat -> A := + fun A : Type => nat_rect (fun _ => A). +Implicit Arguments recursion [A]. + +Theorem succ_neq_0 : forall n : nat, S n <> 0. +Proof. +intros; discriminate. +Qed. + +Theorem pred_0 : pred 0 = 0. +Proof. +reflexivity. +Qed. + +Theorem recursion_wd : forall (A : Type) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' -> + forall n n' : nat, n = n' -> + Aeq (recursion a f n) (recursion a' f' n'). +Proof. +unfold fun2_eq; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto. +Qed. + +Theorem recursion_0 : + forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a. +Proof. +reflexivity. +Qed. + +Theorem recursion_succ : + forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A), + Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f -> + forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). +Proof. +induction n; simpl; auto. +Qed. + +End NPeanoAxiomsMod. + +(* Now we apply the largest property functor *) + +Module Export NPeanoSubPropMod := NSubPropFunct NPeanoAxiomsMod. + diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v new file mode 100644 index 00000000..0275d1e1 --- /dev/null +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -0,0 +1,115 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NSig.v 11027 2008-06-01 13:28:59Z letouzey $ i*) + +Require Import ZArith Znumtheory. + +Open Scope Z_scope. + +(** * NSig *) + +(** Interface of a rich structure about natural numbers. + Specifications are written via translation to Z. +*) + +Module Type NType. + + Parameter t : Type. + + Parameter to_Z : t -> Z. + Notation "[ x ]" := (to_Z x). + Parameter spec_pos: forall x, 0 <= [x]. + + Parameter of_N : N -> t. + Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x. + Definition to_N n := Zabs_N (to_Z n). + + Definition eq n m := ([n] = [m]). + + Parameter zero : t. + Parameter one : t. + + Parameter spec_0: [zero] = 0. + Parameter spec_1: [one] = 1. + + Parameter compare : t -> t -> comparison. + + Parameter spec_compare: forall x y, + match compare x y with + | Eq => [x] = [y] + | Lt => [x] < [y] + | Gt => [x] > [y] + end. + + Definition lt n m := compare n m = Lt. + Definition le n m := compare n m <> Gt. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + + Parameter eq_bool : t -> t -> bool. + + Parameter spec_eq_bool: forall x y, + if eq_bool x y then [x] = [y] else [x] <> [y]. + + Parameter succ : t -> t. + + Parameter spec_succ: forall n, [succ n] = [n] + 1. + + Parameter add : t -> t -> t. + + Parameter spec_add: forall x y, [add x y] = [x] + [y]. + + Parameter pred : t -> t. + + Parameter spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1. + Parameter spec_pred0: forall x, [x] = 0 -> [pred x] = 0. + + Parameter sub : t -> t -> t. + + Parameter spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y]. + Parameter spec_sub0: forall x y, [x] < [y]-> [sub x y] = 0. + + Parameter mul : t -> t -> t. + + Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. + + Parameter square : t -> t. + + Parameter spec_square: forall x, [square x] = [x] * [x]. + + Parameter power_pos : t -> positive -> t. + + Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + + Parameter sqrt : t -> t. + + Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + + Parameter div_eucl : t -> t -> t * t. + + Parameter spec_div_eucl: forall x y, + 0 < [y] -> + let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. + + Parameter div : t -> t -> t. + + Parameter spec_div: forall x y, 0 < [y] -> [div x y] = [x] / [y]. + + Parameter modulo : t -> t -> t. + + Parameter spec_modulo: + forall x y, 0 < [y] -> [modulo x y] = [x] mod [y]. + + Parameter gcd : t -> t -> t. + + Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + +End NType. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v new file mode 100644 index 00000000..fe068437 --- /dev/null +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -0,0 +1,356 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: NSigNAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import ZArith. +Require Import Nnat. +Require Import NAxioms. +Require Import NSig. + +(** * The interface [NSig.NType] implies the interface [NAxiomsSig] *) + +Module NSig_NAxioms (N:NType) <: NAxiomsSig. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with N.t. +Open Local Scope IntScope. +Notation "[ x ]" := (N.to_Z x) : IntScope. +Infix "==" := N.eq (at level 70) : IntScope. +Notation "0" := N.zero : IntScope. +Infix "+" := N.add : IntScope. +Infix "-" := N.sub : IntScope. +Infix "*" := N.mul : IntScope. + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := N.t. +Definition NZeq := N.eq. +Definition NZ0 := N.zero. +Definition NZsucc := N.succ. +Definition NZpred := N.pred. +Definition NZadd := N.add. +Definition NZsub := N.sub. +Definition NZmul := N.mul. + +Theorem NZeq_equiv : equiv N.t N.eq. +Proof. +repeat split; repeat red; intros; auto; congruence. +Qed. + +Add Relation N.t N.eq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) + as NZeq_rel. + +Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd. +Proof. +unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto. +Qed. + +Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd. +Proof. +unfold N.eq; intros. +generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0). +destruct N.eq_bool; rewrite N.spec_0; intros. +rewrite 2 N.spec_pred0; congruence. +rewrite 2 N.spec_pred; f_equal; auto; try omega. +Qed. + +Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd. +Proof. +unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto. +Qed. + +Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd. +Proof. +unfold N.eq; intros x x' Hx y y' Hy. +destruct (Z_lt_le_dec [x] [y]). +rewrite 2 N.spec_sub0; f_equal; congruence. +rewrite 2 N.spec_sub; f_equal; congruence. +Qed. + +Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd. +Proof. +unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto. +Qed. + +Theorem NZpred_succ : forall n, N.pred (N.succ n) == n. +Proof. +unfold N.eq; intros. +rewrite N.spec_pred; rewrite N.spec_succ. +omega. +generalize (N.spec_pos n); omega. +Qed. + +Definition N_of_Z z := N.of_N (Zabs_N z). + +Section Induction. + +Variable A : N.t -> Prop. +Hypothesis A_wd : predicate_wd N.eq A. +Hypothesis A0 : A 0. +Hypothesis AS : forall n, A n <-> A (N.succ n). + +Add Morphism A with signature N.eq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +Let B (z : Z) := A (N_of_Z z). + +Lemma B0 : B 0. +Proof. +unfold B, N_of_Z; simpl. +rewrite <- (A_wd 0); auto. +red; rewrite N.spec_0, N.spec_of_N; auto. +Qed. + +Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1). +Proof. +intros z H1 H2. +unfold B in *. apply -> AS in H2. +setoid_replace (N_of_Z (z + 1)) with (N.succ (N_of_Z z)); auto. +unfold N.eq. rewrite N.spec_succ. +unfold N_of_Z. +rewrite 2 N.spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith. +Qed. + +Lemma B_holds : forall z : Z, (0 <= z)%Z -> B z. +Proof. +exact (natlike_ind B B0 BS). +Qed. + +Theorem NZinduction : forall n, A n. +Proof. +intro n. setoid_replace n with (N_of_Z (N.to_Z n)). +apply B_holds. apply N.spec_pos. +red; unfold N_of_Z. +rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto. +apply N.spec_pos. +Qed. + +End Induction. + +Theorem NZadd_0_l : forall n, 0 + n == n. +Proof. +intros; red; rewrite N.spec_add, N.spec_0; auto with zarith. +Qed. + +Theorem NZadd_succ_l : forall n m, (N.succ n) + m == N.succ (n + m). +Proof. +intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith. +Qed. + +Theorem NZsub_0_r : forall n, n - 0 == n. +Proof. +intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith. +apply N.spec_pos. +Qed. + +Theorem NZsub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m). +Proof. +intros; red. +destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H]. +rewrite N.spec_sub0; auto. +rewrite N.spec_succ in H. +rewrite N.spec_pred0; auto. +destruct (Z_eq_dec [n] [m]). +rewrite N.spec_sub; auto with zarith. +rewrite N.spec_sub0; auto with zarith. + +rewrite N.spec_sub, N.spec_succ in *; auto. +rewrite N.spec_pred, N.spec_sub; auto with zarith. +rewrite N.spec_sub; auto with zarith. +Qed. + +Theorem NZmul_0_l : forall n, 0 * n == 0. +Proof. +intros; red. +rewrite N.spec_mul, N.spec_0; auto with zarith. +Qed. + +Theorem NZmul_succ_l : forall n m, (N.succ n) * m == n * m + m. +Proof. +intros; red. +rewrite N.spec_add, 2 N.spec_mul, N.spec_succ; ring. +Qed. + +End NZAxiomsMod. + +Definition NZlt := N.lt. +Definition NZle := N.le. +Definition NZmin := N.min. +Definition NZmax := N.max. + +Infix "<=" := N.le : IntScope. +Infix "<" := N.lt : IntScope. + +Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z. +Proof. + intros; generalize (N.spec_compare x y). + destruct (N.compare x y); auto. + intros H; rewrite H; symmetry; apply Zcompare_refl. +Qed. + +Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. +Proof. + intros; unfold N.lt, Zlt; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. +Proof. + intros; unfold N.le, Zle; rewrite spec_compare_alt; intuition. +Qed. + +Lemma spec_min : forall x y, [N.min x y] = Zmin [x] [y]. +Proof. + intros; unfold N.min, Zmin. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Lemma spec_max : forall x y, [N.max x y] = Zmax [x] [y]. +Proof. + intros; unfold N.max, Zmax. + rewrite spec_compare_alt; destruct Zcompare; auto. +Qed. + +Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd. +Proof. +intros x x' Hx y y' Hy. +rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd. +Proof. +intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd. +Proof. +intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition. +Qed. + +Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd. +Proof. +intros; red; rewrite 2 spec_min; congruence. +Qed. + +Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd. +Proof. +intros; red; rewrite 2 spec_max; congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. +Proof. +intros. +unfold N.eq; rewrite spec_lt, spec_le; omega. +Qed. + +Theorem NZlt_irrefl : forall n, ~ n < n. +Proof. +intros; rewrite spec_lt; auto with zarith. +Qed. + +Theorem NZlt_succ_r : forall n m, n < (N.succ m) <-> n <= m. +Proof. +intros; rewrite spec_lt, spec_le, N.spec_succ; omega. +Qed. + +Theorem NZmin_l : forall n m, n <= m -> N.min n m == n. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmin_r : forall n m, m <= n -> N.min n m == m. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_min. +generalize (Zmin_spec [n] [m]); omega. +Qed. + +Theorem NZmax_l : forall n m, m <= n -> N.max n m == n. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +Theorem NZmax_r : forall n m, n <= m -> N.max n m == m. +Proof. +intros n m; unfold N.eq; rewrite spec_le, spec_max. +generalize (Zmax_spec [n] [m]); omega. +Qed. + +End NZOrdAxiomsMod. + +Theorem pred_0 : N.pred 0 == 0. +Proof. +red; rewrite N.spec_pred0; rewrite N.spec_0; auto. +Qed. + +Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) := + Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n). +Implicit Arguments recursion [A]. + +Theorem recursion_wd : +forall (A : Type) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' -> + forall x x' : N.t, x == x' -> + Aeq (recursion a f x) (recursion a' f' x'). +Proof. +unfold fun2_wd, N.eq, fun2_eq. +intros A Aeq a a' Eaa' f f' Eff' x x' Exx'. +unfold recursion. +unfold N.to_N. +rewrite <- Exx'; clear x' Exx'. +replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])). +induction (Zabs_nat [x]). +simpl; auto. +rewrite N_of_S, 2 Nrect_step; auto. +destruct [x]; simpl; auto. +change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N. +change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N. +Qed. + +Theorem recursion_0 : + forall (A : Type) (a : A) (f : N.t -> A -> A), recursion a f 0 = a. +Proof. +intros A a f; unfold recursion, N.to_N; rewrite N.spec_0; simpl; auto. +Qed. + +Theorem recursion_succ : + forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A), + Aeq a a -> fun2_wd N.eq Aeq Aeq f -> + forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)). +Proof. +unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n. +replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)). +rewrite Nrect_step. +apply f_wd; auto. +unfold N.to_N. +rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto. + apply N.spec_pos. + +fold (recursion a f n). +apply recursion_wd; auto. +red; auto. +red; auto. +unfold N.to_N. + +rewrite N.spec_succ. +change ([n]+1)%Z with (Zsucc [n]). +apply Z_of_N_eq_rev. +rewrite Z_of_N_succ. +rewrite 2 Z_of_N_abs. +rewrite 2 Zabs_eq; auto. +generalize (N.spec_pos n); auto with zarith. +apply N.spec_pos; auto. +Qed. + +End NSig_NAxioms. |