diff options
| -rw-r--r-- | theories/Classes/RelationPairs.v | 40 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/NumPrelude.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 2 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Ex.v | 2 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Lists.v | 4 |
10 files changed, 35 insertions, 27 deletions
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 7ae221d44..fd01495c4 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -13,13 +13,16 @@ Require Import Relations Morphisms. (* NB: This should be system-wide someday, but for that we need to fix the simpl tactic, since "simpl fst" would be refused for - the moment. *) + the moment. Implicit Arguments fst [[A] [B]]. Implicit Arguments snd [[A] [B]]. Implicit Arguments pair [[A] [B]]. -(* /NB *) +/NB *) + +Local Notation Fst := (@fst _ _). +Local Notation Snd := (@snd _ _). Arguments Scope relation_conjunction [type_scope signature_scope signature_scope]. @@ -44,22 +47,25 @@ Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A := Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. -(** We declare measures to the system using the [Measure] class. - Otherwise the instances would easily introduce loops, +Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope. +Notation "R @@2" := (R @@ Snd)%signature (at level 30) : signature_scope. + +(** We declare measures to the system using the [Measure] class. + Otherwise the instances would easily introduce loops, never instantiating the [f] function. *) Class Measure {A B} (f : A -> B). (** Standard measures. *) -Instance fst_measure : @Measure (A * B) A fst. -Instance snd_measure : @Measure (A * B) B snd. +Instance fst_measure : @Measure (A * B) A Fst. +Instance snd_measure : @Measure (A * B) B Snd. (** We define a product relation over [A*B]: each components should satisfy the corresponding initial relation. *) Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) := - relation_conjunction (RA @@ fst) (RB @@ snd). + relation_conjunction (RA @@1) (RB @@2). Infix "*" := RelProd : signature_scope. @@ -68,12 +74,12 @@ Section RelCompFun_Instances. Global Instance RelCompFun_Reflexive `(Measure A B f, Reflexive _ R) : Reflexive (R@@f). - Proof. firstorder. Qed. - + Proof. firstorder. Qed. + Global Instance RelCompFun_Symmetric `(Measure A B f, Symmetric _ R) : Symmetric (R@@f). Proof. firstorder. Qed. - + Global Instance RelCompFun_Transitive `(Measure A B f, Transitive _ R) : Transitive (R@@f). Proof. firstorder. Qed. @@ -106,33 +112,33 @@ Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). Lemma FstRel_ProdRel {A B}(RA:relation A) : - relation_equivalence (RA @@ fst) (RA*(fun _ _ : B => True)). + relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)). Proof. firstorder. Qed. Lemma SndRel_ProdRel {A B}(RB:relation B) : - relation_equivalence (RB @@ snd) ((fun _ _ : A =>True) * RB). + relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB). Proof. firstorder. Qed. Instance FstRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (RA*RB) (RA @@ fst). + subrelation (RA*RB) (RA @@1). Proof. firstorder. Qed. Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (RA*RB) (RB @@ snd). + subrelation (RA*RB) (RB @@2). Proof. firstorder. Qed. Instance pair_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA==>RB==> RA*RB) pair. + Proper (RA==>RB==> RA*RB) (@pair _ _). Proof. firstorder. Qed. Instance fst_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA*RB ==> RA) fst. + Proper (RA*RB ==> RA) Fst. Proof. intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto. Qed. Instance snd_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA*RB ==> RB) snd. + Proper (RA*RB ==> RB) Snd. Proof. intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto. Qed. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index da33059c9..e3c14879d 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -61,8 +61,10 @@ Ltac wsimpl := unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w. Ltac wcongruence := repeat red; intros; wsimpl; congruence. -Instance znz_measure: Measure w_op.(znz_to_Z). Instance eq_equiv : Equivalence eq. +Proof. +unfold eq. firstorder. +Qed. Instance succ_wd : Proper (eq ==> eq) succ. Proof. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 0d8f8bf5d..516827616 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -12,7 +12,7 @@ Require Import ZAxioms ZProperties. -Require Import ZArith. +Require Import ZArith_base. Local Open Scope Z_scope. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 410af329d..f752c1976 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -36,8 +36,8 @@ Hint Rewrite Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec. Ltac zcongruence := repeat red; intros; zsimpl; congruence. -Instance Z_measure: @Measure Z.t Z Z.to_Z. Instance eq_equiv : Equivalence Z.eq. +Proof. unfold Z.eq. firstorder. Qed. Obligation Tactic := zcongruence. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 123917375..69dbf656e 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -11,6 +11,7 @@ (*i $Id$ i*) Require Import Bool. (* To get the orb and negb function *) +Require Import RelationPairs. Require Export NStrongRec. Module NdefOpsPropFunct (Import N : NAxiomsSig). diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index aa291cfdc..66d3a89c2 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -34,9 +34,8 @@ Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence. Obligation Tactic := ncongruence. -Instance: @Measure N.t Z N.to_Z. - Instance eq_equiv : Equivalence N.eq. +Proof. unfold N.eq. firstorder. Qed. Program Instance succ_wd : Proper (N.eq==>N.eq) N.succ. Program Instance pred_wd : Proper (N.eq==>N.eq) N.pred. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 290c9b1c2..32860cd31 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -10,7 +10,7 @@ (*i $Id$ i*) -Require Export Setoid Morphisms RelationPairs. +Require Export Setoid Morphisms. Set Implicit Arguments. (* diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 14646fa84..fcfb5d7e7 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -94,8 +94,8 @@ Local Open Scope bigQ_scope. (** [BigQ] is a setoid *) -Instance bigQ_measure: RelationPairs.Measure BigQ.to_Q. Instance BigQeq_rel : Equivalence BigQ.eq. +Proof. unfold BigQ.eq. split; red; eauto with qarith. Qed. Instance BigQadd_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.add. Proof. diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v index 6a0231973..c64fb7a97 100644 --- a/theories/Structures/OrderedType2Ex.v +++ b/theories/Structures/OrderedType2Ex.v @@ -46,7 +46,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Include PairDecidableType O1 O2. Definition lt := - (relation_disjunction (O1.lt @@ fst) (O1.eq * O2.lt))%signature. + (relation_disjunction (O1.lt @@1) (O1.eq * O2.lt))%signature. Instance lt_strorder : StrictOrder lt. Proof. diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v index 4aa07dfdc..567cbd9f8 100644 --- a/theories/Structures/OrderedType2Lists.v +++ b/theories/Structures/OrderedType2Lists.v @@ -73,9 +73,9 @@ Module KeyOrderedType(Import O:OrderedType). Local Open Scope signature_scope. - Definition eqk : relation (key*elt) := eq @@ fst. + Definition eqk : relation (key*elt) := eq @@1. Definition eqke : relation (key*elt) := eq * Logic.eq. - Definition ltk : relation (key*elt) := lt @@ fst. + Definition ltk : relation (key*elt) := lt @@1. Hint Unfold eqk eqke ltk. |