diff options
20 files changed, 181 insertions, 459 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index c6532d868..2076a9ab2 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -45,29 +45,29 @@ Definition NZmul := w_op.(znz_mul). Instance NZeq_equiv : Equivalence NZeq. -Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Instance NZsucc_wd : Proper (NZeq ==> NZeq) NZsucc. Proof. unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. Qed. -Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Instance NZpred_wd : Proper (NZeq ==> NZeq) NZpred. Proof. unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. Qed. -Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Instance NZadd_wd : Proper (NZeq ==> NZeq ==> NZeq) NZadd. Proof. unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). now rewrite H1, H2. Qed. -Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Instance NZsub_wd : Proper (NZeq ==> NZeq ==> NZeq) NZsub. Proof. unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). now rewrite H1, H2. Qed. -Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. +Instance NZmul_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmul. Proof. unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul). now rewrite H1, H2. @@ -135,13 +135,10 @@ Qed. Section Induction. Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZeq A. +Hypothesis A_wd : Proper (NZeq ==> iff) 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 NZeq ==> iff as A_morph. -Proof. apply A_wd. Qed. - Let B (n : Z) := A (Z_to_NZ n). Lemma B0 : B 0. diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 917e3fc12..5f68b2bb1 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -350,9 +350,7 @@ Qed. Section PosNeg. Variable P : Z -> Prop. -Hypothesis P_wd : predicate_wd Zeq P. - -Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed. +Hypothesis P_wd : Proper (Zeq ==> iff) P. Theorem Z0_pos_neg : P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 7b3c0ba6e..00e34a5b5 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -64,7 +64,7 @@ Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m. Proof NZeq_dne. Theorem Zcentral_induction : -forall A : Z -> Prop, predicate_wd Zeq A -> +forall A : Z -> Prop, Proper (Zeq==>iff) 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/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v index 4d927cb3b..500dd9f53 100644 --- a/theories/Numbers/Integer/Abstract/ZDomain.v +++ b/theories/Numbers/Integer/Abstract/ZDomain.v @@ -10,22 +10,17 @@ (*i $Id$ i*) +Require Import Bool. Require Export NumPrelude. Module Type ZDomainSignature. Parameter Inline Z : Set. Parameter Inline Zeq : Z -> Z -> Prop. -Parameter Inline e : Z -> Z -> bool. +Parameter Inline Zeqb : Z -> Z -> bool. -Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y. -Axiom eq_equiv : equiv Z Zeq. - -Add Relation Z Zeq - reflexivity proved by (proj1 eq_equiv) - symmetry proved by (proj2 (proj2 eq_equiv)) - transitivity proved by (proj1 (proj2 eq_equiv)) -as eq_rel. +Axiom eqb_equiv_eq : forall x y : Z, Zeqb x y = true <-> Zeq x y. +Instance eq_equiv : Equivalence Zeq. Delimit Scope IntScope with Int. Bind Scope IntScope with Z. @@ -37,16 +32,11 @@ End ZDomainSignature. Module ZDomainProperties (Import ZDomainModule : ZDomainSignature). Open Local Scope IntScope. -Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd. +Instance Zeqb_wd : Proper (Zeq ==> Zeq ==> eq) Zeqb. 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 <- eq_equiv_e; now rewrite H2 | -assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' | -rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]]. -assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 | -assert (x == y); [rewrite Exx'; now rewrite Eyy' | -rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]]. +apply eq_true_iff_eq. +rewrite 2 eqb_equiv_eq, Exx', Eyy'; auto with *. Qed. Theorem neq_sym : forall n m, n # m -> m # n. @@ -62,7 +52,7 @@ Qed. Declare Left Step ZE_stepl. (* The right step lemma is just transitivity of Zeq *) -Declare Right Step (proj1 (proj2 eq_equiv)). +Declare Right Step (@Equivalence_Transitive _ _ eq_equiv). End ZDomainProperties. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 1b8bdda40..efd1f0da3 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -221,21 +221,21 @@ Proof NZneq_succ_iter_l. in the induction step *) Theorem Zright_induction : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) 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 Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) 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 Zright_induction' : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> forall z : Z, (forall n : Z, n <= z -> A n) -> (forall n : Z, z <= n -> A n -> A (S n)) -> @@ -243,7 +243,7 @@ Theorem Zright_induction' : Proof NZright_induction'. Theorem Zleft_induction' : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> forall z : Z, (forall n : Z, z <= n -> A n) -> (forall n : Z, n < z -> A (S n) -> A n) -> @@ -251,21 +251,21 @@ Theorem Zleft_induction' : Proof NZleft_induction'. Theorem Zstrong_right_induction : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> forall z : Z, (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) -> forall n : Z, z <= n -> A n. Proof NZstrong_right_induction. Theorem Zstrong_left_induction : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> forall z : Z, (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) -> forall n : Z, n <= z -> A n. Proof NZstrong_left_induction. Theorem Zstrong_right_induction' : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) 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) -> @@ -273,7 +273,7 @@ Theorem Zstrong_right_induction' : Proof NZstrong_right_induction'. Theorem Zstrong_left_induction' : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> forall z : Z, (forall n : Z, z <= n -> A n) -> (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) -> @@ -281,7 +281,7 @@ Theorem Zstrong_left_induction' : Proof NZstrong_left_induction'. Theorem Zorder_induction : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) 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) -> @@ -289,7 +289,7 @@ Theorem Zorder_induction : Proof NZorder_induction. Theorem Zorder_induction' : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) 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)) -> @@ -297,7 +297,7 @@ Theorem Zorder_induction' : Proof NZorder_induction'. Theorem Zorder_induction_0 : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> A 0 -> (forall n : Z, 0 <= n -> A n -> A (S n)) -> (forall n : Z, n < 0 -> A (S n) -> A n) -> @@ -305,7 +305,7 @@ Theorem Zorder_induction_0 : Proof NZorder_induction_0. Theorem Zorder_induction'_0 : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> A 0 -> (forall n : Z, 0 <= n -> A n -> A (S n)) -> (forall n : Z, n <= 0 -> A n -> A (P n)) -> @@ -317,7 +317,7 @@ Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0). (** Elimintation principle for < *) Theorem Zlt_ind : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> forall n : Z, A (S n) -> (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m. Proof NZlt_ind. @@ -325,7 +325,7 @@ Proof NZlt_ind. (** Elimintation principle for <= *) Theorem Zle_ind : - forall A : Z -> Prop, predicate_wd Zeq A -> + forall A : Z -> Prop, Proper (Zeq==>iff) A -> forall n : Z, A n -> (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m. Proof NZle_ind. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 7afa1e442..9b55c771c 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -29,31 +29,11 @@ Definition NZsub := Zminus. Definition NZmul := Zmult. Instance NZeq_equiv : Equivalence NZeq. - -Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. -Proof. -congruence. -Qed. - -Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. -Proof. -congruence. -Qed. - -Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Proof. -congruence. -Qed. - -Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. -Proof. -congruence. -Qed. +Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc. +Program Instance NZpred_wd : Proper (eq==>eq) NZpred. +Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd. +Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub. +Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul. Theorem NZpred_succ : forall n : Z, NZpred (NZsucc n) = n. Proof. @@ -61,7 +41,7 @@ exact Zpred'_succ'. Qed. Theorem NZinduction : - forall A : Z -> Prop, predicate_wd NZeq A -> + forall A : Z -> Prop, Proper (NZeq ==> iff) 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. @@ -108,25 +88,10 @@ Definition NZle := Zle. Definition NZmin := Zmin. Definition NZmax := Zmax. -Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. -Proof. -unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. -Proof. -unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. -Proof. -congruence. -Qed. +Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt. +Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle. +Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin. +Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax. Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n = m. Proof. @@ -182,10 +147,7 @@ match x with | Zneg x => Zpos x end. -Add Morphism Zopp with signature NZeq ==> NZeq as Zopp_wd. -Proof. -congruence. -Qed. +Program Instance Zopp_wd : Proper (eq==>eq) Zopp. Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n. Proof. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 3eb5238d9..dcda3f1e5 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -44,7 +44,7 @@ Qed. Add Ring NSR : Nsemi_ring. -(* The definitios of functions (NZadd, NZmul, etc.) will be unfolded by +(* The definitions of functions (NZadd, NZmul, etc.) will be unfolded by the properties functor. Since we don't want Zadd_comm to refer to unfolded definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1), we will provide an extra layer of definitions. *) @@ -130,24 +130,24 @@ Proof. split; [apply ZE_refl | apply ZE_sym | apply ZE_trans]. Qed. -Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd. +Instance Zpair_wd : Proper (NE==>NE==>Zeq) (@pair N N). Proof. intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2. Qed. -Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd. +Instance NZsucc_wd : Proper (Zeq ==> Zeq) NZsucc. Proof. unfold NZsucc, Zeq; intros n m H; simpl. do 2 rewrite add_succ_l; now rewrite H. Qed. -Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd. +Instance NZpred_wd : Proper (Zeq ==> Zeq) NZpred. Proof. unfold NZpred, Zeq; intros n m H; simpl. do 2 rewrite add_succ_r; now rewrite H. Qed. -Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd. +Instance NZadd_wd : Proper (Zeq ==> Zeq ==> Zeq) NZadd. Proof. unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl. assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2)) @@ -156,7 +156,7 @@ stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. Qed. -Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd. +Instance NZsub_wd : Proper (Zeq ==> Zeq ==> Zeq) NZsub. Proof. unfold Zeq, NZsub; intros n1 m1 H1 n2 m2 H2; simpl. symmetry in H2. @@ -166,7 +166,7 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring. now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring. Qed. -Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd. +Instance NZmul_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmul. Proof. unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. @@ -189,17 +189,13 @@ Qed. Section Induction. Open Scope NatScope. (* automatically closes at the end of the section *) Variable A : Z -> Prop. -Hypothesis A_wd : predicate_wd Zeq A. - -Add Morphism A with signature Zeq ==> iff as A_morph. -Proof. -exact A_wd. -Qed. +Hypothesis A_wd : Proper (Zeq==>iff) A. Theorem NZinduction : - A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) + A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. + (* 0 is interpreted as in Z due to "Bind" directive *) Proof. -intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *. +intros A0 AS n; unfold NZ0, Zsucc, Zeq in *. destruct n as [n m]. cut (forall p : N, A (p, 0)); [intro H1 |]. cut (forall p : N, A (0, p)); [intro H2 |]. @@ -266,7 +262,7 @@ Definition NZle := Zle. Definition NZmin := Zmin. Definition NZmax := Zmax. -Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd. +Instance NZlt_wd : Proper (Zeq ==> Zeq ==> iff) NZlt. Proof. unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. stepr (snd m1 + fst m2) by apply add_comm. @@ -285,7 +281,7 @@ now stepl (fst m1 + snd m2) by apply add_comm. stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm. Qed. -Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd. +Instance NZle_wd : Proper (Zeq ==> Zeq ==> iff) NZle. Proof. unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. do 2 rewrite lt_eq_cases. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int. @@ -293,7 +289,7 @@ fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%I now rewrite H1, H2. Qed. -Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd. +Instance NZmin_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmin. Proof. intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl. destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. @@ -309,7 +305,7 @@ stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring. unfold Zeq in H2. rewrite H2. ring. Qed. -Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd. +Instance NZmax_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmax. Proof. intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl. destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. @@ -372,7 +368,7 @@ Definition Zopp (n : Z) : Z := (snd n, fst n). Notation "- x" := (Zopp x) : IntScope. -Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. +Instance Zopp_wd : Proper (Zeq ==> Zeq) Zopp. Proof. unfold Zeq; intros n m H; simpl. symmetry. stepl (fst n + snd m) by apply add_comm. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 3e029d81b..823ef149c 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -32,6 +32,7 @@ Hint Rewrite Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec. Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec. +Ltac zcongruence := repeat red; intros; zsimpl; congruence. Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. @@ -47,30 +48,13 @@ Definition NZmul := Z.mul. Instance NZeq_equiv : Equivalence Z.eq. -Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. +Obligation Tactic := zcongruence. -Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. - -Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. - -Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. - -Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd. -Proof. -intros; zsimpl; f_equal; assumption. -Qed. +Program Instance NZsucc_wd : Proper (Z.eq ==> Z.eq) NZsucc. +Program Instance NZpred_wd : Proper (Z.eq ==> Z.eq) NZpred. +Program Instance NZadd_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZadd. +Program Instance NZsub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZsub. +Program Instance NZmul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZmul. Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n. Proof. @@ -80,13 +64,10 @@ Qed. Section Induction. Variable A : Z.t -> Prop. -Hypothesis A_wd : predicate_wd Z.eq A. +Hypothesis A_wd : Proper (Z.eq==>iff) A. Hypothesis A0 : A 0. Hypothesis AS : forall n, A n <-> A (Z.succ n). -Add Morphism A with signature Z.eq ==> iff as A_morph. -Proof. apply A_wd. Qed. - Let B (z : Z) := A (Z.of_Z z). Lemma B0 : B 0. @@ -204,30 +185,30 @@ Proof. rewrite spec_compare_alt; destruct Zcompare; auto. Qed. -Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd. +Instance compare_wd : Proper (Z.eq ==> Z.eq ==> eq) Z.compare. Proof. intros x x' Hx y y' Hy. rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition. Qed. -Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd. +Instance NZlt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt. Proof. intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition. Qed. -Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd. +Instance NZle_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.le. Proof. intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition. Qed. -Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd. +Instance NZmin_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.min. Proof. -intros; red; rewrite 2 spec_min; congruence. +repeat red; intros; rewrite 2 spec_min; congruence. Qed. -Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd. +Instance NZmax_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.max. Proof. -intros; red; rewrite 2 spec_max; congruence. +repeat red; intros; rewrite 2 spec_max; congruence. Qed. Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. @@ -274,10 +255,7 @@ End NZOrdAxiomsMod. Definition Zopp := Z.opp. -Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd. -Proof. -intros; zsimpl; auto with zarith. -Qed. +Program Instance Zopp_wd : Proper (Z.eq ==> Z.eq) Z.opp. Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n. Proof. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 7ad38577f..0c9d006d6 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -56,10 +56,7 @@ Section CentralInduction. Variable A : predicate NZ. -Hypothesis A_wd : predicate_wd NZeq A. - -Add Morphism A with signature NZeq ==> iff as A_morph. -Proof. apply A_wd. Qed. +Hypothesis A_wd : Proper (NZeq==>iff) A. Theorem NZcentral_induction : forall z : NZ, A z -> diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index e8c292992..85b284a72 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -394,10 +394,7 @@ in the induction step *) Section Induction. Variable A : NZ -> Prop. -Hypothesis A_wd : predicate_wd NZeq A. - -Add Morphism A with signature NZeq ==> iff as A_morph. -Proof. apply A_wd. Qed. +Hypothesis A_wd : Proper (NZeq==>iff) A. Section Center. @@ -557,8 +554,7 @@ Theorem NZorder_induction' : Proof. intros Az AS AP n; apply NZorder_induction; try assumption. intros m H1 H2. apply AP in H2; [| now apply <- NZle_succ_l]. -unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m); -[assumption | apply NZpred_succ]. +apply -> (A_wd (P (S m)) m); [assumption | apply NZpred_succ]. Qed. End Center. @@ -615,26 +611,24 @@ Variable z : NZ. Let Rlt (n m : NZ) := z <= n /\ n < m. Let Rgt (n m : NZ) := m < n /\ n <= z. -Add Morphism Rlt with signature NZeq ==> NZeq ==> iff as Rlt_wd. +Instance Rlt_wd : Proper (NZeq ==> NZeq ==> iff) Rlt. Proof. -intros x1 x2 H1 x3 x4 H2; unfold Rlt; rewrite H1; now rewrite H2. +intros x1 x2 H1 x3 x4 H2; unfold Rlt. rewrite H1; now rewrite H2. Qed. -Add Morphism Rgt with signature NZeq ==> NZeq ==> iff as Rgt_wd. +Instance Rgt_wd : Proper (NZeq ==> NZeq ==> iff) Rgt. Proof. intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2. Qed. -Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc Rlt). +Instance NZAcc_lt_wd : Proper (NZeq==>iff) (Acc Rlt). Proof. -unfold predicate_wd, fun_wd. intros x1 x2 H; split; intro H1; destruct H1 as [H2]; constructor; intros; apply H2; now (rewrite H || rewrite <- H). Qed. -Lemma NZAcc_gt_wd : predicate_wd NZeq (Acc Rgt). +Instance NZAcc_gt_wd : Proper (NZeq==>iff) (Acc Rgt). Proof. -unfold predicate_wd, fun_wd. intros x1 x2 H; split; intro H1; destruct H1 as [H2]; constructor; intros; apply H2; now (rewrite H || rewrite <- H). Qed. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 60b43f0d2..02d82bacd 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -129,7 +129,7 @@ symmetry in H; false_hyp H neq_succ_0. Qed. Theorem induction : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) 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. @@ -146,7 +146,7 @@ from NZ. *) Ltac induct n := induction_maker n ltac:(apply induction). Theorem case_analysis : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> A 0 -> (forall n : N, A (S n)) -> forall n : N, A n. Proof. intros; apply induction; auto. @@ -206,12 +206,7 @@ Fibonacci numbers *) Section PairInduction. Variable A : N -> Prop. -Hypothesis A_wd : predicate_wd Neq A. - -Add Morphism A with signature Neq ==> iff as A_morph. -Proof. -exact A_wd. -Qed. +Hypothesis A_wd : Proper (Neq==>iff) A. Theorem pair_induction : A 0 -> A 1 -> @@ -230,12 +225,7 @@ End PairInduction. Section TwoDimensionalInduction. Variable R : N -> N -> Prop. -Hypothesis R_wd : relation_wd Neq Neq R. - -Add Morphism R with signature Neq ==> Neq ==> iff as R_morph. -Proof. -exact R_wd. -Qed. +Hypothesis R_wd : Proper (Neq==>Neq==>iff) R. Theorem two_dim_induction : R 0 0 -> @@ -260,12 +250,7 @@ End TwoDimensionalInduction. Section DoubleInduction. Variable R : N -> N -> Prop. -Hypothesis R_wd : relation_wd Neq Neq R. - -Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1. -Proof. -exact R_wd. -Qed. +Hypothesis R_wd : Proper (Neq==>Neq==>iff) R. Theorem double_induction : (forall m : N, R 0 m) -> diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index e2a6df1cc..1e1cd95c7 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -24,7 +24,7 @@ Definition def_add (x y : N) := recursion y (fun _ p => S p) x. Infix Local "++" := def_add (at level 50, left associativity). -Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd. +Instance def_add_wd : Proper (Neq ==> Neq ==> Neq) as def_add. Proof. unfold def_add. intros x x' Exx' y y' Eyy'. @@ -72,7 +72,7 @@ Proof. unfold fun2_eq; intros; apply def_add_wd; assumption. Qed. -Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd. +Instance def_mul_wd : Proper (Neq ==> Neq ==> Neq) def_mul. Proof. unfold def_mul. intros x x' Exx' y y' Eyy'. @@ -136,7 +136,7 @@ apply lt_step_wd. assumption. Qed. -Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd. +Instance def_ltb_wd : Proper (Neq ==> Neq ==> eq) def_ltb. Proof. intros; now apply lt_curry_wd. Qed. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index da48d2fe0..6ecf7fd33 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -32,13 +32,13 @@ Definition homomorphism (f : N1 -> N2) : Prop := Definition natural_isomorphism : N1 -> N2 := NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p). -Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd. +Instance natural_isomorphism_wd : Proper (Eq1 ==> Eq2) natural_isomorphism. Proof. unfold natural_isomorphism. intros n m Eqxy. apply NAxiomsMod1.recursion_wd with (Aeq := Eq2). reflexivity. -unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd. +intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd. assumption. Qed. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index aee2cf8f7..a5b496ba3 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -201,21 +201,21 @@ Proof NZneq_succ_iter_l. in the induction step *) Theorem right_induction : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, A z -> (forall n : N, z <= n -> A n -> A (S n)) -> forall n : N, z <= n -> A n. Proof NZright_induction. Theorem left_induction : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, A z -> (forall n : N, n < z -> A (S n) -> A n) -> forall n : N, n <= z -> A n. Proof NZleft_induction. Theorem right_induction' : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, (forall n : N, n <= z -> A n) -> (forall n : N, z <= n -> A n -> A (S n)) -> @@ -223,7 +223,7 @@ Theorem right_induction' : Proof NZright_induction'. Theorem left_induction' : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, (forall n : N, z <= n -> A n) -> (forall n : N, n < z -> A (S n) -> A n) -> @@ -231,21 +231,21 @@ Theorem left_induction' : Proof NZleft_induction'. Theorem strong_right_induction : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> forall n : N, z <= n -> A n. Proof NZstrong_right_induction. Theorem strong_left_induction : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> forall n : N, n <= z -> A n. Proof NZstrong_left_induction. Theorem strong_right_induction' : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) 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) -> @@ -253,7 +253,7 @@ Theorem strong_right_induction' : Proof NZstrong_right_induction'. Theorem strong_left_induction' : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, (forall n : N, z <= n -> A n) -> (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> @@ -261,7 +261,7 @@ Theorem strong_left_induction' : Proof NZstrong_left_induction'. Theorem order_induction : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) 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) -> @@ -269,7 +269,7 @@ Theorem order_induction : Proof NZorder_induction. Theorem order_induction' : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall z : N, A z -> (forall n : N, z <= n -> A n -> A (S n)) -> (forall n : N, n <= z -> A n -> A (P n)) -> @@ -282,7 +282,7 @@ ZOrder) since they boil down to regular induction *) (** Elimintation principle for < *) Theorem lt_ind : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall n : N, A (S n) -> (forall m : N, n < m -> A m -> A (S m)) -> @@ -292,7 +292,7 @@ Proof NZlt_ind. (** Elimintation principle for <= *) Theorem le_ind : - forall A : N -> Prop, predicate_wd Neq A -> + forall A : N -> Prop, Proper (Neq==>iff) A -> forall n : N, A n -> (forall m : N, n <= m -> A m -> A (S m)) -> @@ -309,8 +309,7 @@ Proof NZgt_wf. Theorem lt_wf_0 : well_founded lt. Proof. -setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) - using relation (@relations_eq N N). +setoid_replace lt with (fun n m : N => 0 <= n /\ n < m). apply lt_wf. intros x y; split. intro H; split; [apply le_0_l | assumption]. now intros [_ H]. @@ -400,13 +399,8 @@ Qed. Section RelElim. -(* FIXME: Variable R : relation N. -- does not work *) - -Variable R : N -> N -> Prop. -Hypothesis R_wd : relation_wd Neq Neq R. - -Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. -Proof. apply R_wd. Qed. +Variable R : relation N. +Hypothesis R_wd : Proper (Neq==>Neq==>iff) R. Theorem le_ind_rel : (forall m : N, R 0 m) -> diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index a9eec350f..dea4d664d 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -26,13 +26,7 @@ Variable Aeq : relation A. Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity). -Hypothesis Aeq_equiv : equiv A Aeq. - -Add Relation A Aeq - reflexivity proved by (proj1 Aeq_equiv) - symmetry proved by (proj2 (proj2 Aeq_equiv)) - transitivity proved by (proj1 (proj2 Aeq_equiv)) -as Aeq_rel. +Instance Aeq_equiv : Equivalence Aeq. Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A := recursion @@ -42,10 +36,7 @@ recursion n. Theorem strong_rec_wd : -forall a a' : A, a ==A a' -> - forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' -> - forall n n', n == n' -> - strong_rec a f n ==A strong_rec a' f' n'. + Proper (Aeq ==> (Neq ==> (Neq ==>Aeq) ==> Aeq) ==> Neq ==> Aeq) strong_rec. Proof. intros a a' Eaa' f f' Eff' n n' Enn'. (* First we prove that recursion (which is on type N -> A) returns diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v index c5122ac08..5242826c6 100644 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -32,34 +32,14 @@ Definition NZsub := Nminus. Definition NZmul := Nmult. Instance NZeq_equiv : Equivalence NZeq. - -Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. -Proof. -congruence. -Qed. - -Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. -Proof. -congruence. -Qed. - -Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Proof. -congruence. -Qed. - -Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. -Proof. -congruence. -Qed. +Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc. +Program Instance NZpred_wd : Proper (eq==>eq) NZpred. +Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd. +Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub. +Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul. Theorem NZinduction : - forall A : NZ -> Prop, predicate_wd NZeq A -> + forall A : NZ -> Prop, Proper (NZeq==>iff) A -> A N0 -> (forall n, A n <-> A (NZsucc n)) -> forall n : NZ, A n. Proof. intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS. @@ -117,25 +97,10 @@ Definition NZle := Nle. Definition NZmin := Nmin. Definition NZmax := Nmax. -Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. -Proof. -unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. -Proof. -unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. -Proof. -congruence. -Qed. +Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt. +Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle. +Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin. +Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax. Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m. Proof. @@ -199,14 +164,9 @@ Proof. reflexivity. Qed. -Theorem recursion_wd : -forall (A : Type) (Aeq : relation A), - forall a a' : A, Aeq a a' -> - forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' -> - forall x x' : N, x = x' -> - Aeq (recursion a f x) (recursion a' f' x'). +Instance recursion_wd A (Aeq : relation A) : + Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A). Proof. -unfold fun2_wd, NZeq, fun2_eq. intros A Aeq a a' Eaa' f f' Eff'. intro x; pattern x; apply Nrect. intros x' H; now rewrite <- H. @@ -224,10 +184,10 @@ Qed. Theorem recursion_succ : forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A), - Aeq a a -> fun2_wd NZeq Aeq Aeq f -> + Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)). Proof. -unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect. +unfold recursion; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect. rewrite Nrect_step; rewrite Nrect_base; now apply f_wd. clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|]. now rewrite Nrect_step. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 38951218d..61171a43e 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -29,38 +29,14 @@ Definition NZsub := minus. Definition NZmul := mult. Instance NZeq_equiv : Equivalence NZeq. - -(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZeq" -then the theorem generated for succ_wd below is forall x, succ x = succ x, -which does not match the axioms in NAxiomsSig *) - -Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. -Proof. -congruence. -Qed. - -Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. -Proof. -congruence. -Qed. - -Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Proof. -congruence. -Qed. - -Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. -Proof. -congruence. -Qed. +Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc. +Program Instance NZpred_wd : Proper (eq==>eq) NZpred. +Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd. +Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub. +Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul. Theorem NZinduction : - forall A : nat -> Prop, predicate_wd (@eq nat) A -> + forall A : nat -> Prop, Proper (eq==>iff) A -> A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n. Proof. intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS. @@ -108,25 +84,10 @@ Definition NZle := le. Definition NZmin := min. Definition NZmax := max. -Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. -Proof. -unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. -Proof. -unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. -Proof. -congruence. -Qed. +Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt. +Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle. +Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin. +Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax. Theorem NZlt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m. Proof. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 596603b6f..81893d9af 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -41,26 +41,26 @@ Definition NZmul := N.mul. Instance NZeq_equiv : Equivalence N.eq. -Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd. +Instance NZsucc_wd : Proper (N.eq==>N.eq) NZsucc. Proof. -unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto. +unfold N.eq; repeat red; intros; rewrite 2 N.spec_succ; f_equal; auto. Qed. -Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd. +Instance NZpred_wd : Proper (N.eq==>N.eq) NZpred. Proof. -unfold N.eq; intros. +unfold N.eq; repeat red; intros. generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0). destruct N.eq_bool; rewrite N.spec_0; intros. rewrite 2 N.spec_pred0; congruence. rewrite 2 N.spec_pred; f_equal; auto; try omega. Qed. -Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd. +Instance NZadd_wd : Proper (N.eq==>N.eq==>N.eq) NZadd. Proof. -unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto. +unfold N.eq; repeat red; intros; rewrite 2 N.spec_add; f_equal; auto. Qed. -Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd. +Instance NZsub_wd : Proper (N.eq==>N.eq==>N.eq) NZsub. Proof. unfold N.eq; intros x x' Hx y y' Hy. destruct (Z_lt_le_dec [x] [y]). @@ -68,14 +68,14 @@ rewrite 2 N.spec_sub0; f_equal; congruence. rewrite 2 N.spec_sub; f_equal; congruence. Qed. -Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd. +Instance NZmul_wd : Proper (N.eq==>N.eq==>N.eq) NZmul. Proof. -unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto. +unfold N.eq; repeat red; intros; rewrite 2 N.spec_mul; f_equal; auto. Qed. Theorem NZpred_succ : forall n, N.pred (N.succ n) == n. Proof. -unfold N.eq; intros. +unfold N.eq; repeat red; intros. rewrite N.spec_pred; rewrite N.spec_succ. omega. generalize (N.spec_pos n); omega. @@ -86,13 +86,10 @@ Definition N_of_Z z := N.of_N (Zabs_N z). Section Induction. Variable A : N.t -> Prop. -Hypothesis A_wd : predicate_wd N.eq A. +Hypothesis A_wd : Proper (N.eq==>iff) A. Hypothesis A0 : A 0. Hypothesis AS : forall n, A n <-> A (N.succ n). -Add Morphism A with signature N.eq ==> iff as A_morph. -Proof. apply A_wd. Qed. - Let B (z : Z) := A (N_of_Z z). Lemma B0 : B 0. @@ -211,30 +208,30 @@ Proof. rewrite spec_compare_alt; destruct Zcompare; auto. Qed. -Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd. +Instance compare_wd : Proper (N.eq ==> N.eq ==> eq) N.compare. Proof. intros x x' Hx y y' Hy. rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition. Qed. -Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd. +Instance NZlt_wd : Proper (N.eq ==> N.eq ==> iff) N.lt. Proof. intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition. Qed. -Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd. +Instance NZle_wd : Proper (N.eq ==> N.eq ==> iff) N.le. Proof. intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition. Qed. -Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd. +Instance NZmin_wd : Proper (N.eq ==> N.eq ==> N.eq) N.min. Proof. -intros; red; rewrite 2 spec_min; congruence. +repeat red; intros; rewrite 2 spec_min; congruence. Qed. -Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd. +Instance NZmax_wd : Proper (N.eq ==> N.eq ==> N.eq) N.max. Proof. -intros; red; rewrite 2 spec_max; congruence. +repeat red; intros; rewrite 2 spec_max; congruence. Qed. Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. @@ -313,10 +310,10 @@ Qed. Theorem recursion_succ : forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A), - Aeq a a -> fun2_wd N.eq Aeq Aeq f -> + Aeq a a -> Proper (N.eq==>Aeq==>Aeq) f -> forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)). Proof. -unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n. +unfold N.eq, recursion; intros A Aeq a f EAaa f_wd n. replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)). rewrite Nrect_step. apply f_wd; auto. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index ddd1c50c3..290c9b1c2 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -91,75 +91,31 @@ end. Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r]. -(** Extentional properties of predicates, relations and functions *) +(** Predicates, relations, functions *) Definition predicate (A : Type) := A -> Prop. -Section ExtensionalProperties. - -Variables A B C : Type. -Variable Aeq : relation A. -Variable Beq : relation B. -Variable Ceq : relation C. - -(* "wd" stands for "well-defined" *) - -Definition fun_wd (f : A -> B) := Proper (Aeq==>Beq) f. - -Definition fun2_wd (f : A -> B -> C) := Proper (Aeq==>Beq==>Ceq) f. - -Definition fun_eq : relation (A -> B) := (Aeq==>Beq)%signature. - -(* Note that reflexivity of fun_eq means that every function -is well-defined w.r.t. Aeq and Beq, i.e., -forall x x' : A, Aeq x x' -> Beq (f x) (f x') *) - -Definition fun2_eq (f f' : A -> B -> C) := (Aeq==>Beq==>Ceq)%signature f f'. - -End ExtensionalProperties. - -(* The following definitions instantiate Beq or Ceq to iff; therefore, they -have to be outside the ExtensionalProperties section *) - -Definition predicate_wd (A : Type) (Aeq : relation A) := Proper (Aeq==>iff). - -Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) := - Proper (Aeq==>Beq==>iff). - -Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) := - forall (x : A) (y : B), R1 x y <-> R2 x y. - -Instance relation_eq_equiv A B : Equivalence (@relations_eq A B). -Proof. -intros A B; split; -unfold Reflexive, Symmetric, Transitive, relations_eq. -reflexivity. -now symmetry. -intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2. -Qed. - -Instance well_founded_wd A : Proper (@relations_eq A A ==> iff) (@well_founded A). +Instance well_founded_wd A : + Proper (@relation_equivalence A ==> iff) (@well_founded A). Proof. -unfold relations_eq, well_founded; intros A R1 R2 H. -split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor; -intros y H4; apply H3; [now apply <- H | now apply -> H]. +intros A R1 R2 H. +split; intros WF a; induction (WF a) as [x _ WF']; constructor; +intros y Ryx; apply WF'; destruct (H y x); auto. Qed. -(* solve_predicate_wd solves the goal [predicate_wd P] for P consisting of -morhisms and quatifiers *) +(** [solve_predicate_wd] solves the goal [Proper (?==>iff) P] + for P consisting of morphisms and quantifiers *) Ltac solve_predicate_wd := -unfold predicate_wd; let x := fresh "x" in let y := fresh "y" in let H := fresh "H" in intros x y H; setoid_rewrite H; reflexivity. -(* solve_relation_wd solves the goal [relation_wd R] for R consisting of -morhisms and quatifiers *) +(** [solve_relation_wd] solves the goal [Proper (?==>?==>iff) R] + for R consisting of morphisms and quantifiers *) Ltac solve_relation_wd := -unfold relation_wd, fun2_wd; let x1 := fresh "x" in let y1 := fresh "y" in let H1 := fresh "H" in @@ -181,39 +137,3 @@ Ltac induction_maker n t := pattern n; t; clear n; [solve_predicate_wd | ..]. -(** Relations on cartesian product. Used in MiscFunct for defining -functions whose domain is a product of sets by primitive recursion *) - -Section RelationOnProduct. - -Variables A B : Set. -Variable Aeq : relation A. -Variable Beq : relation B. - -Definition prod_rel : relation (A * B) := (Aeq * Beq)%signature. - -Instance prod_rel_equiv `(Equivalence _ Aeq, Equivalence _ Beq) : - Equivalence prod_rel. - -End RelationOnProduct. - -Implicit Arguments prod_rel [A B]. -Implicit Arguments prod_rel_equiv [A B]. - -(** Miscellaneous *) - -(*Definition comp_bool (x y : comparison) : bool := -match x, y with -| Lt, Lt => true -| Eq, Eq => true -| Gt, Gt => true -| _, _ => false -end. - -Theorem comp_bool_correct : forall x y : comparison, - comp_bool x y <-> x = y. -Proof. -destruct x; destruct y; simpl; split; now intro. -Qed.*) - - diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 4177fc202..38542c12b 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -62,40 +62,42 @@ Open Scope bigQ_scope. (** [BigQ] is a setoid *) -Add Relation BigQ.t BigQ.eq - reflexivity proved by (fun x => Qeq_refl [x]) - symmetry proved by (fun x y => Qeq_sym [x] [y]) - transitivity proved by (fun x y z => Qeq_trans [x] [y] [z]) -as BigQeq_rel. +Instance BigQeq_rel : Equivalence BigQ.eq. -Add Morphism BigQ.add with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQadd_wd. +Instance BigQadd_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.add. Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_add; rewrite H, H0; apply Qeq_refl. + do 3 red. unfold BigQ.eq; intros. + rewrite !BigQ.spec_add, H, H0. reflexivity. Qed. -Add Morphism BigQ.opp with signature BigQ.eq ==> BigQ.eq as BigQopp_wd. +Instance BigQopp_wd : Proper (BigQ.eq==>BigQ.eq) BigQ.opp. Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_opp; rewrite H; apply Qeq_refl. + do 2 red. unfold BigQ.eq; intros. + rewrite !BigQ.spec_opp, H; reflexivity. Qed. -Add Morphism BigQ.sub with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQsub_wd. +Instance BigQsub_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.sub. Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_sub; rewrite H, H0; apply Qeq_refl. + do 3 red. unfold BigQ.eq; intros. + rewrite !BigQ.spec_sub, H, H0; reflexivity. Qed. -Add Morphism BigQ.mul with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQmul_wd. +Instance BigQmul_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.mul. Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_mul; rewrite H, H0; apply Qeq_refl. + do 3 red. unfold BigQ.eq; intros. + rewrite !BigQ.spec_mul, H, H0; reflexivity. Qed. -Add Morphism BigQ.inv with signature BigQ.eq ==> BigQ.eq as BigQinv_wd. +Instance BigQinv_wd : Proper (BigQ.eq==>BigQ.eq) BigQ.inv. Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_inv; rewrite H; apply Qeq_refl. + do 2 red; unfold BigQ.eq; intros. + rewrite !BigQ.spec_inv, H; reflexivity. Qed. -Add Morphism BigQ.div with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQdiv_wd. +Instance BigQdiv_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.div. Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_div; rewrite H, H0; apply Qeq_refl. + do 3 red; unfold BigQ.eq; intros. + rewrite !BigQ.spec_div, H, H0; reflexivity. Qed. (* TODO : fix this. For the moment it's useless (horribly slow) |