From d35d4a8c279cc39d54037ceb97510b56d12e6a1a Mon Sep 17 00:00:00 2001 From: clrenard Date: Wed, 19 Sep 2001 12:03:50 +0000 Subject: Deplacement des setoides. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 18 ++++++----- .depend.coq | 6 ++-- Makefile | 6 ++-- tactics/setoid_replace.ml | 2 +- theories/Init/Setoid.v | 77 ----------------------------------------------- theories/Setoids/Setoid.v | 75 +++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 94 insertions(+), 90 deletions(-) delete mode 100644 theories/Init/Setoid.v create mode 100644 theories/Setoids/Setoid.v diff --git a/.depend b/.depend index 91dc5dc804..327d963ff0 100644 --- a/.depend +++ b/.depend @@ -258,12 +258,12 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \ contrib/extraction/extraction.cmi: kernel/environ.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi contrib/extraction/haskell.cmi: contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmi + contrib/extraction/mlutil.cmi kernel/term.cmi contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \ kernel/term.cmi contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi + contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi contrib/interface/dad.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \ proofs/tacmach.cmi contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \ @@ -1391,12 +1391,14 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \ - lib/options.cmi parsing/pcoq.cmi lib/pp.cmi library/states.cmi \ - lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ - lib/options.cmx parsing/pcoq.cmx lib/pp.cmx library/states.cmx \ - lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ + lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ + lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx toplevel/vernac.cmi contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ contrib/correctness/past.cmi contrib/correctness/penv.cmi \ contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ diff --git a/.depend.coq b/.depend.coq index 1838da5535..1a773e9321 100644 --- a/.depend.coq +++ b/.depend.coq @@ -38,6 +38,7 @@ theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v theories/Sets/Cpo.vo: theories/Sets/Cpo.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo +theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v tactics/Setoid_replace.vo theories/Relations/Rstar.vo: theories/Relations/Rstar.v theories/Relations/Relations.vo: theories/Relations/Relations.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Operators_Properties.vo theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo @@ -119,7 +120,6 @@ theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theo theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo -theories/Init/Setoid.vo: theories/Init/Setoid.v theories/Init/Logic.vo tactics/Setoid_replace.vo tactics/Inv.vo theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo @@ -212,9 +212,11 @@ test-suite/failure/Case10.vo: test-suite/failure/Case10.v test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo +contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo +contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/ZArith/ZArith.vo theories/Logic/Eqdep_dec.vo contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo contrib/ring/ring.cmo -contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Init/Setoid.vo +contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo diff --git a/Makefile b/Makefile index 87b4daf0e9..f3eb31b3d1 100644 --- a/Makefile +++ b/Makefile @@ -331,7 +331,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic.vo theories/Init/Specif.vo \ theories/Init/LogicSyntax.vo theories/Init/SpecifSyntax.vo \ theories/Init/Logic_Type.vo theories/Init/Wf.vo \ - theories/Init/Logic_TypeSyntax.vo theories/Init/Setoid.vo + theories/Init/Logic_TypeSyntax.vo theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) $(COQC) -boot -$(BEST) -R theories Coq -is states/barestate.coq $< @@ -438,9 +438,11 @@ REALSVO=theories/Reals/TypeSyntax.vo \ theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo \ theories/Reals/Reals.vo +SETOIDSVO=theories/Setoids/Setoid.v + THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) $(LISTSVO) \ $(SETSVO) $(INTMAPVO) $(RELATIONSVO) $(WELLFOUNDEDVO) \ - $(REALSVO) $(SETOIDVO) + $(REALSVO) $(SETOIDSVO) $(THEORIESVO): states/initial.coq diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index f7eb0bbd42..cc18b64c1f 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -39,7 +39,7 @@ type morphism = let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c let constant dir s = - let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::dir)) in + let dir = make_dirpath (List.map id_of_string ("Coq"::"Setoids"::dir)) in let id = id_of_string s in try Declare.global_reference_in_absolute_module dir id diff --git a/theories/Init/Setoid.v b/theories/Init/Setoid.v deleted file mode 100644 index c09888ac3d..0000000000 --- a/theories/Init/Setoid.v +++ /dev/null @@ -1,77 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A -> Prop. - -Record Setoid_Theory : Prop := -{ Seq_refl : (x:A) (Aeq x x); - Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x); - Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z) -}. - -End Setoid. - -Definition Prop_S : (Setoid_Theory Prop iff). -Split; [Exact iff_refl | Exact iff_sym | Exact iff_trans]. -Save. - -Add Setoid Prop iff Prop_S. - -Hint prop_set : setoid := Resolve (Seq_refl Prop iff Prop_S). -Hint prop_set : setoid := Resolve (Seq_sym Prop iff Prop_S). -Hint prop_set : setoid := Resolve (Seq_trans Prop iff Prop_S). - -Add Morphism or : or_ext. -Intros. -Inversion H1. -Left. -Inversion H. -Apply (H3 H2). - -Right. -Inversion H0. -Apply (H3 H2). -Save. - -Add Morphism and : and_ext. -Intros. -Inversion H1. -Split. -Inversion H. -Apply (H4 H2). - -Inversion H0. -Apply (H4 H3). -Save. - -Add Morphism not : not_ext. -Red ; Intros. -Apply H0. -Inversion H. -Apply (H3 H1). -Save. - -Definition fleche [A,B:Prop] := A -> B. - -Add Morphism fleche : fleche_ext. -Unfold fleche. -Intros. -Inversion H0. -Inversion H. -Apply (H3 (H1 (H6 H2))). -Save. - diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v new file mode 100644 index 0000000000..80dfe2d633 --- /dev/null +++ b/theories/Setoids/Setoid.v @@ -0,0 +1,75 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* A -> Prop. + +Record Setoid_Theory : Prop := +{ Seq_refl : (x:A) (Aeq x x); + Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x); + Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z) +}. + +End Setoid. + +Definition Prop_S : (Setoid_Theory Prop iff). +Split; [Exact iff_refl | Exact iff_sym | Exact iff_trans]. +Save. + +Add Setoid Prop iff Prop_S. + +Hint prop_set : setoid := Resolve (Seq_refl Prop iff Prop_S). +Hint prop_set : setoid := Resolve (Seq_sym Prop iff Prop_S). +Hint prop_set : setoid := Resolve (Seq_trans Prop iff Prop_S). + +Add Morphism or : or_ext. +Intros. +Inversion H1. +Left. +Inversion H. +Apply (H3 H2). + +Right. +Inversion H0. +Apply (H3 H2). +Save. + +Add Morphism and : and_ext. +Intros. +Inversion H1. +Split. +Inversion H. +Apply (H4 H2). + +Inversion H0. +Apply (H4 H3). +Save. + +Add Morphism not : not_ext. +Red ; Intros. +Apply H0. +Inversion H. +Apply (H3 H1). +Save. + +Definition fleche [A,B:Prop] := A -> B. + +Add Morphism fleche : fleche_ext. +Unfold fleche. +Intros. +Inversion H0. +Inversion H. +Apply (H3 (H1 (H6 H2))). +Save. + -- cgit v1.2.3