diff options
author | 2008-12-14 16:34:43 +0000 | |
---|---|---|
committer | 2008-12-14 16:34:43 +0000 | |
commit | c74f11d65b693207cdfa6d02f697e76093021be7 (patch) | |
tree | b32866140d9f5ecde0bb719c234c6603d44037a8 /theories/Classes/SetoidClass.v | |
parent | 2f63108dccc104fe32344d88b35193d34a88f743 (diff) |
Generalized binding syntax overhaul: only two new binders: `() and `{},
guessing the binding name by default and making all generalized
variables implicit. At the same time, continue refactoring of
Record/Class/Inductive etc.., getting rid of [VernacRecord]
definitively. The AST is not completely satisfying, but leaning towards
Record/Class as restrictions of inductive (Arnaud, anyone ?).
Now, [Class] declaration bodies are either of the form [meth : type] or
[{ meth : type ; ... }], distinguishing singleton "definitional" classes
and inductive classes based on records. The constructor syntax is
accepted ([meth1 : type1 | meth1 : type2]) but raises an error
immediately, as support for defining a class by a general inductive type
is not there yet (this is a bugfix!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidClass.v')
-rw-r--r-- | theories/Classes/SetoidClass.v | 36 |
1 files changed, 14 insertions, 22 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index ddefa5cd7..78616a9a4 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -26,9 +26,9 @@ Require Import Coq.Classes.Functions. (** A setoid wraps an equivalence. *) -Class Setoid A := +Class Setoid A := { equiv : relation A ; - setoid_equiv :> Equivalence equiv. + setoid_equiv :> Equivalence equiv }. (* Too dangerous instance *) (* Program Instance [ eqa : Equivalence A eqA ] => *) @@ -37,13 +37,13 @@ Class Setoid A := (** Shortcuts to make proof search easier. *) -Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. +Definition setoid_refl `(sa : Setoid A) : Reflexive equiv. Proof. typeclasses eauto. Qed. -Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. +Definition setoid_sym `(sa : Setoid A) : Symmetric equiv. Proof. typeclasses eauto. Qed. -Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. +Definition setoid_trans `(sa : Setoid A) : Transitive equiv. Proof. typeclasses eauto. Qed. Existing Instance setoid_refl. @@ -55,7 +55,7 @@ Existing Instance setoid_trans. (* Program Instance eq_setoid : Setoid A := *) (* equiv := eq ; setoid_equiv := eq_equivalence. *) -Program Instance iff_setoid : Setoid Prop := +Program Instance iff_setoid : Setoid Prop := equiv := iff ; setoid_equiv := iff_equivalence. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -84,7 +84,7 @@ Ltac clsubst_nofail := Tactic Notation "clsubst" "*" := clsubst_nofail. -Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z. +Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z. Proof with auto. intros; intro. assert(z == y) by (symmetry ; auto). @@ -92,7 +92,7 @@ Proof with auto. contradiction. Qed. -Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z. +Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. intros; intro. assert(y == x) by (symmetry ; auto). @@ -119,18 +119,11 @@ Ltac setoidify := repeat setoidify_tac. (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) -Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv := - PER_morphism. +Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv := + respect := respect. -(** Add this very useful instance in the database. *) - -Implicit Arguments setoid_morphism [[!sa]]. -Existing Instance setoid_morphism. - -Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) := - Reflexive_partial_app_morphism. - -Existing Instance setoid_partial_app_morphism. +Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Morphism (equiv ++> iff) (equiv x) := + respect := respect. Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto. @@ -144,9 +137,8 @@ Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id. (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) -Class PartialSetoid (A : Type) := - pequiv : relation A ; - pequiv_prf :> PER pequiv. +Class PartialSetoid (A : Type) := + { pequiv : relation A ; pequiv_prf :> PER pequiv }. (** Overloaded notation for partial setoid equivalence. *) |