From 9ed53a06a626b82920db6e058835cf2d413ecd56 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 6 Nov 2009 16:43:48 +0000 Subject: Numbers: more (syntactic) changes toward new style of type classes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/Abstract/NBase.v | 25 ++------- theories/Numbers/Natural/Abstract/NDefOps.v | 6 +-- theories/Numbers/Natural/Abstract/NIso.v | 4 +- theories/Numbers/Natural/Abstract/NOrder.v | 36 ++++++------- theories/Numbers/Natural/Abstract/NStrongRec.v | 13 +---- theories/Numbers/Natural/Binary/NBinDefs.v | 68 +++++-------------------- theories/Numbers/Natural/Peano/NPeano.v | 59 ++++----------------- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 43 ++++++++-------- 8 files changed, 71 insertions(+), 183 deletions(-) (limited to 'theories/Numbers/Natural') 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. -- cgit v1.2.3