diff options
Diffstat (limited to 'theories')
33 files changed, 319 insertions, 1163 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index bde3d9a92..0e47356ad 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -1,20 +1,39 @@ -Require Export NumPrelude. Require Export NZAxioms. Set Implicit Arguments. Module Type ZAxiomsSig. Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. -Open Local Scope NatIntScope. -Notation Z := NZ (only parsing). -Notation E := NZE (only parsing). +Delimit Scope IntScope with Int. +Notation Z := NZ. +Notation Zeq := NZeq. +Notation Z0 := NZ0. +Notation Z1 := (NZsucc NZ0). +Notation S := NZsucc. +Notation P := NZpred. +Notation Zplus := NZplus. +Notation Ztimes := NZtimes. +Notation Zminus := NZminus. +Notation "x == y" := (NZeq x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. +Notation "0" := NZ0 : IntScope. +Notation "1" := (NZsucc NZ0) : IntScope. +Notation "x + y" := (NZplus x y) : IntScope. +Notation "x - y" := (NZminus x y) : IntScope. +Notation "x * y" := (NZtimes x y) : IntScope. +Notation "x < y" := (NZlt x y) : IntScope. +Notation "x <= y" := (NZle x y) : IntScope. +Notation "x > y" := (NZlt y x) (only parsing) : IntScope. +Notation "x >= y" := (NZle y x) (only parsing) : IntScope. Parameter Zopp : Z -> Z. -Add Morphism Zopp with signature E ==> E as Zopp_wd. +Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. -Notation "- x" := (Zopp x) (at level 35, right associativity) : NatIntScope. +Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. + +Open Local Scope IntScope. (* Integers are obtained by postulating that every number has a predecessor *) Axiom Zsucc_pred : forall n : Z, S (P n) == n. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 9f5ff8bd3..dbe2aa439 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -1,8 +1,9 @@ Require Export ZAxioms. Require Import NZTimesOrder. -Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig). -Open Local Scope NatIntScope. +Module ZBasePropFunct (Export ZAxiomsMod : ZAxiomsSig). + +Open Local Scope IntScope. Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. @@ -22,7 +23,7 @@ Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m. Proof NZsucc_inj_wd_neg. Theorem Zcentral_induction : -forall A : Z -> Prop, predicate_wd E A -> +forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, A z -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. diff --git a/theories/Numbers/Integer/Abstract/ZDec.v b/theories/Numbers/Integer/Abstract/ZDec.v deleted file mode 100644 index 843b48b93..000000000 --- a/theories/Numbers/Integer/Abstract/ZDec.v +++ /dev/null @@ -1,3 +0,0 @@ -Axiom E_equiv_e : forall x y : Z, E x y <-> e x y. - - diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v index 7ace860f3..3146b9c2c 100644 --- a/theories/Numbers/Integer/Abstract/ZDomain.v +++ b/theories/Numbers/Integer/Abstract/ZDomain.v @@ -3,13 +3,13 @@ Require Export NumPrelude. Module Type ZDomainSignature. Parameter Inline Z : Set. -Parameter Inline E : Z -> Z -> Prop. +Parameter Inline Zeq : Z -> Z -> Prop. Parameter Inline e : Z -> Z -> bool. -Axiom E_equiv_e : forall x y : Z, E x y <-> e x y. -Axiom E_equiv : equiv Z E. +Axiom E_equiv_e : forall x y : Z, Zeq x y <-> e x y. +Axiom E_equiv : equiv Z Zeq. -Add Relation Z E +Add Relation Z Zeq reflexivity proved by (proj1 E_equiv) symmetry proved by (proj2 (proj2 E_equiv)) transitivity proved by (proj1 (proj2 E_equiv)) @@ -17,15 +17,15 @@ as E_rel. Delimit Scope IntScope with Int. Bind Scope IntScope with Z. -Notation "x == y" := (E x y) (at level 70) : IntScope. -Notation "x # y" := (~ E x y) (at level 70) : IntScope. +Notation "x == y" := (Zeq x y) (at level 70) : IntScope. +Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope. End ZDomainSignature. Module ZDomainProperties (Import ZDomainModule : ZDomainSignature). Open Local Scope IntScope. -Add Morphism e with signature E ==> E ==> eq_bool as e_wd. +Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd. Proof. intros x x' Exx' y y' Eyy'. case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial. @@ -49,7 +49,7 @@ Qed. Declare Left Step ZE_stepl. -(* The right step lemma is just transitivity of E *) +(* The right step lemma is just transitivity of Zeq *) Declare Right Step (proj1 (proj2 E_equiv)). End ZDomainProperties. diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v index e0ef2f15d..7eed9a8ee 100644 --- a/theories/Numbers/Integer/Abstract/ZOrder.v +++ b/theories/Numbers/Integer/Abstract/ZOrder.v @@ -2,7 +2,7 @@ Require Export ZTimes. Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope IntScope. (* Axioms *) @@ -140,21 +140,21 @@ Proof NZneq_succ_iter_l. in the induction step *) Theorem Zright_induction : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, A z -> (forall n : Z, z <= n -> A n -> A (S n)) -> forall n : Z, z <= n -> A n. Proof NZright_induction. Theorem Zleft_induction : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, A z -> (forall n : Z, n < z -> A (S n) -> A n) -> forall n : Z, n <= z -> A n. Proof NZleft_induction. Theorem Zorder_induction : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, A z -> (forall n : Z, z <= n -> A n -> A (S n)) -> (forall n : Z, n < z -> A (S n) -> A n) -> @@ -162,7 +162,7 @@ Theorem Zorder_induction : Proof NZorder_induction. Theorem Zorder_induction' : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, A z -> (forall n : Z, z <= n -> A n -> A (S n)) -> (forall n : Z, n <= z -> A n -> A (P n)) -> @@ -175,7 +175,7 @@ unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); Qed. Theorem Zright_induction' : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, (forall n : Z, n <= z -> A n) -> (forall n : Z, z <= n -> A n -> A (S n)) -> @@ -183,7 +183,7 @@ Theorem Zright_induction' : Proof NZright_induction'. Theorem Zstrong_right_induction' : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall z : Z, (forall n : Z, n <= z -> A n) -> (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) -> @@ -193,7 +193,7 @@ Proof NZstrong_right_induction'. (** Elimintation principle for < *) Theorem Zlt_ind : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall n : Z, A (S n) -> (forall m : Z, n < m -> A m -> A (S m)) -> @@ -203,7 +203,7 @@ Proof NZlt_ind. (** Elimintation principle for <= *) Theorem Zle_ind : - forall A : Z -> Prop, predicate_wd E A -> + forall A : Z -> Prop, predicate_wd Zeq A -> forall n : Z, A n -> (forall m : Z, n <= m -> A m -> A (S m)) -> diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v index c22b346b4..bae74feca 100644 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ b/theories/Numbers/Integer/Abstract/ZPlus.v @@ -2,7 +2,7 @@ Require Export ZBase. Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope IntScope. Theorem Zplus_0_l : forall n : Z, 0 + n == n. Proof NZplus_0_l. diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index 6a13aa3db..49fd6f558 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -2,7 +2,7 @@ Require Export ZOrder. Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope IntScope. (** Theorems that are true on both natural numbers and integers *) diff --git a/theories/Numbers/Integer/Abstract/ZPred.v b/theories/Numbers/Integer/Abstract/ZPred.v deleted file mode 100644 index 4814ab086..000000000 --- a/theories/Numbers/Integer/Abstract/ZPred.v +++ /dev/null @@ -1,54 +0,0 @@ -Axiom succ_pred : forall x : Z, S (P x) == x. -Add Morphism P with signature E ==> E as pred_wd. - -Theorem pred_inj : forall x y, P x == P y -> x == y. -Proof. -intros x y H. -setoid_replace x with (S (P x)); [| symmetry; apply succ_pred]. -setoid_replace y with (S (P y)); [| symmetry; apply succ_pred]. -now rewrite H. -Qed. - -Theorem pred_succ : forall x, P (S x) == x. -Proof. -intro x. -apply succ_inj. -now rewrite succ_pred. -Qed. - -(* The following tactics are intended for replacing a certain -occurrence of a term t in the goal by (S (P t)) or by (P (S t)). -Unfortunately, this cannot be done by setoid_replace tactic for two -reasons. First, it seems impossible to do rewriting when one side of -the equation in question (succ_pred or pred_succ) is a variable, due to bug 1604. -This does not work even when the predicate is an identifier (e.g., -when one tries to rewrite (A x) into (A (S (P x)))). Second, the -setoid_rewrite tactic, like the ordinary rewrite tactic, does not -allow specifying the exact occurrence of the term to be rewritten. Now -while not in the setoid context, this occurrence can be specified -using the pattern tactic, it does not work with setoids, since pattern -creates a lambda abstractuion, and setoid_rewrite does not work with -them. *) - -Ltac rewrite_succP t set_tac repl thm := -let x := fresh "x" in -set_tac x t; -setoid_replace x with (repl x); [| symmetry; apply thm]; -unfold x; clear x. - -Tactic Notation "rewrite_succ_pred" constr(t) := -rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) succ_pred. - -Tactic Notation "rewrite_succ_pred" constr(t) "at" integer(k) := -rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) succ_pred. - -Tactic Notation "rewrite_pred_succ" constr(t) := -rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) pred_succ. - -Tactic Notation "rewrite_pred_succ" constr(t) "at" integer(k) := -rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) pred_succ. - -(* One can add tactic notations for replacements in assumptions rather -than in the goal. For the reason of many possible variants, the core -of the tactic is factored out. *) - diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v index bc7321cba..0290c237b 100644 --- a/theories/Numbers/Integer/Abstract/ZTimes.v +++ b/theories/Numbers/Integer/Abstract/ZTimes.v @@ -3,7 +3,7 @@ Require Export ZPlus. Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope IntScope. Theorem Ztimes_0_r : forall n : Z, n * 0 == 0. Proof NZtimes_0_r. @@ -48,7 +48,7 @@ Proof NZtimes_neq_0. (** Z forms a ring *) -Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZE. +Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZeq. Proof. constructor. exact Zplus_0_l. diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index 438142095..b1a0551f8 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -2,7 +2,7 @@ Require Export ZPlusOrder. Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig). Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope IntScope. (** Theorems that are true on both natural numbers and integers *) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 0a52d214a..85596562e 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -8,7 +8,7 @@ Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. Definition NZ := Z. -Definition NZE := (@eq Z). +Definition NZeq := (@eq Z). Definition NZ0 := 0. Definition NZsucc := Zsucc'. Definition NZpred := Zpred'. @@ -16,38 +16,38 @@ Definition NZplus := Zplus. Definition NZminus := Zminus. Definition NZtimes := Zmult. -Theorem NZE_equiv : equiv Z NZE. +Theorem NZE_equiv : equiv Z NZeq. Proof. exact (@eq_equiv Z). Qed. -Add Relation Z NZE +Add Relation Z NZeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Proof. congruence. Qed. -Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Proof. congruence. Qed. -Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. +Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd. Proof. congruence. Qed. -Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. +Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. Proof. congruence. Qed. -Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. +Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd. Proof. congruence. Qed. @@ -58,7 +58,7 @@ exact Zpred'_succ'. Qed. Theorem NZinduction : - forall A : Z -> Prop, predicate_wd NZE A -> + forall A : Z -> Prop, predicate_wd NZeq A -> A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n. Proof. intros A A_wd A0 AS n; apply Zind; clear n. @@ -103,14 +103,14 @@ End NZAxiomsMod. Definition NZlt := Zlt. Definition NZle := Zle. -Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. Proof. -unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. +unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. Qed. -Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. Proof. -unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. +unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. Qed. Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n = m. @@ -139,9 +139,7 @@ match x with | Zneg x => Zpos x end. -Notation "- x" := (Zopp x) : Z_scope. - -Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd. +Add Morphism Zopp with signature NZeq ==> NZeq as Zopp_wd. Proof. congruence. Qed. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 9a012b26c..38e8e097a 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -49,14 +49,14 @@ Notation "x >= y" := (Zle y x) (only parsing) : IntScope. Notation Local N := NZ. (* To remember N without having to use a long qualifying name. since NZ will be redefined *) -Notation Local NE := NZE (only parsing). +Notation Local NE := NZeq (only parsing). Notation Local plus_wd := NZplus_wd (only parsing). Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. Definition NZ : Set := Z. -Definition NZE := Zeq. +Definition NZeq := Zeq. Definition NZ0 := Z0. Definition NZsucc := Zsucc. Definition NZpred := Zpred. diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v index 7479868e9..2d63a22fa 100644 --- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v +++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v @@ -16,7 +16,7 @@ Notation Local wB := (base w_op.(znz_digits)). Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99). -Definition NZE (n m : NZ) := [| n |] = [| m |]. +Definition NZeq (n m : NZ) := [| n |] = [| m |]. Definition NZ0 := w_op.(znz_0). Definition NZsucc := w_op.(znz_succ). Definition NZpred := w_op.(znz_pred). @@ -24,51 +24,51 @@ Definition NZplus := w_op.(znz_add). Definition NZminus := w_op.(znz_sub). Definition NZtimes := w_op.(znz_mul). -Theorem NZE_equiv : equiv NZ NZE. +Theorem NZE_equiv : equiv NZ NZeq. Proof. -unfold equiv, reflexive, symmetric, transitive, NZE; repeat split; intros; auto. +unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto. now transitivity [| y |]. Qed. -Add Relation NZ NZE +Add Relation NZ NZeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Proof. -unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. +unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. Qed. -Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Proof. -unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. +unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. Qed. -Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. +Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd. Proof. -unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). now rewrite H1, H2. Qed. -Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. +Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. Proof. -unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). now rewrite H1, H2. Qed. -Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. +Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd. Proof. -unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul). +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul). now rewrite H1, H2. Qed. Delimit Scope IntScope with Int. Bind Scope IntScope with NZ. Open Local Scope IntScope. -Notation "x == y" := (NZE x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope. +Notation "x == y" := (NZeq x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. Notation "0" := NZ0 : IntScope. Notation "'S'" := NZsucc : IntScope. Notation "'P'" := NZpred : IntScope. @@ -110,14 +110,14 @@ Qed. Theorem NZpred_succ : forall n : NZ, P (S n) == n. Proof. -intro n; unfold NZsucc, NZpred, NZE. rewrite w_spec.(spec_pred), w_spec.(spec_succ). +intro n; unfold NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred), w_spec.(spec_succ). rewrite <- NZpred_mod_wB. replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod. Qed. Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int. Proof. -unfold NZE, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct. +unfold NZeq, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct. symmetry; apply w_spec.(spec_0). exact w_spec. split; [auto with zarith |apply gt_wB_0]. Qed. @@ -125,11 +125,11 @@ Qed. Section Induction. Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZE A. +Hypothesis A_wd : predicate_wd NZeq A. Hypothesis A0 : A 0. Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *) -Add Morphism A with signature NZE ==> iff as A_morph. +Add Morphism A with signature NZeq ==> iff as A_morph. Proof A_wd. Let B (n : Z) := A (Z_to_NZ n). @@ -143,8 +143,8 @@ Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1). Proof. intros n H1 H2 H3. unfold B in *. apply -> AS in H3. -setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZE. assumption. -unfold NZE. rewrite w_spec.(spec_succ). +setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZeq. assumption. +unfold NZeq. rewrite w_spec.(spec_succ). unfold NZ_to_Z, Z_to_NZ. do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]). symmetry; apply Zmod_def_small; auto with zarith. @@ -159,9 +159,9 @@ Qed. Theorem NZinduction : forall n : NZ, A n. Proof. -intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZE. +intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZeq. apply B_holds. apply w_spec.(spec_to_Z). -unfold NZE, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. +unfold NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. reflexivity. exact w_spec. apply w_spec.(spec_to_Z). @@ -171,13 +171,13 @@ End Induction. Theorem NZplus_0_l : forall n : NZ, 0 + n == n. Proof. -intro n; unfold NZplus, NZ0, NZE. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0). +intro n; unfold NZplus, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0). rewrite Zplus_0_l. rewrite Zmod_def_small; [reflexivity | apply w_spec.(spec_to_Z)]. Qed. Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). Proof. -intros n m; unfold NZplus, NZsucc, NZE. rewrite w_spec.(spec_add). +intros n m; unfold NZplus, NZsucc, NZeq. rewrite w_spec.(spec_add). do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add). rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0. rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l; [ |apply gt_wB_0]. @@ -186,13 +186,13 @@ Qed. Theorem NZminus_0_r : forall n : NZ, n - 0 == n. Proof. -intro n; unfold NZminus, NZ0, NZE. rewrite w_spec.(spec_sub). +intro n; unfold NZminus, NZ0, NZeq. rewrite w_spec.(spec_sub). rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. Qed. Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). Proof. -intros n m; unfold NZminus, NZsucc, NZpred, NZE. +intros n m; unfold NZminus, NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub). rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r; [ | apply gt_wB_0]. rewrite Zminus_mod_idemp_l; [ | apply gt_wB_0]. @@ -201,13 +201,13 @@ Qed. Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0. Proof. -intro n; unfold NZtimes, NZ0, NZ, NZE. rewrite w_spec.(spec_mul). +intro n; unfold NZtimes, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul). rewrite w_spec.(spec_0). now rewrite Zmult_0_r. Qed. Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. Proof. -intros n m; unfold NZtimes, NZsucc, NZplus, NZE. rewrite w_spec.(spec_mul). +intros n m; unfold NZtimes, NZsucc, NZplus, NZeq. rewrite w_spec.(spec_mul). rewrite w_spec.(spec_add). rewrite w_spec.(spec_mul). rewrite w_spec.(spec_succ). rewrite Zplus_mod_idemp_l; [ | apply gt_wB_0]. rewrite Zmult_mod_idemp_r; [ | apply gt_wB_0]. rewrite Zmult_plus_distr_r. now rewrite Zmult_1_r. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 1509b5f7d..89f44fcd4 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -3,7 +3,7 @@ Require Export NumPrelude. Module Type NZAxiomsSig. Parameter Inline NZ : Set. -Parameter Inline NZE : NZ -> NZ -> Prop. +Parameter Inline NZeq : NZ -> NZ -> Prop. Parameter Inline NZ0 : NZ. Parameter Inline NZsucc : NZ -> NZ. Parameter Inline NZpred : NZ -> NZ. @@ -11,26 +11,26 @@ Parameter Inline NZplus : NZ -> NZ -> NZ. Parameter Inline NZminus : NZ -> NZ -> NZ. Parameter Inline NZtimes : NZ -> NZ -> NZ. -Axiom NZE_equiv : equiv NZ NZE. -Add Relation NZ NZE +Axiom NZE_equiv : equiv NZ NZeq. +Add Relation NZ NZeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. -Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. -Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. -Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. -Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd. +Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd. Delimit Scope NatIntScope with NatInt. Open Local Scope NatIntScope. -Notation "x == y" := (NZE x y) (at level 70) : NatIntScope. -Notation "x ~= y" := (~ NZE x y) (at level 70) : NatIntScope. +Notation "x == y" := (NZeq x y) (at level 70) : NatIntScope. +Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatIntScope. Notation "0" := NZ0 : NatIntScope. -Notation "'S'" := NZsucc : NatIntScope. -Notation "'P'" := NZpred : NatIntScope. +Notation S := NZsucc. +Notation P := NZpred. Notation "1" := (S 0) : NatIntScope. Notation "x + y" := (NZplus x y) : NatIntScope. Notation "x - y" := (NZminus x y) : NatIntScope. @@ -39,7 +39,7 @@ Notation "x * y" := (NZtimes x y) : NatIntScope. Axiom NZpred_succ : forall n : NZ, P (S n) == n. Axiom NZinduction : - forall A : NZ -> Prop, predicate_wd NZE A -> + forall A : NZ -> Prop, predicate_wd NZeq A -> A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n. Axiom NZplus_0_l : forall n : NZ, 0 + n == n. @@ -60,8 +60,8 @@ Open Local Scope NatIntScope. Parameter Inline NZlt : NZ -> NZ -> Prop. Parameter Inline NZle : NZ -> NZ -> Prop. -Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. -Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. Notation "x < y" := (NZlt x y) : NatIntScope. Notation "x <= y" := (NZle x y) : NatIntScope. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 121f78813..c467816d7 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -14,7 +14,7 @@ intros x y z H1 H2; now rewrite <- H1. Qed. Declare Left Step NZE_stepl. -(* The right step lemma is just the transitivity of NZE *) +(* The right step lemma is just the transitivity of NZeq *) Declare Right Step (proj1 (proj2 NZE_equiv)). Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2. @@ -48,9 +48,9 @@ declaration of the morphism below because the "predicate NZ" is not recognized as a type of function. Maybe it should do "eval hnf" or something like this. The same goes for "relation". *) -Hypothesis A_wd : predicate_wd NZE A. +Hypothesis A_wd : predicate_wd NZeq A. -Add Morphism A with signature NZE ==> iff as A_morph. +Add Morphism A with signature NZeq ==> iff as A_morph. Proof A_wd. Theorem NZcentral_induction : diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index cb3dd3093..f4c39934f 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -347,9 +347,9 @@ in the induction step *) Section Induction. Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZE A. +Hypothesis A_wd : predicate_wd NZeq A. -Add Morphism A with signature NZE ==> iff as A_morph. +Add Morphism A with signature NZeq ==> iff as A_morph. Proof A_wd. Section Center. @@ -532,12 +532,12 @@ Variable z : NZ. Let R (n m : NZ) := z <= n /\ n < m. -Add Morphism R with signature NZE ==> NZE ==> iff as R_wd. +Add Morphism R with signature NZeq ==> NZeq ==> iff as R_wd. Proof. intros x1 x2 H1 x3 x4 H2; unfold R; rewrite H1; now rewrite H2. Qed. -Lemma NZAcc_lt_wd : predicate_wd NZE (Acc R). +Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc R). Proof. unfold predicate_wd, fun_wd. intros x1 x2 H; split; intro H1; destruct H1 as [H2]; diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 444175c14..2a17754d5 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -1,33 +1,52 @@ -Require Export NumPrelude. Require Export NZAxioms. Set Implicit Arguments. Module Type NAxiomsSig. Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. -Open Local Scope NatIntScope. -Notation N := NZ (only parsing). -Notation E := NZE (only parsing). +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 plus := NZplus. +Notation times := NZtimes. +Notation minus := NZminus. +Notation "x == y" := (NZeq x y) (at level 70) : NatScope. +Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatScope. +Notation "0" := NZ0 : NatScope. +Notation "1" := (NZsucc NZ0) : NatScope. +Notation "x + y" := (NZplus x y) : NatScope. +Notation "x - y" := (NZminus x y) : NatScope. +Notation "x * y" := (NZtimes 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 : Set, A -> (N -> A -> A) -> N -> A. Implicit Arguments recursion [A]. Axiom pred_0 : P 0 == 0. -Axiom recursion_wd : forall (A : Set) (EA : relation A), - forall a a' : A, EA a a' -> - forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> +Axiom recursion_wd : forall (A : Set) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : N -> A -> A, eq_fun2 Neq Aeq Aeq f f' -> forall x x' : N, x == x' -> - EA (recursion a f x) (recursion a' f' x'). + Aeq (recursion a f x) (recursion a' f' x'). Axiom recursion_0 : forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a. Axiom recursion_succ : - forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), - EA a a -> fun2_wd E EA EA f -> - forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). + forall (A : Set) (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)). End NAxiomsSig. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 9705d05ba..c0c479dc8 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -1,8 +1,9 @@ Require Export NAxioms. Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *) -Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig). -Open Local Scope NatIntScope. +Module NBasePropFunct (Export 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 @@ -16,8 +17,14 @@ 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, NPlus.v to see all -available properties for plus (i.e., one does not have to go to NAxioms.v -and NZPlus.v). *) +available properties for plus, i.e., one does not have to go to NAxioms.v +for axioms and NZPlus.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. @@ -49,9 +56,9 @@ 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 Morphism if_zero with signature @eq ==> @eq ==> E ==> @eq as if_zero_wd. +Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd. Proof. -intros; unfold if_zero. apply recursion_wd with (EA := (@eq A)). +intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). reflexivity. unfold eq_fun2; now intros. assumption. Qed. @@ -92,7 +99,7 @@ symmetry in H; false_hyp H neq_succ_0. Qed. Theorem induction : - forall A : N -> Prop, predicate_wd E A -> + 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. @@ -109,7 +116,7 @@ from N. *) Ltac induct n := induction_maker n ltac:(apply induction). Theorem case_analysis : - forall A : N -> Prop, predicate_wd E A -> + 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. @@ -167,9 +174,9 @@ Fibonacci numbers *) Section PairInduction. Variable A : N -> Prop. -Hypothesis A_wd : predicate_wd E A. +Hypothesis A_wd : predicate_wd Neq A. -Add Morphism A with signature E ==> iff as A_morph. +Add Morphism A with signature Neq ==> iff as A_morph. Proof. exact A_wd. Qed. @@ -191,9 +198,9 @@ End PairInduction. Section TwoDimensionalInduction. Variable R : N -> N -> Prop. -Hypothesis R_wd : rel_wd E E R. +Hypothesis R_wd : rel_wd Neq Neq R. -Add Morphism R with signature E ==> E ==> iff as R_morph. +Add Morphism R with signature Neq ==> Neq ==> iff as R_morph. Proof. exact R_wd. Qed. @@ -221,9 +228,9 @@ End TwoDimensionalInduction. Section DoubleInduction. Variable R : N -> N -> Prop. -Hypothesis R_wd : rel_wd E E R. +Hypothesis R_wd : rel_wd Neq Neq R. -Add Morphism R with signature E ==> E ==> iff as R_morph1. +Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1. Proof. exact R_wd. Qed. diff --git a/theories/Numbers/Natural/Abstract/NDepRec.v b/theories/Numbers/Natural/Abstract/NDepRec.v deleted file mode 100644 index 648786854..000000000 --- a/theories/Numbers/Natural/Abstract/NDepRec.v +++ /dev/null @@ -1,72 +0,0 @@ -Require Export NTimes. - -(* Here we allow dependent recursion only for domains with Libniz -equality. The reason is that, if the domain is A : nat -> Set, then (A -n) must coincide with (A n') whenever n == n'. However, it is possible -to try to use arbitrary domain and require that n == n' -> A n = A n'. *) - -Module Type NDepRecSignature. -Declare Module Export NDomainModule : NDomainEqSignature. -Declare Module Export NBaseMod : NBaseSig with - Module NDomainModule := NDomainModule. -(* Instead of these two lines, I would like to say -Declare Module Export Nat : NBaseSig with Module NDomain : NatEqDomain. *) -Open Local Scope NatScope. - -Parameter Inline dep_recursion : - forall A : N -> Set, A 0 -> (forall n, A n -> A (S n)) -> forall n, A n. - -Axiom dep_recursion_0 : - forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)), - dep_recursion A a f 0 = a. - -Axiom dep_recursion_succ : - forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N), - dep_recursion A a f (S n) = f n (dep_recursion A a f n). - -End NDepRecSignature. - -Module NDepRecTimesProperties - (Import NDepRecModule : NDepRecSignature) - (Import NTimesMod : NTimesSig - with Module NPlusMod.NBaseMod := NDepRecModule.NBaseMod). -Module Export NTimesPropertiesModule := NTimesPropFunct NTimesMod. -Open Local Scope NatScope. - -Theorem not_0_implies_succ_dep : forall n, n # O -> {m : N | n == S m}. -Proof. -intro n; pattern n; apply dep_recursion; clear n; -[intro H; now elim H | intros n _ _; now exists n]. -Qed. - -Theorem plus_eq_1_dep : - forall m n : N, m + n == 1 -> {m == 0 /\ n == 1} + {m == 1 /\ n == 0}. -(* Why do we write == here instead of just = ? "x == y" is a notation -for (E x y) declared (along with E := (@eq N)) in NatDomainEq signature. If we -want to rewrite, e.g., plus_comm, which contains E, in a formula with -=, setoid rewrite signals an error, because E is not declared a -morphism w.r.t. = even though E is defined to be =. Thus, we need to -use E instead of = in our formulas. *) -Proof. -intros m n; pattern m; apply dep_recursion; clear m. -intro H. -rewrite plus_0_l in H. left; now split. -intros m IH H. rewrite plus_succ_l in H. apply succ_inj in H. -apply plus_eq_0 in H. destruct H as [H1 H2]. -right; now split; [rewrite H1 |]. -Qed. - -Theorem times_eq_0_dep : - forall n m, n * m == 0 -> {n == 0} + {m == 0}. -Proof. -intros n m; pattern n; apply dep_recursion; pattern m; apply dep_recursion; -clear n m. -intros; left; reflexivity. -intros; left; reflexivity. -intros; right; reflexivity. -intros n _ m _ H. -rewrite times_succ_l in H. rewrite plus_succ_r in H; now apply succ_0 in H. -Qed. - -End NDepRecTimesProperties. - diff --git a/theories/Numbers/Natural/Abstract/NDomain.v b/theories/Numbers/Natural/Abstract/NDomain.v deleted file mode 100644 index 8f326ffec..000000000 --- a/theories/Numbers/Natural/Abstract/NDomain.v +++ /dev/null @@ -1,102 +0,0 @@ -Require Import Ring. -Require Export NumPrelude. - -Module Type NDomainSignature. - -Parameter Inline N : Set. -Parameter Inline E : N -> N -> Prop. -Parameter Inline e : N -> N -> bool. - -(* Theoretically, we it is enough to have decidable equality e only. -If necessary, E could be defined using a coercion. However, after we -prove properties of natural numbers, we would like them to eventually -use ordinary Leibniz equality. E.g., we would like the commutativity -theorem, instantiated to nat, to say forall x y : nat, x + y = y + x, -and not forall x y : nat, eq_true (e (x + y) (y + x)) - -In fact, if we wanted to have decidable equality e only, we would have -some trouble doing rewriting. If there is a hypothesis H : e x y, this -means more precisely that H : eq_true (e x y). Such hypothesis is not -recognized as equality by setoid rewrite because it does not have the -form R x y where R is an identifier. *) - -Axiom E_equiv_e : forall x y : N, E x y <-> e x y. -Axiom E_equiv : equiv N E. - -Add Relation N E - reflexivity proved by (proj1 E_equiv) - symmetry proved by (proj2 (proj2 E_equiv)) - transitivity proved by (proj1 (proj2 E_equiv)) -as E_rel. - -Delimit Scope NatScope with Nat. -Bind Scope NatScope with N. -Notation "x == y" := (E x y) (at level 70) : NatScope. -Notation "x # y" := (~ E x y) (at level 70) : NatScope. - -End NDomainSignature. - -(* Now we give NDomainSignature, but with E being Leibniz equality. If -an implementation uses this signature, then more facts may be proved -about it. *) -Module Type NDomainEqSignature. - -Parameter Inline N : Set. -Definition E := (@eq N). -Parameter Inline e : N -> N -> bool. - -Axiom E_equiv_e : forall x y : N, E x y <-> e x y. -Definition E_equiv : equiv N E := eq_equiv N. - -Add Relation N E - reflexivity proved by (proj1 E_equiv) - symmetry proved by (proj2 (proj2 E_equiv)) - transitivity proved by (proj1 (proj2 E_equiv)) -as E_rel. - -Delimit Scope NatScope with Nat. -Bind Scope NatScope with N. -Notation "x == y" := (E x y) (at level 70) : NatScope. -Notation "x # y" := ((E x y) -> False) (at level 70) : NatScope. -(* Why do we need a new notation for Leibniz equality? See DepRec.v *) - -End NDomainEqSignature. - -Module NDomainProperties (Import NDomainModule : NDomainSignature). -(* It also accepts module of type NatDomainEq *) -Open Local Scope NatScope. - -Theorem Zneq_symm : forall n m, n # m -> m # n. -Proof. -intros n m H1 H2; symmetry in H2; false_hyp H2 H1. -Qed. - -(* The following easily follows from transitivity of e and E, but -we need to deal with the coercion *) -Add Morphism e with signature E ==> E ==> eq_bool as e_wd. -Proof. -intros x x' Exx' y y' Eyy'. -case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial. -assert (x == y); [apply <- E_equiv_e; now rewrite H2 | -assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' | -rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]]. -assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 | -assert (x == y); [rewrite Exx'; now rewrite Eyy' | -rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]]. -Qed. - -Theorem NE_stepl : forall x y z : N, x == y -> x == z -> z == y. -Proof. -intros x y z H1 H2; now rewrite <- H1. -Qed. - -Declare Left Step NE_stepl. - -(* The right step lemma is just transitivity of E *) -Declare Right Step (proj1 (proj2 E_equiv)). - -Ltac stepl_ring t := stepl t; [| ring]. -Ltac stepr_ring t := stepr t; [| ring]. - -End NDomainProperties. - diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 66e028abe..b792beefe 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -1,49 +1,49 @@ -Require Export NAxioms. +Require Import NBase. -Module Homomorphism (Nat1 Nat2 : NBaseSig). +Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). -Notation Local N1 := Nat1.NDomainModule.N. -Notation Local N2 := Nat2.NDomainModule.N. -Notation Local E1 := Nat1.NDomainModule.E. -Notation Local E2 := Nat2.NDomainModule.E. -Notation Local O1 := Nat1.O. -Notation Local O2 := Nat2.O. -Notation Local S1 := Nat1.S. -Notation Local S2 := Nat2.S. -Notation Local "x == y" := (Nat2.NDomainModule.E x y) (at level 70). +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 x : N1, f (S1 x) == S2 (f x). + f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n). Definition natural_isomorphism : N1 -> N2 := - Nat1.recursion O2 (fun (x : N1) (p : N2) => S2 p). + NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p). -Add Morphism natural_isomorphism -with signature E1 ==> E2 -as natural_isomorphism_wd. +Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd. Proof. unfold natural_isomorphism. -intros x y Exy. -apply Nat1.recursion_wd with (EA := E2). +intros n m Eqxy. +apply NAxiomsMod1.recursion_wd with (Aeq := Eq2). reflexivity. -unfold eq_fun2. intros _ _ _ y' y'' H. now apply Nat2.succ_wd. +unfold eq_fun2. 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 Nat1.recursion_0. +unfold natural_isomorphism; now rewrite NAxiomsMod1.recursion_0. Qed. Theorem natural_isomorphism_succ : - forall x : N1, natural_isomorphism (S1 x) == S2 (natural_isomorphism x). + forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n). Proof. -unfold natural_isomorphism; -intro x; now rewrite (Nat1.recursion_succ Nat2.NDomainModule.E); -[| unfold fun2_wd; intros; apply Nat2.succ_wd |]. +unfold natural_isomorphism. +intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq); +[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |]. Qed. -Theorem iso_hom : homomorphism natural_isomorphism. +Theorem hom_nat_iso : homomorphism natural_isomorphism. Proof. unfold homomorphism, natural_isomorphism; split; [exact natural_isomorphism_0 | exact natural_isomorphism_succ]. @@ -51,61 +51,59 @@ Qed. End Homomorphism. -Module Inverse (Nat1 Nat2 : NBaseSig). +Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). -Module Import NBasePropMod1 := NBasePropFunct Nat1. +Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1. (* This makes the tactic induct available. Since it is taken from -NBasePropFunct Nat1, it refers to Nat1.induction. *) +(NBasePropFunct NAxiomsMod1), it refers to induction on N1. *) -Module Hom12 := Homomorphism Nat1 Nat2. -Module Hom21 := Homomorphism Nat2 Nat1. +Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2. +Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1. -Notation Local N1 := Nat1.NDomainModule.N. -Notation Local N2 := Nat2.NDomainModule.N. +Notation Local N1 := NAxiomsMod1.N. +Notation Local N2 := NAxiomsMod2.N. Notation Local h12 := Hom12.natural_isomorphism. Notation Local h21 := Hom21.natural_isomorphism. -Notation Local "x == y" := (Nat1.NDomainModule.E x y) (at level 70). +Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity). -Lemma iso_inverse : - forall x : N1, h21 (h12 x) == x. +Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n. Proof. -induct x. -now rewrite Hom12.natural_isomorphism_0; rewrite Hom21.natural_isomorphism_0. -intros x IH. -rewrite Hom12.natural_isomorphism_succ; rewrite Hom21.natural_isomorphism_succ; -now rewrite IH. +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 (Nat1 Nat2 : NBaseSig). +Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). -Module Hom12 := Homomorphism Nat1 Nat2. -Module Hom21 := Homomorphism Nat2 Nat1. +Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2. +Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1. -Module Inverse121 := Inverse Nat1 Nat2. -Module Inverse212 := Inverse Nat2 Nat1. +Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2. +Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1. -Notation Local N1 := Nat1.NDomainModule.N. -Notation Local N2 := Nat2.NDomainModule.N. -Notation Local E1 := Nat1.NDomainModule.E. -Notation Local E2 := Nat2.NDomainModule.E. +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 x : N1, E1 (f2 (f1 x)) x /\ - forall y : N2, E2 (f1 (f2 y)) y. + forall n : N1, Eq1 (f2 (f1 n)) n /\ + forall n : N2, Eq2 (f1 (f2 n)) n. -Theorem iso_iso : isomorphism h12 h21. +Theorem iso_nat_iso : isomorphism h12 h21. Proof. unfold isomorphism. -split. apply Hom12.iso_hom. -split. apply Hom21.iso_hom. -split. apply Inverse121.iso_inverse. -apply Inverse212.iso_inverse. +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/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index 07fc67499..5ac1f70fb 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -2,7 +2,11 @@ Require Export NTimesOrder. Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope NatScope. + +Theorem minus_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2. +Proof NZminus_wd. Theorem minus_0_r : forall n : N, n - 0 == n. Proof NZminus_0_r. diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v deleted file mode 100644 index 4333d9e46..000000000 --- a/theories/Numbers/Natural/Abstract/NMiscFunct.v +++ /dev/null @@ -1,398 +0,0 @@ -Require Import Bool. (* To get the orb and negb function *) -Require Export NStrongRec. -Require Export NTimesOrder. - -Module MiscFunctFunctor (Import NatMod : NBaseSig). -Module Export StrongRecPropertiesModule := StrongRecProperties NatMod. -Open Local Scope NatScope. - -(*****************************************************) -(** Addition *) - -Definition plus (x y : N) := recursion y (fun _ p => S p) x. - -Lemma plus_step_wd : fun2_wd E E E (fun _ p => S p). -Proof. -unfold fun2_wd; intros _ _ _ p p' H; now rewrite H. -Qed. - -Add Morphism plus with signature E ==> E ==> E as plus_wd. -Proof. -unfold plus. -intros x x' Exx' y y' Eyy'. -apply recursion_wd with (EA := E). -assumption. -unfold eq_fun2; intros _ _ _ p p' Epp'; now rewrite Epp'. -assumption. -Qed. - -Theorem plus_0 : forall y, plus 0 y == y. -Proof. -intro y. unfold plus. -(*pose proof (recursion_0 E y (fun _ p => S p)) as H.*) -rewrite recursion_0. apply (proj1 E_equiv). -Qed. - -Theorem plus_succ : forall x y, plus (S x) y == S (plus x y). -Proof. -intros x y; unfold plus. -now rewrite (recursion_succ E); [|apply plus_step_wd|]. -Qed. - -(*****************************************************) -(** Multiplication *) - -Definition times (x y : N) := recursion 0 (fun _ p => plus p x) y. - -Lemma times_step_wd : forall x, fun2_wd E E E (fun _ p => plus p x). -Proof. -unfold fun2_wd. intros. now apply plus_wd. -Qed. - -Lemma times_step_equal : - forall x x', x == x' -> eq_fun2 E E E (fun _ p => plus p x) (fun x p => plus p x'). -Proof. -unfold eq_fun2; intros; apply plus_wd; assumption. -Qed. - -Add Morphism times with signature E ==> E ==> E as times_wd. -Proof. -unfold times. -intros x x' Exx' y y' Eyy'. -apply recursion_wd with (EA := E). -reflexivity. apply times_step_equal. assumption. assumption. -Qed. - -Theorem times_0_r : forall x, times x 0 == 0. -Proof. -intro. unfold times. now rewrite recursion_0. -Qed. - -Theorem times_succ_r : forall x y, times x (S y) == plus (times x y) x. -Proof. -intros x y; unfold times. -now rewrite (recursion_succ E); [| apply times_step_wd |]. -Qed. - -(*****************************************************) -(** Less Than *) - -Definition lt (m : N) : N -> bool := - recursion (if_zero false true) - (fun _ f => fun n => recursion false (fun n' _ => f n') n) - m. - -(* It would be more efficient to make a three-way comparison, i.e., -return Eq, Lt, or Gt, but since these are no-use default functions, -we define <= as (< or =) *) -Definition le (n m : N) := lt n m || e n m. - -Theorem le_lt : forall n m, le n m <-> lt n m \/ n == m. -Proof. -intros n m. rewrite E_equiv_e. unfold le. -do 3 rewrite eq_true_unfold_pos. -assert (H : lt n m || e n m = true <-> lt n m = true \/ e n m = true). -split; [apply orb_prop | apply orb_true_intro]. -now rewrite H. -Qed. - -Theorem le_intro_left : forall n m, lt n m -> le n m. -Proof. -intros; rewrite le_lt; now left. -Qed. - -Theorem le_intro_right : forall n m, n == m -> le n m. -Proof. -intros; rewrite le_lt; now right. -Qed. - -Lemma lt_base_wd : eq_fun E eq_bool (if_zero false true) (if_zero false true). -unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_succet. -Qed. - -Lemma lt_step_wd : - let step := (fun _ f => fun n => recursion false (fun n' _ => f n') n) in - eq_fun2 E (eq_fun E eq_bool) (eq_fun E eq_bool) step step. -Proof. -unfold eq_fun2, eq_fun, eq_bool. -intros x x' Exx' f f' Eff' y y' Eyy'. -apply recursion_wd with (EA := eq_bool); unfold eq_bool. -reflexivity. -unfold eq_fun2; intros; now apply Eff'. -assumption. -Qed. - -Lemma lt_curry_wd : forall m m', m == m' -> eq_fun E eq_bool (lt m) (lt m'). -Proof. -unfold lt. -intros m m' Emm'. -apply recursion_wd with (EA := eq_fun E eq_bool). -apply lt_base_wd. -apply lt_step_wd. -assumption. -Qed. - -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Proof. -unfold eq_fun; intros m m' Emm' n n' Enn'. -now apply lt_curry_wd. -Qed. - -(* Note that if we unfold lt along with eq_fun above, then "apply" signals -as error "Impossible to unify", not just, e.g., "Cannot solve second-order -unification problem". Something is probably wrong. *) - -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. -Proof. -intros x1 x2 H1 x3 x4 H2; unfold le; rewrite H1; now rewrite H2. -Qed. - -Theorem lt_base_eq : forall n, lt 0 n = if_zero false true n. -Proof. -intro n; unfold lt; now rewrite recursion_0. -Qed. - -Theorem lt_step_eq : forall m n, lt (S m) n = recursion false (fun n' _ => lt m n') n. -Proof. -intros m n; unfold lt. -pose proof (recursion_succ (eq_fun E 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. -unfold eq_bool in H. -assert (H1 : n == n); [reflexivity | apply H in H1; now rewrite H1]. -Qed. - -Theorem lt_0 : forall n, ~ lt n 0. -Proof. -ases/g -rewrite lt_base_eq; rewrite if_zero_0; now intro. -intros n; rewrite lt_step_eq. rewrite recursion_0. now intro. -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)? *) - -Lemma lt_0_1 : lt 0 1. -Proof. -rewrite lt_base_eq; now rewrite if_zero_succ. -Qed. - -Lemma lt_0_succn : forall n, lt 0 (S n). -Proof. -intro n; rewrite lt_base_eq; now rewrite if_zero_succ. -Qed. - -Lemma lt_succn_succm : forall n m, lt (S n) (S m) <-> lt n m. -Proof. -intros n m. -rewrite lt_step_eq. rewrite (recursion_succ eq_bool). -reflexivity. -now unfold eq_bool. -unfold fun2_wd; intros; now apply lt_wd. -Qed. - -Theorem lt_succ : forall m n, lt m (S n) <-> le m n. -Proof. -assert (A : forall m n, lt m (S n) <-> lt m n \/ m == n). -induct m. -ases/g -[split; intro; [now right | apply lt_0_1] | -intro n; split; intro; [left |]; apply lt_0_succn]. -ases/g -split. -intro. assert (H1 : lt n 0); [now apply -> lt_succn_succm | false_hyp H1 lt_0]. -intro H; destruct H as [H | H]. -false_hyp H lt_0. false_hyp H succ_0. -intro m. pose proof (IH m) as H; clear IH. -assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_succn_succm |]. -assert (lt (S n) (S m) <-> lt n m); [apply lt_succn_succm |]. -assert (S n == S m <-> n == m); [split; [ apply succ_inj | apply succ_wd]|]. tauto. -intros; rewrite le_lt; apply A. -Qed. - -(*****************************************************) -(** Even *) - -Definition even (x : N) := recursion true (fun _ p => negb p) x. - -Lemma even_step_wd : fun2_wd E 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 E ==> eq_bool as even_wd. -Proof. -unfold even; intros. -apply recursion_wd with (A := bool) (EA := eq_bool). -now unfold eq_bool. -unfold eq_fun2. 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 E E. - -Add Relation (prod N N) E2 -reflexivity proved by (prod_rel_refl N N E E E_equiv E_equiv) -symmetry proved by (prod_rel_symm N N E E E_equiv E_equiv) -transitivity proved by (prod_rel_trans N N E E E_equiv E_equiv) -as E2_rel. - -Lemma half_step_wd: fun2_wd E 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 E ==> E 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 (EA := E2); unfold E2. -unfold E2. -unfold prod_rel; simpl; now split. -unfold eq_fun2, 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 E ==> E as log_wd. -Proof. -intros x x' Exx'. unfold log. -apply strong_rec_wd with (EA := E); try (reflexivity || assumption). -unfold eq_fun2. 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. - -(*********************************************************) -(** To get the properties of plus, times and lt defined *) -(** via recursion, we form the corresponding modules and *) -(** apply the properties functors to these modules *) - -Module NDefaultPlusModule <: NPlusSig. - -Module NBaseMod := NatMod. -(* If we used the name NBaseMod instead of NatMod then this would -produce many warnings like "Trying to mask the absolute name -NBaseMod", "Trying to mask the absolute name Nat.O" etc. *) - -Definition plus := plus. - -Add Morphism plus with signature E ==> E ==> E as plus_wd. -Proof. -exact plus_wd. -Qed. - -Theorem plus_0_l : forall n, plus 0 n == n. -Proof. -exact plus_0. -Qed. - -Theorem plus_succ_l : forall n m, plus (S n) m == S (plus n m). -Proof. -exact plus_succ. -Qed. - -End NDefaultPlusModule. - -Module NDefaultTimesModule <: NTimesSig. -Module NPlusMod := NDefaultPlusModule. - -Definition times := times. - -Add Morphism times with signature E ==> E ==> E as times_wd. -Proof. -exact times_wd. -Qed. - -Definition times_0_r := times_0_r. -Definition times_succ_r := times_succ_r. - -End NDefaultTimesModule. - -Module NDefaultOrderModule <: NOrderSig. -Module NBaseMod := NatMod. - -Definition lt := lt. -Definition le := le. - -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Proof. -exact lt_wd. -Qed. - -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. -Proof. -exact le_wd. -Qed. - -(* This produces a warning about a morphism redeclaration. Why is not -there a warning after declaring lt? *) - -Theorem le_lt : forall x y, le x y <-> lt x y \/ x == y. -Proof. -exact le_lt. -Qed. - -Theorem lt_0 : forall x, ~ (lt x 0). -Proof. -exact lt_0. -Qed. - -Theorem lt_succ : forall x y, lt x (S y) <-> le x y. -Proof. -exact lt_succ. -Qed. - -End NDefaultOrderModule. - -Module Export DefaultTimesOrderProperties := - NTimesOrderProperties NDefaultTimesModule NDefaultOrderModule. - -End MiscFunctFunctor. - diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 7c2610ccc..3e338825e 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -2,12 +2,20 @@ Require Export NTimes. Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod. -Open Local Scope NatIntScope. +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 le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n == m. Proof NZle_lt_or_eq. @@ -142,21 +150,21 @@ Proof NZneq_succ_iter_l. in the induction step *) Theorem right_induction : - forall A : N -> Prop, predicate_wd E A -> + 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 E A -> + 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 order_induction : - forall A : N -> Prop, predicate_wd E A -> + 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) -> @@ -164,7 +172,7 @@ Theorem order_induction : Proof NZorder_induction. Theorem right_induction' : - forall A : N -> Prop, predicate_wd E A -> + 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)) -> @@ -172,7 +180,7 @@ Theorem right_induction' : Proof NZright_induction'. Theorem strong_right_induction' : - forall A : N -> Prop, predicate_wd E A -> + 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) -> @@ -182,7 +190,7 @@ Proof NZstrong_right_induction'. (** Elimintation principle for < *) Theorem lt_ind : - forall A : N -> Prop, predicate_wd E A -> + forall A : N -> Prop, predicate_wd Neq A -> forall n : N, A (S n) -> (forall m : N, n < m -> A m -> A (S m)) -> @@ -192,7 +200,7 @@ Proof NZlt_ind. (** Elimintation principle for <= *) Theorem le_ind : - forall A : N -> Prop, predicate_wd E A -> + forall A : N -> Prop, predicate_wd Neq A -> forall n : N, A n -> (forall m : N, n <= m -> A m -> A (S m)) -> @@ -258,9 +266,9 @@ Section RelElim. (* FIXME: Variable R : relation N. -- does not work *) Variable R : N -> N -> Prop. -Hypothesis R_wd : rel_wd E E R. +Hypothesis R_wd : rel_wd Neq Neq R. -Add Morphism R with signature E ==> E ==> iff as R_morph2. +Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. Proof R_wd. Theorem le_ind_rel : diff --git a/theories/Numbers/Natural/Abstract/NOtherInd.v b/theories/Numbers/Natural/Abstract/NOtherInd.v deleted file mode 100644 index 7faae620a..000000000 --- a/theories/Numbers/Natural/Abstract/NOtherInd.v +++ /dev/null @@ -1,161 +0,0 @@ -Require Export NDomain. -Declare Module Export NDomainModule : NDomainSignature. -Open Local Scope NatScope. - -Parameter O : N. -Parameter S : N -> N. - -Notation "0" := O. - -Definition induction := -forall P : N -> Prop, predicate_wd E P -> - P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n. - -Definition other_induction := -forall P : N -> Prop, - (forall n : N, n == 0 -> P n) -> - (forall n : N, P n -> forall m : N, m == S n -> P m) -> - forall n : N, P n. - -Theorem other_ind_implies_ind : other_induction -> induction. -Proof. -unfold induction, other_induction; intros OI P predicate_wd Base Step. -apply OI; unfold predicate_wd in predicate_wd. -intros; now apply -> (predicate_wd 0). -intros n Pn m EmSn; now apply -> (predicate_wd (S n)); [apply Step|]. -Qed. - -Theorem ind_implies_other_ind : induction -> other_induction. -Proof. -intros I P Base Step. -set (A := fun n => forall m, m == n -> P m). -cut (forall n, A n). -unfold A; intros H n; now apply (H n). -apply I. -unfold predicate_wd, A. intros x y Exy. -split; intros H m Em; apply H; [now rewrite Exy | now rewrite <- Exy]. -exact Base. -intros n Qn m EmSn; now apply Step with (n := n); [apply Qn |]. -Qed. - -(* This theorem is not really needed. It shows that if we have -other_induction and we proved the base case and the induction step, we -can in fact show that the predicate in question is well-defined, and -therefore we can turn this other induction into the standard one. *) -Theorem other_ind_implies_predicate_wd : -other_induction -> - forall P : N -> Prop, - (forall n : N, n == 0 -> P n) -> - (forall n : N, P n -> forall m : N, m == S n -> P m) -> - predicate_wd E P. -Proof. -intros OI P Base Step; unfold predicate_wd. -intros x; pattern x; apply OI; clear x. -(* Base case *) -intros x H1 y H2. -assert (y == 0); [rewrite <- H2; now rewrite H1|]. -assert (P x); [now apply Base|]. -assert (P y); [now apply Base|]. -split; now intro. -(* Step *) -intros x IH z H y H1. -rewrite H in H1. symmetry in H1. -split; (intro H2; eapply Step; [|apply H || apply H1]); now apply OI. -Qed. - -Section Recursion. - -Variable A : Set. -Variable EA : relation A. -Hypothesis EA_symm : symmetric A EA. -Hypothesis EA_trans : transitive A EA. - -Add Relation A EA - symmetry proved by EA_symm - transitivity proved by EA_trans -as EA_rel. - -Lemma EA_neighbor : forall a a' : A, EA a a' -> EA a a. -Proof. -intros a a' EAaa'. -apply EA_trans with (y := a'); [assumption | apply EA_symm; assumption]. -Qed. - -Parameter recursion : A -> (N -> A -> A) -> N -> A. - -Axiom recursion_0 : - forall (a : A) (f : N -> A -> A), - EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a. - -Axiom recursion_succ : - forall (a : A) (f : N -> A -> A), - EA a a -> fun2_wd E EA EA f -> - forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). - -Theorem recursion_wd : induction -> - forall a a' : A, EA a a' -> - forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' -> - forall x x' : N, x == x' -> - EA (recursion a f x) (recursion a' f' x'). -Proof. -intros I a a' Eaa' f f' f_wd f'_wd Eff'. -apply ind_implies_other_ind in I. -intro x; pattern x; apply I; clear x. -intros x Ex0 x' Exx'. -rewrite Ex0 in Exx'; symmetry in Exx'. -(* apply recursion_0 in Ex0. produces -Anomaly: type_of: this is not a well-typed term. Please report. *) -assert (EA (recursion a f x) a). -apply recursion_0. now apply EA_neighbor with (a' := a'). assumption. -assert (EA a' (recursion a' f' x')). -apply EA_symm. apply recursion_0. now apply EA_neighbor with (a' := a). assumption. -apply EA_trans with (y := a). assumption. -now apply EA_trans with (y := a'). -intros x IH y H y' H1. -rewrite H in H1; symmetry in H1. -assert (EA (recursion a f y) (f x (recursion a f x))). -apply recursion_succ. now apply EA_neighbor with (a' := a'). -assumption. now symmetry. -assert (EA (f' x (recursion a' f' x)) (recursion a' f' y')). -symmetry; apply recursion_succ. now apply EA_neighbor with (a' := a). assumption. -now symmetry. -assert (EA (f x (recursion a f x)) (f' x (recursion a' f' x))). -apply Eff'. reflexivity. apply IH. reflexivity. -apply EA_trans with (y := (f x (recursion a f x))). assumption. -apply EA_trans with (y := (f' x (recursion a' f' x))). assumption. -assumption. -Qed. - -Axiom recursion_0' : - forall (a : A) (f : N -> A -> A), - forall x : N, x == 0 -> recursion a f x = a. - -Axiom recursion_succ' : - forall (a : A) (f : N -> A -> A), - EA a a -> fun2_wd E EA EA f -> - forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). - -Theorem recursion_wd' : other_induction -> - forall a a' : A, EA a a -> EA a' a' -> EA a a' -> - forall f f' : N -> A -> A, fun2_wd E EA EA f -> fun2_wd E EA EA f' -> eq_fun2 E EA EA f f' -> - forall x x' : N, x == x' -> - EA (recursion a f x) (recursion a' f' x'). -Proof. -intros I a a' a_wd a'_wd Eaa' f f' f_wd f'_wd Eff'. -intro x; pattern x; apply I; clear x. -intros x Ex0 x' Exx'. rewrite Ex0 in Exx'. symmetry in Exx'. -replace (recursion a f x) with a. replace (recursion a' f' x') with a'. -assumption. symmetry; now apply recursion_0'. symmetry; now apply recursion_0'. -intros x IH y EySx y' Eyy'. rewrite EySx in Eyy'. symmetry in Eyy'. -apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_succ'. -apply EA_trans with (y := (f' x (recursion a' f' x))). -apply Eff'. reflexivity. now apply IH. -symmetry; now apply recursion_succ'. -Qed. - - - -End Recursion. - -Implicit Arguments recursion [A]. - diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v index 8ca3ba000..1e5c2211f 100644 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ b/theories/Numbers/Natural/Abstract/NPlus.v @@ -2,7 +2,11 @@ Require Export NBase. Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NBasePropMod := NBasePropFunct NAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope NatScope. + +Theorem plus_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2. +Proof NZplus_wd. Theorem plus_0_l : forall n : N, 0 + n == n. Proof NZplus_0_l. diff --git a/theories/Numbers/Natural/Abstract/NPred.v b/theories/Numbers/Natural/Abstract/NPred.v deleted file mode 100644 index d3d22651c..000000000 --- a/theories/Numbers/Natural/Abstract/NPred.v +++ /dev/null @@ -1,46 +0,0 @@ -Require Export NAxioms. - -(* We would like to have a signature for the predecessor: first, to be -able to provide an efficient implementation, and second, to be able to -use this function in the signatures defining other functions, e.g., -subtraction. If we just define predecessor by recursion in -NBasePropFunct functor, we would not be able to use it in other -signatures. *) - -Module Type NPredSignature. -Declare Module Export NBaseMod : NBaseSig. -Open Local Scope NatScope. - -Parameter Inline P : N -> N. - -Add Morphism P with signature E ==> E as pred_wd. - -Axiom pred_0 : P 0 == 0. -Axiom pred_succ : forall n, P (S n) == n. - -End NPredSignature. - -Module NDefPred (Import NM : NBaseSig) <: NPredSignature. -Module NBaseMod := NM. -Open Local Scope NatScope. - -Definition P (n : N) : N := recursion 0 (fun m _ : N => m) n. - -Add Morphism P with signature E ==> E as pred_wd. -Proof. -intros; unfold P. -now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |]. -Qed. - -Theorem pred_0 : P 0 == 0. -Proof. -unfold P; now rewrite recursion_0. -Qed. - -Theorem pred_succ : forall n, P (S n) == n. -Proof. -intro n; unfold P; now rewrite (recursion_succ E); [| unfold fun2_wd; now intros |]. -Qed. - -End NDefPred. - diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v deleted file mode 100644 index d1f4aac26..000000000 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ /dev/null @@ -1,69 +0,0 @@ -Require Export NAxioms. - -Module StrongRecProperties (Import NBaseMod : NBaseSig). -Module Export NBasePropMod := NBasePropFunct NBaseMod. -Open Local Scope NatScope. - -Section StrongRecursion. - -Variable A : Set. -Variable EA : relation A. - -Hypothesis EA_equiv : equiv A EA. - -Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (x : N) : A := -(recursion (fun _ : N => a) - (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)) - (S x)) x. - -Lemma strong_rec_step_wd : forall f : N -> (N -> A) -> A, -fun2_wd E (eq_fun E EA) EA f -> - fun2_wd E (eq_fun E EA) (eq_fun E EA) - (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)). -Proof. -unfold fun2_wd; intros f f_wd. -intros x x' Exx'. unfold eq_fun. intros g g' Egg' y y' Eyy'. -assert (H : e y x = e y' x'). now apply e_wd. rewrite H. -destruct (e y' x'); simpl. -now apply f_wd. now apply Egg'. -Qed. - -Theorem strong_rec_wd : -forall a a', EA a a' -> - forall f f', eq_fun2 E (eq_fun E EA) EA f f' -> - forall x x', x == x' -> - EA (strong_rec a f x) (strong_rec a' f' x'). -Proof. -intros a a' Eaa' f f' Eff' x x' Exx'. -assert (H : eq_fun E EA - (recursion (fun _ : N => a) - (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f x p) else (p y)) - (S x)) - (recursion (fun _ : N => a') - (fun (x : N) (p : N -> A) (y : N) => if (e y x) then (f' x p) else (p y)) - (S x'))). -apply recursion_wd with (EA := eq_fun E EA). -unfold eq_fun; now intros. -unfold eq_fun2. intros y y' Eyy' p p' Epp'. unfold eq_fun. intros z z' Ezz'. -assert (H: e z y = e z' y'); [now apply e_wd|]. -rewrite <- H. destruct (e z y); [now apply Eff' | now apply Epp']. -now rewrite Exx'. -unfold strong_rec. -now apply H. -Qed. - -(* To do: -Definition step_good (g : N -> (N -> A) -> A) := - forall (x : N) (h1 h2 : N -> A), - (forall y : N, y < x -> EA (h1 y) (h2 y)) -> EA (g x h1) (g x h2). - -Theorem strong_recursion_fixpoint : forall a g, step_good g -> - let f x := (strong_rec a g x) in forall x, EA (f x) (g x f). -*) - -End StrongRecursion. - -Implicit Arguments strong_rec [A]. - -End StrongRecProperties. - diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v index bcf073ffa..76b85ee87 100644 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ b/theories/Numbers/Natural/Abstract/NTimes.v @@ -5,7 +5,11 @@ Require Export NPlus. Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope NatScope. + +Theorem times_wd : + forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2. +Proof NZtimes_wd. Theorem times_0_r : forall n, n * 0 == 0. Proof NZtimes_0_r. @@ -39,7 +43,7 @@ Proof NZtimes_1_l. Theorem times_1_r : forall n : N, n * 1 == n. Proof NZtimes_1_r. -Lemma Nsemi_ring : semi_ring_theory 0 1 NZplus NZtimes E. +Lemma Nsemi_ring : semi_ring_theory 0 1 NZplus NZtimes Neq. Proof. constructor. exact plus_0_l. diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index dc1b977aa..e644304dc 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -2,7 +2,7 @@ Require Export NOrder. Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope NatScope. Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m. Proof NZplus_lt_mono_l. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 557177907..b35af2e01 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -7,7 +7,7 @@ Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. Definition NZ := N. -Definition NZE := (@eq N). +Definition NZeq := (@eq N). Definition NZ0 := 0. Definition NZsucc := Nsucc. Definition NZpred := Npred. @@ -15,42 +15,42 @@ Definition NZplus := Nplus. Definition NZminus := Nminus. Definition NZtimes := Nmult. -Theorem NZE_equiv : equiv N NZE. +Theorem NZE_equiv : equiv N NZeq. Proof (eq_equiv N). -Add Relation N NZE +Add Relation N NZeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Proof. congruence. Qed. -Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Proof. congruence. Qed. -Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. +Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd. Proof. congruence. Qed. -Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. +Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. Proof. congruence. Qed. -Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. +Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd. Proof. congruence. Qed. Theorem NZinduction : - forall A : N -> Prop, predicate_wd NZE A -> + forall A : N -> Prop, predicate_wd NZeq A -> A 0 -> (forall n, A n <-> A (Nsucc n)) -> forall n : N, A n. Proof. intros A A_wd A0 AS. apply Nind. assumption. intros; now apply -> AS. @@ -91,14 +91,14 @@ End NZAxiomsMod. Definition NZlt := Nlt. Definition NZle := Nle. -Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. Proof. -unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. Qed. -Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. Proof. -unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. Qed. Theorem NZle_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m. @@ -135,14 +135,14 @@ reflexivity. Qed. Theorem recursion_wd : -forall (A : Set) (EA : relation A), - forall a a' : A, EA a a' -> - forall f f' : N -> A -> A, eq_fun2 NZE EA EA f f' -> +forall (A : Set) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : N -> A -> A, eq_fun2 NZeq Aeq Aeq f f' -> forall x x' : N, x = x' -> - EA (recursion a f x) (recursion a' f' x'). + Aeq (recursion a f x) (recursion a' f' x'). Proof. -unfold fun2_wd, NZE, eq_fun2. -intros A EA a a' Eaa' f f' Eff'. +unfold fun2_wd, NZeq, eq_fun2. +intros A Aeq a a' Eaa' f f' Eff'. intro x; pattern x; apply Nind. intros x' H; now rewrite <- H. clear x. @@ -158,11 +158,11 @@ intros A a f; unfold recursion; unfold Nrec; now rewrite Nrect_base. Qed. Theorem recursion_succ : - forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), - EA a a -> fun2_wd NZE EA EA f -> - forall n : N, EA (recursion a f (Nsucc n)) (f n (recursion a f n)). + forall (A : Set) (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 NZE, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind. +unfold NZeq, recursion, Nrec, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nind. 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. @@ -172,7 +172,6 @@ End NBinaryAxiomsMod. Module Export NBinaryMinusPropMod := NMinusPropFunct 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 *) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index f8a9ecd63..a3109fc6d 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -6,7 +6,7 @@ Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. Definition NZ := nat. -Definition NZE := (@eq nat). +Definition NZeq := (@eq nat). Definition NZ0 := 0. Definition NZsucc := S. Definition NZpred := pred. @@ -14,40 +14,40 @@ Definition NZplus := plus. Definition NZminus := minus. Definition NZtimes := mult. -Theorem NZE_equiv : equiv nat NZE. +Theorem NZE_equiv : equiv nat NZeq. Proof (eq_equiv nat). -Add Relation nat NZE +Add Relation nat NZeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZE" +(* 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 NZE ==> NZE as NZsucc_wd. +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Proof. congruence. Qed. -Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Proof. congruence. Qed. -Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. +Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd. Proof. congruence. Qed. -Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. +Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. Proof. congruence. Qed. -Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. +Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd. Proof. congruence. Qed. @@ -99,14 +99,14 @@ End NZAxiomsMod. Definition NZlt := lt. Definition NZle := le. -Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. Proof. -unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. Qed. -Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. Proof. -unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. Qed. Theorem NZle_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m. @@ -143,11 +143,11 @@ Proof. reflexivity. Qed. -Theorem recursion_wd : forall (A : Set) (EA : relation A), - forall a a' : A, EA a a' -> - forall f f' : nat -> A -> A, eq_fun2 (@eq nat) EA EA f f' -> +Theorem recursion_wd : forall (A : Set) (Aeq : relation A), + forall a a' : A, Aeq a a' -> + forall f f' : nat -> A -> A, eq_fun2 (@eq nat) Aeq Aeq f f' -> forall n n' : nat, n = n' -> - EA (recursion a f n) (recursion a' f' n'). + Aeq (recursion a f n) (recursion a' f' n'). Proof. unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto. Qed. @@ -159,9 +159,9 @@ reflexivity. Qed. Theorem recursion_succ : - forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A), - EA a a -> fun2_wd (@eq nat) EA EA f -> - forall n : nat, EA (recursion a f (S n)) (f n (recursion a f n)). + forall (A : Set) (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. unfold eq_fun2; induction n; simpl; auto. Qed. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 7feed2b14..5f945701f 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -91,26 +91,26 @@ Definition predicate (A : Type) := A -> Prop. Section ExtensionalProperties. Variables A B C : Type. -Variable EA : relation A. -Variable EB : relation B. -Variable EC : relation C. +Variable Aeq : relation A. +Variable Beq : relation B. +Variable Ceq : relation C. (* "wd" stands for "well-defined" *) -Definition fun_wd (f : A -> B) := forall x y : A, EA x y -> EB (f x) (f y). +Definition fun_wd (f : A -> B) := forall x y : A, Aeq x y -> Beq (f x) (f y). Definition fun2_wd (f : A -> B -> C) := - forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f x' y'). + forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f x' y'). Definition eq_fun : relation (A -> B) := - fun f f' => forall x x' : A, EA x x' -> EB (f x) (f' x'). + fun f f' => forall x x' : A, Aeq x x' -> Beq (f x) (f' x'). (* Note that reflexivity of eq_fun means that every function -is well-defined w.r.t. EA and EB, i.e., -forall x x' : A, EA x x' -> EB (f x) (f x') *) +is well-defined w.r.t. Aeq and Beq, i.e., +forall x x' : A, Aeq x x' -> Beq (f x) (f x') *) Definition eq_fun2 (f f' : A -> B -> C) := - forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f' x' y'). + forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f' x' y'). End ExtensionalProperties. @@ -119,10 +119,10 @@ Implicit Arguments fun2_wd [A B C]. Implicit Arguments eq_fun [A B]. Implicit Arguments eq_fun2 [A B C]. -Definition predicate_wd (A : Type) (EA : relation A) := fun_wd EA iff. +Definition predicate_wd (A : Type) (Aeq : relation A) := fun_wd Aeq iff. -Definition rel_wd (A B : Type) (EA : relation A) (EB : relation B) := - fun2_wd EA EB iff. +Definition rel_wd (A B : Type) (Aeq : relation A) (Beq : relation B) := + fun2_wd Aeq Beq iff. Implicit Arguments predicate_wd [A]. Implicit Arguments rel_wd [A B]. @@ -168,14 +168,14 @@ functions whose domain is a product of sets by primitive recursion *) Section RelationOnProduct. Variables A B : Set. -Variable EA : relation A. -Variable EB : relation B. +Variable Aeq : relation A. +Variable Beq : relation B. -Hypothesis EA_equiv : equiv A EA. -Hypothesis EB_equiv : equiv B EB. +Hypothesis EA_equiv : equiv A Aeq. +Hypothesis EB_equiv : equiv B Beq. Definition prod_rel : relation (A * B) := - fun p1 p2 => EA (fst p1) (fst p2) /\ EB (snd p1) (snd p2). + fun p1 p2 => Aeq (fst p1) (fst p2) /\ Beq (snd p1) (snd p2). Lemma prod_rel_refl : reflexive (A * B) prod_rel. Proof. |