From b40d51ba9582bbdae454a3c0707520042201f248 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 31 Dec 2007 13:27:00 +0000 Subject: Move Classes.Setoid to Classes.SetoidClass to avoid name clash. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10411 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 2 +- tactics/class_setoid.ml4 | 8 +- theories/Classes/Setoid.v | 192 --------------------------------------- theories/Classes/SetoidClass.v | 192 +++++++++++++++++++++++++++++++++++++++ theories/Classes/SetoidTactics.v | 2 +- 5 files changed, 198 insertions(+), 198 deletions(-) delete mode 100644 theories/Classes/Setoid.v create mode 100644 theories/Classes/SetoidClass.v diff --git a/Makefile.common b/Makefile.common index 84a15bf837..a8801f3df0 100644 --- a/Makefile.common +++ b/Makefile.common @@ -706,7 +706,7 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor UNICODEVO:= theories/Unicode/Utf8.vo -CLASSESVO:= theories/Classes/Init.vo theories/Classes/Setoid.vo theories/Classes/SetoidTactics.v +CLASSESVO:= theories/Classes/Init.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.v THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 index 0c8bdd2980..9111ba97e1 100644 --- a/tactics/class_setoid.ml4 +++ b/tactics/class_setoid.ml4 @@ -57,10 +57,10 @@ let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") let iff = lazy (gen_constant ["Init"; "Logic"] "iff") -let iff_setoid = lazy (gen_constant ["Classes"; "Setoid"] "iff_setoid") -let setoid_equiv = lazy (gen_constant ["Classes"; "Setoid"] "equiv") -let setoid_morphism = lazy (gen_constant ["Classes"; "Setoid"] "setoid_morphism") -let setoid_refl_proj = lazy (gen_constant ["Classes"; "Setoid"] "equiv_refl") +let iff_setoid = lazy (gen_constant ["Classes"; "SetoidClass"] "iff_setoid") +let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv") +let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism") +let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl") let arrow_morphism a b = mkLambda (Name (id_of_string "A"), a, diff --git a/theories/Classes/Setoid.v b/theories/Classes/Setoid.v deleted file mode 100644 index 915a7a944a..0000000000 --- a/theories/Classes/Setoid.v +++ /dev/null @@ -1,192 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* R y x := equiv_sym _ _ equiv_prf. -Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf. - - -Ltac refl := - match goal with - | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X) - | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X) - | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X) - | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X) - | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X) - end. - -Ltac sym := - match goal with - | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y)) - | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X)) - | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X)) - | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X)) - | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X)) - end. - -Ltac trans Y := - match goal with - | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z)) - | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z)) - | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z)) - | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z)) - | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z)) - end. - -Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop := - forall x y, eqa x y -> eqb (m x) (m y). - -Class [ Setoid a eqa, Setoid b eqb ] => Morphism (m : a -> b) := - respect : respectful m. - -(** Here we build a setoid instance for functions which relates respectful ones only. *) - -Definition respecting [ Setoid a R, Setoid b R' ] : Type := { morph : a -> b | respectful morph }. - -Obligations Tactic := try red ; program_simpl ; unfold equiv in * ; try tauto. - -Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : - Setoid ({ morph : a -> b | respectful morph }) - (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) := - equiv_prf := Build_equivalence _ _ _ _ _. - -Next Obligation. -Proof. - trans (y x0) ; eauto. - apply H. - refl. -Qed. - -Next Obligation. -Proof. - sym ; apply H. - sym ; auto. -Qed. - -(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from - some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *) - -Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] (m : a -> b -> c) : Prop := - forall x y, eqa x y -> - forall z w, eqb z w -> eqc (m x z) (m y w). - -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => BinaryMorphism (m : a -> b -> c) := - respect2 : binary_respectful m. - -Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] (m : a -> b -> c -> d) : Prop := - forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v). - -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => TernaryMorphism (m : a -> b -> c -> d) := - respect3 : ternary_respectful m. - -(** Definition of the usual morphisms in [Prop]. *) - -Program Instance iff_setoid : Setoid Prop iff := - equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym. - -Program Instance not_morphism : Morphism Prop iff Prop iff not. - -Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and. - -(* We make the setoids implicit, they're always [iff] *) - -Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]]. - -Program Instance or_morphism : ? BinaryMorphism or. - -Definition impl (A B : Prop) := A -> B. - -Program Instance impl_morphism : ? BinaryMorphism impl. - -Next Obligation. -Proof. - unfold impl. tauto. -Qed. - -(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) - -Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R. - -Next Obligation. -Proof with auto. - split ; intros. - trans x. sym... trans z... - trans y... trans w... sym... -Qed. - -Definition iff_morphism : BinaryMorphism iff := setoid_morphism. - -Existing Instance iff_morphism. - -Implicit Arguments eq [[A]]. - -Program Instance eq_setoid : Setoid A eq := - equiv_prf := Build_equivalence _ _ _ _ _. - -Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq. - -Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m. - -Implicit Arguments arrow_morphism [[A] [B] [C]]. - -Program Instance type_setoid : Setoid Type (fun x y => x = y) := - equiv_prf := Build_equivalence _ _ _ _ _. - -Lemma setoid_subst : forall (x y : Type), x == y -> x -> y. -Proof. - intros. - rewrite <- H. - apply X. -Qed. - -Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y. -Proof. - intros. - clrewrite <- H. - apply H0. -Qed. - -Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, - ? Morphism sb sc g, ? Morphism sa sb f ] => - compose_morphism : ? Morphism sa sc (fun x => g (f x)). - -Next Obligation. -Proof. - apply (respect (m0:=m)). - apply (respect (m0:=m0)). - assumption. -Qed. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v new file mode 100644 index 0000000000..915a7a944a --- /dev/null +++ b/theories/Classes/SetoidClass.v @@ -0,0 +1,192 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* R y x := equiv_sym _ _ equiv_prf. +Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf. + + +Ltac refl := + match goal with + | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X) + | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X) + | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X) + | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X) + | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X) + end. + +Ltac sym := + match goal with + | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y)) + | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X)) + | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X)) + | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X)) + | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X)) + end. + +Ltac trans Y := + match goal with + | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z)) + | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z)) + | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z)) + | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z)) + | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z)) + end. + +Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop := + forall x y, eqa x y -> eqb (m x) (m y). + +Class [ Setoid a eqa, Setoid b eqb ] => Morphism (m : a -> b) := + respect : respectful m. + +(** Here we build a setoid instance for functions which relates respectful ones only. *) + +Definition respecting [ Setoid a R, Setoid b R' ] : Type := { morph : a -> b | respectful morph }. + +Obligations Tactic := try red ; program_simpl ; unfold equiv in * ; try tauto. + +Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : + Setoid ({ morph : a -> b | respectful morph }) + (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) := + equiv_prf := Build_equivalence _ _ _ _ _. + +Next Obligation. +Proof. + trans (y x0) ; eauto. + apply H. + refl. +Qed. + +Next Obligation. +Proof. + sym ; apply H. + sym ; auto. +Qed. + +(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from + some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *) + +Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] (m : a -> b -> c) : Prop := + forall x y, eqa x y -> + forall z w, eqb z w -> eqc (m x z) (m y w). + +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => BinaryMorphism (m : a -> b -> c) := + respect2 : binary_respectful m. + +Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] (m : a -> b -> c -> d) : Prop := + forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v). + +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => TernaryMorphism (m : a -> b -> c -> d) := + respect3 : ternary_respectful m. + +(** Definition of the usual morphisms in [Prop]. *) + +Program Instance iff_setoid : Setoid Prop iff := + equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym. + +Program Instance not_morphism : Morphism Prop iff Prop iff not. + +Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and. + +(* We make the setoids implicit, they're always [iff] *) + +Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]]. + +Program Instance or_morphism : ? BinaryMorphism or. + +Definition impl (A B : Prop) := A -> B. + +Program Instance impl_morphism : ? BinaryMorphism impl. + +Next Obligation. +Proof. + unfold impl. tauto. +Qed. + +(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) + +Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R. + +Next Obligation. +Proof with auto. + split ; intros. + trans x. sym... trans z... + trans y... trans w... sym... +Qed. + +Definition iff_morphism : BinaryMorphism iff := setoid_morphism. + +Existing Instance iff_morphism. + +Implicit Arguments eq [[A]]. + +Program Instance eq_setoid : Setoid A eq := + equiv_prf := Build_equivalence _ _ _ _ _. + +Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq. + +Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m. + +Implicit Arguments arrow_morphism [[A] [B] [C]]. + +Program Instance type_setoid : Setoid Type (fun x y => x = y) := + equiv_prf := Build_equivalence _ _ _ _ _. + +Lemma setoid_subst : forall (x y : Type), x == y -> x -> y. +Proof. + intros. + rewrite <- H. + apply X. +Qed. + +Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y. +Proof. + intros. + clrewrite <- H. + apply H0. +Qed. + +Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, + ? Morphism sb sc g, ? Morphism sa sb f ] => + compose_morphism : ? Morphism sa sc (fun x => g (f x)). + +Next Obligation. +Proof. + apply (respect (m0:=m)). + apply (respect (m0:=m0)). + assumption. +Qed. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 8e037db1a3..4832f1d72f 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -19,7 +19,7 @@ Require Import Coq.Program.Program. Set Implicit Arguments. Unset Strict Implicit. -Require Export Coq.Classes.Setoid. +Require Export Coq.Classes.SetoidClass. Ltac rew H := clrewrite H. -- cgit v1.2.3