diff options
| author | letouzey | 2009-11-06 16:43:48 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-06 16:43:48 +0000 |
| commit | 9ed53a06a626b82920db6e058835cf2d413ecd56 (patch) | |
| tree | 6bd4efe0d8679f9a3254091e6f1d64b1b2462ec2 /theories/Numbers/Cyclic/Abstract | |
| parent | 625a129d5e9b200399a147111f191abe84282aa4 (diff) | |
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
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index c6532d868a..2076a9ab2a 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. |