diff options
Diffstat (limited to 'theories/Numbers')
31 files changed, 265 insertions, 124 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 627235252..fd192dce6 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -31,6 +31,8 @@ Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99). Definition eq (n m : t) := [| n |] = [| m |]. Definition zero := ZnZ.zero. +Definition one := ZnZ.one. +Definition two := ZnZ.succ ZnZ.one. Definition succ := ZnZ.succ. Definition pred := ZnZ.pred. Definition add := ZnZ.add. @@ -45,10 +47,10 @@ Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. -Hint Rewrite ZnZ.spec_0 ZnZ.spec_succ ZnZ.spec_pred +Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. Ltac zify := - unfold eq, zero, succ, pred, add, sub, mul in *; + unfold eq, zero, one, two, succ, pred, add, sub, mul in *; autorewrite with cyclic. Ltac zcongruence := repeat red; intros; zify; congruence. @@ -75,20 +77,19 @@ Proof. pose proof gt_wB_1; auto with zarith. Qed. +Lemma one_mod_wB : 1 mod wB = 1. +Proof. +rewrite Zmod_small. reflexivity. split. auto with zarith. apply gt_wB_1. +Qed. + Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB. Proof. -intro n. -pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zplus_mod. -reflexivity. -now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]]. +intro n. rewrite <- one_mod_wB at 2. now rewrite <- Zplus_mod. Qed. Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB. Proof. -intro n. -pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zminus_mod. -reflexivity. -now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]]. +intro n. rewrite <- one_mod_wB at 2. now rewrite Zminus_mod. Qed. Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |]. @@ -103,6 +104,16 @@ rewrite <- pred_mod_wB. replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod. Qed. +Theorem one_succ : one == succ zero. +Proof. +zify; simpl. now rewrite one_mod_wB. +Qed. + +Theorem two_succ : two == succ one. +Proof. +reflexivity. +Qed. + Section Induction. Variable A : t -> Prop. diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index eb27e6378..b5ca908b4 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -102,6 +102,11 @@ Proof. intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0. Qed. +Theorem lt_m1_0 : -(1) < 0. +Proof. +apply opp_neg_pos, lt_0_1. +Qed. + Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n. Proof. intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 540e17cb4..23eac0e69 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -125,7 +125,7 @@ Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1). Proof. intros n m H1 H2. apply -> lt_le_pred in H2. setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m. -apply <- eq_opp_r. now rewrite opp_pred, opp_0. +apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0. Qed. End ZOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 76428584d..25989b2d4 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -177,22 +177,16 @@ Qed. Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1. Proof. -assert (F : ~ 1 < -1). -intro H. -assert (H1 : -1 < 0). apply <- opp_neg_pos. apply lt_succ_diag_r. -assert (H2 : 1 < 0) by now apply lt_trans with (-1). -false_hyp H2 nlt_succ_diag_l. +assert (F := lt_m1_0). zero_pos_neg n. -intros m H; rewrite mul_0_l in H; false_hyp H neq_succ_diag_r. -intros n H; split; apply <- le_succ_l in H; le_elim H. -intros m H1; apply (lt_1_mul_l n m) in H. -rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H F. false_hyp H neq_succ_diag_l. false_hyp H lt_irrefl. -intros; now left. -intros m H1; apply (lt_1_mul_l n m) in H. rewrite mul_opp_l in H1; -apply -> eq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H lt_irrefl. apply -> eq_opp_l in H. rewrite opp_0 in H. -false_hyp H neq_succ_diag_l. false_hyp H F. +(* n = 0 *) +intros m. nzsimpl. now left. +(* 0 < n, proving P n /\ P (-n) *) +intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. +le_elim Hn; split; intros m H. +destruct (lt_1_mul_l n m) as [|[|]]; order'. +rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'. +now left. intros; right; symmetry; now apply opp_wd. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 1ababfe5c..4c752043c 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -41,20 +41,20 @@ Proof. intros x. split; intros [(y,H)|(y,H)]. right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl. + left. exists (S y). rewrite H. now nzsimpl'. right. exists (P y). rewrite <- succ_inj_wd. rewrite H. - nzsimpl. now rewrite <- add_succ_l, <- add_succ_r, succ_pred. + nzsimpl'. now rewrite <- add_succ_l, <- add_succ_r, succ_pred. left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. Qed. Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1. Proof. - intros. nzsimpl. apply lt_succ_r. now apply add_le_mono. + intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono. Qed. Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m. Proof. - intros. nzsimpl. + intros. nzsimpl'. rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r. apply add_le_mono; now apply le_succ_l. Qed. @@ -95,7 +95,7 @@ Qed. Lemma odd_1 : odd 1 = true. Proof. - rewrite odd_spec. exists 0. now nzsimpl. + rewrite odd_spec. exists 0. now nzsimpl'. Qed. Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n. @@ -140,7 +140,7 @@ Proof. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1. + exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 9de681375..782a11024 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -78,12 +78,10 @@ Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b. Proof. intros a b (c,H). rewrite H. destruct (le_gt_cases 0 c). - assert (0 <= 2) by (apply le_le_succ_r, le_0_1). - rewrite 2 pow_mul_r; trivial. + rewrite 2 pow_mul_r by order'. rewrite 2 pow_2_r. now rewrite mul_opp_opp. - assert (2*c < 0). - apply mul_pos_neg; trivial. rewrite lt_succ_r. apply le_0_1. + assert (2*c < 0) by (apply mul_pos_neg; order'). now rewrite !pow_neg. Qed. @@ -91,10 +89,8 @@ Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b). Proof. intros a b (c,H). rewrite H. destruct (le_gt_cases 0 c) as [LE|GT]. - assert (0 <= 2*c). - apply mul_nonneg_nonneg; trivial. - apply le_le_succ_r, le_0_1. - rewrite add_succ_r, add_0_r, !pow_succ_r; trivial. + assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order'). + rewrite add_1_r, !pow_succ_r; trivial. rewrite pow_opp_even by (now exists c). apply mul_opp_l. apply double_above in GT. rewrite mul_0_r in GT. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 6c9dc77c1..92be49bda 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -70,6 +70,7 @@ Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope]. Local Notation "0" := BigZ.zero : bigZ_scope. Local Notation "1" := BigZ.one : bigZ_scope. +Local Notation "2" := BigZ.two : bigZ_scope. Infix "+" := BigZ.add : bigZ_scope. Infix "-" := BigZ.sub : bigZ_scope. Notation "- x" := (BigZ.opp x) : bigZ_scope. @@ -171,6 +172,7 @@ Ltac isBigZcst t := | BigZ.Neg ?t => isBigNcst t | BigZ.zero => constr:true | BigZ.one => constr:true + | BigZ.two => constr:true | BigZ.minus_one => constr:true | _ => constr:false end. @@ -186,6 +188,7 @@ Ltac BigZ_to_N t := | BigZ.Pos ?t => BigN_to_N t | BigZ.zero => constr:0%N | BigZ.one => constr:1%N + | BigZ.two => constr:2%N | _ => constr:NotConstant end. @@ -198,7 +201,6 @@ Add Ring BigZr : BigZring div BigZdiv). Section TestRing. -Local Notation "2" := (BigZ.Pos (BigN.N0 2%int31)) : bigZ_scope. Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x. Proof. intros. ring_simplify. reflexivity. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index fb760bdf5..f9490cc9c 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -31,6 +31,7 @@ Module Make (N:NType) <: ZType. Definition zero := Pos N.zero. Definition one := Pos N.one. + Definition two := Pos N.two. Definition minus_one := Neg N.one. Definition of_Z x := @@ -64,6 +65,10 @@ Module Make (N:NType) <: ZType. exact N.spec_1. Qed. + Theorem spec_2: to_Z two = 2. + exact N.spec_2. + Qed. + Theorem spec_m1: to_Z minus_one = -1. simpl; rewrite N.spec_1; auto. Qed. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 28a37abf8..5f8728394 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -63,6 +63,8 @@ Module Z Definition t := Z. Definition eqb := Zeq_bool. Definition zero := 0. +Definition one := 1. +Definition two := 2. Definition succ := Zsucc. Definition pred := Zpred. Definition add := Zplus. @@ -99,6 +101,16 @@ Definition sub_succ_r := Zminus_succ_r. Definition mul_0_l := Zmult_0_l. Definition mul_succ_l := Zmult_succ_l. +Lemma one_succ : 1 = Zsucc 0. +Proof. +reflexivity. +Qed. + +Lemma two_succ : 2 = Zsucc 1. +Proof. +reflexivity. +Qed. + (** Boolean Equality *) Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y). diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 7df1871e1..ab555ca32 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -25,7 +25,8 @@ Bind Scope NScope with N.t. Infix "==" := N.eq (at level 70) : NScope. Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope. Notation "0" := N.zero : NScope. -Notation "1" := (N.succ N.zero) : NScope. +Notation "1" := N.one : NScope. +Notation "2" := N.two : NScope. Infix "+" := N.add : NScope. Infix "-" := N.sub : NScope. Infix "*" := N.mul : NScope. @@ -43,6 +44,8 @@ Module Z. Definition t := (N.t * N.t)%type. Definition zero : t := (0, 0). +Definition one : t := (1,0). +Definition two : t := (2,0). Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2). Definition succ (n : t) : t := (N.succ n#1, n#2). Definition pred (n : t) : t := (n#1, N.succ n#2). @@ -73,7 +76,8 @@ Bind Scope ZScope with Z.t. Infix "==" := Z.eq (at level 70) : ZScope. Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope. Notation "0" := Z.zero : ZScope. -Notation "1" := (Z.succ Z.zero) : ZScope. +Notation "1" := Z.one : ZScope. +Notation "2" := Z.two : ZScope. Infix "+" := Z.add : ZScope. Infix "-" := Z.sub : ZScope. Infix "*" := Z.mul : ZScope. @@ -159,20 +163,22 @@ Hypothesis A_wd : Proper (Z.eq==>iff) A. Theorem bi_induction : A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n. Proof. +Open Scope NScope. intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *. destruct n as [n m]. -cut (forall p, A (p, 0%N)); [intro H1 |]. -cut (forall p, A (0%N, p)); [intro H2 |]. +cut (forall p, A (p, 0)); [intro H1 |]. +cut (forall p, A (0, p)); [intro H2 |]. destruct (add_dichotomy n m) as [[p H] | [p H]]. -rewrite (A_wd (n, m) (0%N, p)) by (rewrite add_0_l; now rewrite add_comm). +rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm). apply H2. -rewrite (A_wd (n, m) (p, 0%N)) by now rewrite add_0_r. apply H1. +rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1. induct p. assumption. intros p IH. -apply -> (A_wd (0%N, p) (1%N, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. -now apply <- AS. +apply -> (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. +rewrite one_succ in IH. now apply <- AS. induct p. assumption. intros p IH. -replace 0%N with (snd (p, 0%N)); [| reflexivity]. -replace (N.succ p) with (N.succ (fst (p, 0%N))); [| reflexivity]. now apply -> AS. +replace 0 with (snd (p, 0)); [| reflexivity]. +replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS. +Close Scope NScope. Qed. End Induction. @@ -189,6 +195,16 @@ Proof. intro n; unfold Z.succ, Z.pred, Z.eq; simpl; now nzsimpl. Qed. +Theorem one_succ : 1 == Z.succ 0. +Proof. +unfold Z.eq; simpl. now nzsimpl'. +Qed. + +Theorem two_succ : 2 == Z.succ 1. +Proof. +unfold Z.eq; simpl. now nzsimpl'. +Qed. + Theorem opp_0 : - 0 == 0. Proof. unfold Z.opp, Z.eq; simpl. now nzsimpl. @@ -297,6 +313,8 @@ Qed. Definition t := Z.t. Definition eq := Z.eq. Definition zero := Z.zero. +Definition one := Z.one. +Definition two := Z.two. Definition succ := Z.succ. Definition pred := Z.pred. Definition add := Z.add. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index b33ed5f8e..be201f2d6 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -38,6 +38,7 @@ Module Type ZType. Parameter max : t -> t -> t. Parameter zero : t. Parameter one : t. + Parameter two : t. Parameter minus_one : t. Parameter succ : t -> t. Parameter add : t -> t -> t. @@ -65,6 +66,7 @@ Module Type ZType. Parameter spec_max : forall x y, [max x y] = Zmax [x] [y]. Parameter spec_0: [zero] = 0. Parameter spec_1: [one] = 1. + Parameter spec_2: [two] = 2. Parameter spec_m1: [minus_one] = -1. Parameter spec_succ: forall n, [succ n] = [n] + 1. Parameter spec_add: forall x y, [add x y] = [x] + [y]. @@ -94,6 +96,8 @@ Module Type ZType_Notation (Import Z:ZType). Notation "[ x ]" := (to_Z x). Infix "==" := eq (at level 70). Notation "0" := zero. + Notation "1" := one. + Notation "2" := two. Infix "+" := add. Infix "-" := sub. Infix "*" := mul. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 90bda6343..3e6375543 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -17,7 +17,7 @@ Require Import ZArith Nnat ZAxioms ZDivFloor ZSig. Module ZTypeIsZAxioms (Import Z : ZType'). Hint Rewrite - spec_0 spec_1 spec_add spec_sub spec_pred spec_succ + spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn spec_pow spec_even spec_odd @@ -43,6 +43,16 @@ Proof. intros. zify. auto with zarith. Qed. +Theorem one_succ : 1 == succ 0. +Proof. +now zify. +Qed. + +Theorem two_succ : 2 == succ 1. +Proof. +now zify. +Qed. + Section Induction. Variable A : Z.t -> Prop. @@ -225,12 +235,12 @@ Proof. intros n. zify. omega with *. Qed. -Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0. +Theorem sgn_pos : forall n, 0<n -> sgn n == 1. Proof. intros n. zify. omega with *. Qed. -Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0). +Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1. Proof. intros n. zify. omega with *. Qed. @@ -239,9 +249,6 @@ Qed. Program Instance pow_wd : Proper (eq==>eq==>eq) pow. -Local Notation "1" := (succ 0). -Local Notation "2" := (succ 1). - Lemma pow_0_r : forall a, a^0 == 1. Proof. intros. now zify. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 7d7cc4ac5..202875b8a 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -14,7 +14,9 @@ Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. +Hint Rewrite one_succ two_succ : nz'. Ltac nzsimpl := autorewrite with nz. +Ltac nzsimpl' := autorewrite with nz nz'. Theorem add_0_r : forall n, n + 0 == n. Proof. @@ -38,14 +40,16 @@ Qed. Theorem add_1_l : forall n, 1 + n == S n. Proof. -intro n; now nzsimpl. +intro n; now nzsimpl'. Qed. Theorem add_1_r : forall n, n + 1 == S n. Proof. -intro n; now nzsimpl. +intro n; now nzsimpl'. Qed. +Hint Rewrite add_1_l add_1_r : nz. + Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. intros n m p; nzinduct n. now nzsimpl. @@ -80,7 +84,9 @@ Qed. Theorem sub_1_r : forall n, n - 1 == P n. Proof. -intro n; now nzsimpl. +intro n; now nzsimpl'. Qed. +Hint Rewrite sub_1_r : nz. + End NZAddProp. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index f2b300cff..8d56772ac 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -26,8 +26,6 @@ Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T). Notation "0" := zero. Notation S := succ. Notation P := pred. - Notation "1" := (S 0). - Notation "2" := (S 1). End ZeroSuccPredNotation. Module Type ZeroSuccPred' (T:Typ) := @@ -42,9 +40,33 @@ Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E). A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n. End IsNZDomain. -Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain. -Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain. +(** Axiomatization of some more constants + Simply denoting "1" for (S 0) and so on works ok when implementing + by nat, but leaves some (Nsucc N0) when implementing by N. +*) + +Module Type OneTwo (Import T:Typ). + Parameter Inline one two : t. +End OneTwo. + +Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T). + Notation "1" := one. + Notation "2" := two. +End OneTwoNotation. + +Module Type OneTwo' (T:Typ) := OneTwo T <+ OneTwoNotation T. + +Module Type IsOneTwo (E:Eq')(Z:ZeroSuccPred' E)(O:OneTwo' E). + Import E Z O. + Axiom one_succ : 1 == S 0. + Axiom two_succ : 2 == S 1. +End IsOneTwo. + +Module Type NZDomainSig := + EqualityType <+ ZeroSuccPred <+ IsNZDomain <+ OneTwo <+ IsOneTwo. +Module Type NZDomainSig' := + EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo. (** Axiomatization of basic operations : [+] [-] [*] *) diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 3b9720f32..fe66d88c6 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -160,12 +160,12 @@ Qed. Lemma div_1_l: forall a, 1<a -> 1/a == 0. Proof. -intros; apply div_small; split; auto. apply le_succ_diag_r. +intros; apply div_small; split; auto. apply le_0_1. Qed. Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1. Proof. -intros; apply mod_small; split; auto. apply le_succ_diag_r. +intros; apply mod_small; split; auto. apply le_0_1. Qed. Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index a26e93d76..2ab7413e3 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -313,8 +313,8 @@ Theorem ofnat_S_gt_0 : Proof. unfold ofnat. intros n; induction n as [| n IH]; simpl in *. -apply lt_0_1. -apply lt_trans with 1. apply lt_0_1. now rewrite <- succ_lt_mono. +apply lt_succ_diag_r. +apply lt_trans with (S 0). apply lt_succ_diag_r. now rewrite <- succ_lt_mono. Qed. Theorem ofnat_S_neq_0 : diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 55ec3f30e..33c50b24e 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -56,14 +56,16 @@ Qed. Theorem mul_1_l : forall n, 1 * n == n. Proof. -intro n. now nzsimpl. +intro n. now nzsimpl'. Qed. Theorem mul_1_r : forall n, n * 1 == n. Proof. -intro n. now nzsimpl. +intro n. now nzsimpl'. Qed. +Hint Rewrite mul_1_l mul_1_r : nz. + Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. Proof. intros n m p. now rewrite <- 2 mul_assoc, (mul_comm m). diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 93201964e..e2e398025 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -231,19 +231,33 @@ Qed. Theorem lt_0_1 : 0 < 1. Proof. -apply lt_succ_diag_r. +rewrite one_succ. apply lt_succ_diag_r. Qed. Theorem le_0_1 : 0 <= 1. Proof. -apply le_succ_diag_r. +apply lt_le_incl, lt_0_1. +Qed. + +Theorem lt_0_2 : 0 < 2. +Proof. +transitivity 1. apply lt_0_1. rewrite two_succ. apply lt_succ_diag_r. +Qed. + +Theorem le_0_2 : 0 <= 2. +Proof. +apply lt_le_incl, lt_0_2. Qed. Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m. Proof. -intros n m H1 H2. apply <- le_succ_l in H1. order. +intros n m H1 H2. rewrite one_succ. apply <- le_succ_l in H1. order. Qed. +(** The order tactic enriched with some knowledge of 0,1,2 *) + +Ltac order' := generalize lt_0_1 lt_0_2; order. + (** More Trichotomy, decidability and double negation elimination. *) diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index cbc286fbb..a9b2fdc31 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -40,13 +40,6 @@ Module NZPowProp Hint Rewrite pow_0_r pow_succ_r : nz. -Lemma lt_0_2 : 0 < 2. -Proof. - apply lt_succ_r, le_0_1. -Qed. - -Ltac order' := generalize lt_0_1 lt_0_2; order. - (** Power and basic constants *) Lemma pow_0_l : forall a, 0<a -> 0^a == 0. @@ -58,7 +51,7 @@ Qed. Lemma pow_1_r : forall a, a^1 == a. Proof. - intros. now nzsimpl. + intros. now nzsimpl'. Qed. Lemma pow_1_l : forall a, 0<=a -> 1^a == 1. @@ -68,13 +61,15 @@ Proof. now nzsimpl. Qed. -Hint Rewrite pow_1_l : nz. +Hint Rewrite pow_1_r pow_1_l : nz. Lemma pow_2_r : forall a, a^2 == a*a. Proof. - intros. nzsimpl; order'. + intros. rewrite two_succ. nzsimpl; order'. Qed. +Hint Rewrite pow_2_r : nz. + (** Power and addition, multiplication *) Lemma pow_add_r : forall a b c, 0<=b -> 0<=c -> @@ -173,7 +168,7 @@ Qed. Lemma pow_le_mono_r : forall a b c, 0<a -> 0<=b<=c -> a^b <= a^c. Proof. intros a b c Ha (Hb,H). - apply le_succ_l in Ha. + apply le_succ_l in Ha; rewrite <- one_succ in Ha. apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. apply lt_le_incl, pow_lt_mono_r; now try split. @@ -192,7 +187,7 @@ Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> a^b < c^d. Proof. intros a b c d (Ha,Hac) (Hb,Hbd). - apply le_succ_l in Ha. + apply le_succ_l in Ha; rewrite <- one_succ in Ha. apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. transitivity (a^d). apply pow_lt_mono_r; intuition order. @@ -277,9 +272,9 @@ Proof. intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. nzsimpl. order'. clear b Hb. intros b Hb IH. nzsimpl; trivial. - rewrite <- !le_succ_l in *. + rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha. transitivity (2*(S b)). - nzsimpl. rewrite <- 2 succ_le_mono. + nzsimpl'. rewrite <- 2 succ_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. apply mul_le_mono_nonneg; trivial. order'. @@ -323,7 +318,7 @@ Proof. (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)). (* begin *) intros a b c (Ha,H) Hc. - rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl. + rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. rewrite <- !add_assoc. apply add_le_mono_l. rewrite !add_assoc. apply add_le_mono_r. destruct (le_exists_sub _ _ H) as (d & EQ & Hd). @@ -345,7 +340,7 @@ Proof. rewrite mul_assoc. rewrite (mul_comm (a+b)). assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). - assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl; order). + assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order). rewrite EQ', <- !mul_assoc. apply mul_le_mono_nonneg_l. apply pow_nonneg_nonneg; order'. diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 96d60c997..fbe71a4c7 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -45,7 +45,7 @@ Qed. Theorem eq_add_1 : forall n m, n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. Proof. -intros n m H. +intros n m. rewrite one_succ. intro H. assert (H1 : exists p, 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. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index e9ec6a823..7ed563be5 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -94,12 +94,11 @@ Qed. Theorem eq_pred_0 : forall 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]. +rewrite pred_0. now split; [left|]. 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. +split. intros H; right. now rewrite H, one_succ. +intros [H|H]. elim (neq_succ_0 _ H). +apply succ_inj_wd. now rewrite <- one_succ. Qed. Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n. @@ -130,6 +129,7 @@ Theorem pair_induction : A 0 -> A 1 -> (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n. Proof. +rewrite one_succ. 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. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index c1bac7165..8d11b5ce3 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -308,7 +308,7 @@ Qed. Theorem half_1 : half 1 == 0. Proof. -unfold half. rewrite half_aux_succ, half_aux_0; simpl; auto with *. +unfold half. rewrite one_succ, half_aux_succ, half_aux_0; simpl; auto with *. Qed. Theorem half_double : forall n, @@ -346,9 +346,8 @@ assert (LE : 0 <= half n) by apply le_0_l. le_elim LE; auto. destruct (half_double n) as [E|E]; rewrite <- LE, mul_0_r, ?add_0_r in E; rewrite E in LT. -destruct (nlt_0_r _ LT). -rewrite <- succ_lt_mono in LT. -destruct (nlt_0_r _ LT). +order'. +order. Qed. Theorem half_decrease : forall n, 0 < n -> half n < n. @@ -359,11 +358,11 @@ destruct (half_double n) as [E|E]; rewrite E at 2; rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. assert (LE : 0 <= half n) by apply le_0_l. -le_elim LE; auto. +nzsimpl. le_elim LE; auto. rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT). rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. -rewrite add_succ_l. apply lt_0_succ. +nzsimpl. apply lt_0_succ. Qed. @@ -437,7 +436,7 @@ destruct (n<<2) as [ ]_eqn:H. auto with *. apply succ_wd, E, half_decrease. rewrite <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. -apply lt_succ_l; auto. +order'. Qed. Hint Resolve log_good_step. @@ -468,7 +467,7 @@ intros n IH k Hk1 Hk2. destruct (lt_ge_cases k 2) as [LT|LE]. (* base *) rewrite log_init, pow_0 by auto. -rewrite <- le_succ_l in Hk2. +rewrite <- le_succ_l, <- one_succ in Hk2. le_elim Hk2. rewrite <- nle_gt, le_succ_l in LT. destruct LT; auto. rewrite <- Hk2. diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index f6c6ad542..6ecdef9ef 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -65,10 +65,10 @@ Proof. intros n m. split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. intro H; destruct (lt_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. +apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. order'. 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. +rewrite H2, mul_0_r in H. order'. 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 m). rewrite H in H3; false_hyp H3 lt_irrefl. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index fa855f210..2816af7c4 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -63,6 +63,7 @@ Qed. Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n. Proof. +setoid_rewrite one_succ. induct n. now left. cases n. intros; right; now left. intros n IH. destruct IH as [H | [H | H]]. @@ -73,6 +74,7 @@ Qed. Theorem lt_1_r : forall n, n < 1 <-> n == 0. Proof. +setoid_rewrite one_succ. cases n. split; intro; [reflexivity | apply lt_succ_diag_r]. intros n. rewrite <- succ_lt_mono. @@ -81,6 +83,7 @@ Qed. Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1. Proof. +setoid_rewrite one_succ. cases n. split; intro; [now left | apply le_succ_diag_r]. intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index e815f9ee6..bd6588686 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -40,17 +40,17 @@ Proof. intros x. intros [(y,H)|(y,H)]. right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl. + left. exists (S y). rewrite H. now nzsimpl'. Qed. Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1. Proof. - intros. nzsimpl. apply lt_succ_r. now apply add_le_mono. + intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono. Qed. Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m. Proof. - intros. nzsimpl. + intros. nzsimpl'. rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r. apply add_le_mono; now apply le_succ_l. Qed. @@ -91,7 +91,7 @@ Qed. Lemma odd_1 : odd 1 = true. Proof. - rewrite odd_spec. exists 0. now nzsimpl. + rewrite odd_spec. exists 0. now nzsimpl'. Qed. Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n. @@ -138,7 +138,7 @@ Proof. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1. + exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). @@ -176,19 +176,17 @@ Proof. exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm. exists (n'-m'-1). rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r. - rewrite <- (add_1_l 1) at 5. rewrite sub_add_distr. + rewrite two_succ at 5. rewrite <- (add_1_l 1). rewrite sub_add_distr. symmetry. apply sub_add. apply le_add_le_sub_l. - rewrite add_1_l, <- (mul_1_r 2) at 1. - rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l. - rewrite le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r. + rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1. + rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l by order'. + rewrite one_succ, le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r. destruct (le_gt_cases n' m') as [LE|GT]; trivial. generalize (double_below _ _ LE). order. - apply lt_succ_r, le_0_1. exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm. apply add_sub_swap. - apply mul_le_mono_pos_l. - apply lt_succ_r, le_0_1. + apply mul_le_mono_pos_l; try order'. destruct (le_gt_cases m' n') as [LE|GT]; trivial. generalize (double_above _ _ GT). order. exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index ef4ac7c45..0f04869c0 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -68,6 +68,7 @@ Arguments Scope BigN.gcd [bigN_scope bigN_scope]. Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *) +Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *) Infix "+" := BigN.add : bigN_scope. Infix "-" := BigN.sub : bigN_scope. Infix "*" := BigN.mul : bigN_scope. @@ -164,6 +165,7 @@ Ltac isBigNcst t := end | BigN.zero => constr:true | BigN.one => constr:true + | BigN.two => constr:true | _ => constr:false end. @@ -194,7 +196,6 @@ Add Ring BigNr : BigNring div BigNdiv). Section TestRing. -Local Notation "2" := (BigN.N0 2%int31) : bigN_scope. (* temporary notation *) Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. intros. ring_simplify. reflexivity. Qed. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 6697d59c3..9e6e4b609 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -71,7 +71,7 @@ Module Make (W0:CyclicType) <: NType. Definition to_N (x : t) := Zabs_N (to_Z x). - (** * Zero and One *) + (** * Zero, One *) Definition zero := mk_t O ZnZ.zero. Definition one := mk_t O ZnZ.one. @@ -115,6 +115,18 @@ Module Make (W0:CyclicType) <: NType. rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption. Qed. + (** Two *) + + (** Not really pretty, but since W0 might be Z/2Z, we're not sure + there's a proper 2 there. *) + + Definition two := succ one. + + Lemma spec_2 : [two] = 2. + Proof. + unfold two. now rewrite spec_succ, spec_1. + Qed. + (** * Addition *) Local Notation addn := (fun n => diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 65b166df6..d1217d407 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -46,6 +46,16 @@ Definition sub_succ_r := Nminus_succ_r. Definition mul_0_l := Nmult_0_l. Definition mul_succ_l n m := eq_trans (Nmult_Sn_m n m) (Nplus_comm _ _). +Lemma one_succ : 1 = Nsucc 0. +Proof. +reflexivity. +Qed. + +Lemma two_succ : 2 = Nsucc 1. +Proof. +reflexivity. +Qed. + (** Order *) Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt. @@ -165,7 +175,9 @@ Definition eq := @eq N. Definition eqb := Neqb. Definition compare := Ncompare. Definition eq_dec := N_eq_dec. -Definition zero := N0. +Definition zero := 0. +Definition one := 1. +Definition two := 2. Definition succ := Nsucc. Definition pred := Npred. Definition add := Nplus. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 5bb26d04f..bbf4f5cd7 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -163,6 +163,16 @@ Proof. reflexivity. Qed. +Theorem one_succ : 1 = S 0. +Proof. +reflexivity. +Qed. + +Theorem two_succ : 2 = S 1. +Proof. +reflexivity. +Qed. + Theorem add_0_l : forall n : nat, 0 + n = n. Proof. reflexivity. @@ -259,6 +269,8 @@ Definition eq := @eq nat. Definition eqb := beq_nat. Definition compare := nat_compare. Definition zero := 0. +Definition one := 1. +Definition two := 2. Definition succ := S. Definition pred := pred. Definition add := plus. diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 3ff2ded62..7cf3e7046 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -40,6 +40,7 @@ Module Type NType. Parameter min : t -> t -> t. Parameter zero : t. Parameter one : t. + Parameter two : t. Parameter succ : t -> t. Parameter pred : t -> t. Parameter add : t -> t -> t. @@ -66,6 +67,7 @@ Module Type NType. Parameter spec_min : forall x y, [min x y] = Zmin [x] [y]. Parameter spec_0: [zero] = 0. Parameter spec_1: [one] = 1. + Parameter spec_2: [two] = 2. Parameter spec_succ: forall n, [succ n] = [n] + 1. Parameter spec_add: forall x y, [add x y] = [x] + [y]. Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1). @@ -94,6 +96,8 @@ Module Type NType_Notation (Import N:NType). Notation "[ x ]" := (to_Z x). Infix "==" := eq (at level 70). Notation "0" := zero. + Notation "1" := one. + Notation "2" := two. Infix "+" := add. Infix "-" := sub. Infix "*" := mul. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 568ebeae8..e1dc5349b 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -13,7 +13,7 @@ Require Import ZArith Nnat NAxioms NDiv NSig. Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite - spec_0 spec_1 spec_succ spec_add spec_mul spec_pred spec_sub + spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd : nsimpl. @@ -37,6 +37,16 @@ Proof. intros. zify. generalize (spec_pos n); omega with *. Qed. +Theorem one_succ : 1 == succ 0. +Proof. +now zify. +Qed. + +Theorem two_succ : 2 == succ 1. +Proof. +now zify. +Qed. + Definition N_of_Z z := of_N (Zabs_N z). Section Induction. @@ -181,9 +191,6 @@ Qed. Program Instance pow_wd : Proper (eq==>eq==>eq) pow. -Local Notation "1" := (succ 0). -Local Notation "2" := (succ 1). - Lemma pow_0_r : forall a, a^0 == 1. Proof. intros. now zify. |