diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 115 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 356 |
2 files changed, 471 insertions, 0 deletions
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. |