diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-18 17:58:23 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-18 17:58:23 +0000 |
commit | cb738f93e74b2d11bc5a67e75cf5f6f07e676d77 (patch) | |
tree | 437672694a73f72f2d0ae9268b659e5964a08bd1 | |
parent | 895fcffc774abada4677d52a7dbbb54a85cadec7 (diff) |
Getting rid of the previous implementation of setoid_rewrite which was
unplugged a long time ago.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile.common | 3 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 1 | ||||
-rw-r--r-- | contrib/ring/ring.ml | 26 | ||||
-rw-r--r-- | contrib/setoid_ring/newring.ml4 | 1 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 1 | ||||
-rw-r--r-- | tactics/equality.ml | 1 | ||||
-rw-r--r-- | tactics/extraargs.ml4 | 16 | ||||
-rw-r--r-- | tactics/extraargs.mli | 7 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 81 | ||||
-rw-r--r-- | tactics/setoid_replace.ml | 2023 | ||||
-rw-r--r-- | tactics/setoid_replace.mli | 85 | ||||
-rw-r--r-- | theories/Setoids/Setoid_Prop.v | 79 | ||||
-rw-r--r-- | theories/Setoids/Setoid_tac.v | 595 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 1 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 1 |
15 files changed, 13 insertions, 2908 deletions
diff --git a/Makefile.common b/Makefile.common index debec248a..d9d9f2ea0 100644 --- a/Makefile.common +++ b/Makefile.common @@ -215,8 +215,7 @@ TACTICS:=\ tactics/evar_tactics.cmo \ tactics/hiddentac.cmo tactics/elim.cmo \ tactics/dhyp.cmo tactics/auto.cmo \ - toplevel/ind_tables.cmo \ - tactics/setoid_replace.cmo tactics/equality.cmo \ + toplevel/ind_tables.cmo tactics/equality.cmo \ tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \ tactics/tacinterp.cmo tactics/autorewrite.cmo \ tactics/decl_interp.cmo tactics/decl_proof_instr.cmo diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6b65fbcc5..68460c76e 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1906,7 +1906,6 @@ let rec xlate_vernac = xlate_error "TODO: Print TypeClasses" | PrintInspect n -> CT_inspect (CT_int n) | PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s) - | PrintSetoids -> CT_print_setoids | PrintTables -> CT_print_tables | PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a) | PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index eac109cae..adcf51fe8 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -307,14 +307,14 @@ let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false let implement_theory env t th args = is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args)) -(* The following test checks whether the provided morphism is the default - one for the given operation. In principle the test is too strict, since - it should possible to provide another proof for the same fact (proof - irrelevance). In particular, the error message is be not very explicative. *) +(* (\* The following test checks whether the provided morphism is the default *) +(* one for the given operation. In principle the test is too strict, since *) +(* it should possible to provide another proof for the same fact (proof *) +(* irrelevance). In particular, the error message is be not very explicative. *\) *) let states_compatibility_for env plus mult opp morphs = - let check op compat = - is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem - compat in + let check op compat = true in +(* is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem *) +(* compat in *) check plus morphs.plusm && check mult morphs.multm && (match (opp,morphs.oppm) with @@ -826,12 +826,10 @@ let raw_polynom th op lc gl = c'''i; ci; c'i_eq_c''i |])))) (tclTHENS (tclORELSE - (Setoid_replace.general_s_rewrite true - Termops.all_occurrences c'i_eq_c''i - ~new_goals:[]) - (Setoid_replace.general_s_rewrite false - Termops.all_occurrences c'i_eq_c''i - ~new_goals:[])) + (Equality.general_rewrite true + Termops.all_occurrences c'i_eq_c''i) + (Equality.general_rewrite false + Termops.all_occurrences c'i_eq_c''i)) [tac])) else (tclORELSE @@ -881,7 +879,7 @@ let guess_equiv_tac th = let match_with_equiv c = match (kind_of_term c) with | App (e,a) -> - if (List.mem e (Setoid_replace.equiv_list ())) + if (List.mem e []) (* (Setoid_replace.equiv_list ())) *) then Some (decompose_app c) else None | _ -> None diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index fc66b1c97..617ee4bed 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -25,7 +25,6 @@ open Tacexpr open Pcoq open Tactic open Constr -open Setoid_replace open Proof_type open Coqlib open Tacmach diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 113b2f040..0a4cd5e29 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -903,7 +903,6 @@ let rec pr_vernac = function | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid | PrintInspect n -> str"Inspect" ++ spc() ++ int n - | PrintSetoids -> str"Print Setoids" | PrintScopes -> str"Print Scopes" | PrintScope s -> str"Print Scope" ++ spc() ++ str s | PrintVisibility s -> str"Print Visibility" ++ pr_opt str s diff --git a/tactics/equality.ml b/tactics/equality.ml index 884a04e8f..721623c91 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -37,7 +37,6 @@ open Tacred open Rawterm open Coqlib open Vernacexpr -open Setoid_replace open Declarations open Indrec open Printer diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index f02ef6dfc..0eb4a76f3 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -98,22 +98,6 @@ ARGUMENT EXTEND occurrences | [ var(id) ] -> [ ArgVar id ] END -(* For Setoid rewrite *) -let pr_morphism_signature _ _ _ s = - spc () ++ Setoid_replace.pr_morphism_signature s - -ARGUMENT EXTEND morphism_signature - TYPED AS morphism_signature - PRINTED BY pr_morphism_signature - | [ constr(out) ] -> [ [],out ] - | [ constr(c) "++>" morphism_signature(s) ] -> - [ let l,out = s in (Some true,c)::l,out ] - | [ constr(c) "-->" morphism_signature(s) ] -> - [ let l,out = s in (Some false,c)::l,out ] - | [ constr(c) "==>" morphism_signature(s) ] -> - [ let l,out = s in (None,c)::l,out ] -END - let pr_gen prc _prlc _prtac c = prc c let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 85ec60078..b27d8fffc 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -24,13 +24,6 @@ val occurrences : (int list or_var) Pcoq.Gram.Entry.e val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type -val rawwit_morphism_signature : - Setoid_replace.morphism_signature raw_abstract_argument_type -val wit_morphism_signature : - Setoid_replace.morphism_signature typed_abstract_argument_type -val morphism_signature : - Setoid_replace.morphism_signature Pcoq.Gram.Entry.e - val rawwit_raw : constr_expr raw_abstract_argument_type val wit_raw : rawconstr typed_abstract_argument_type val raw : constr_expr Pcoq.Gram.Entry.e diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 285aec91c..d3aba0689 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -217,87 +217,6 @@ END let refine_tac = h_refine -(* Setoid_replace *) - -open Setoid_replace - -(* TACTIC EXTEND setoid_replace *) -(* [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] *) -(* END *) - -(* TACTIC EXTEND setoid_rewrite *) -(* [ "setoid_rewrite" orient(b) constr(c) ] *) -(* -> [ general_s_rewrite b c ~new_goals:[] ] *) -(* | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] *) -(* -> [ general_s_rewrite b c ~new_goals:l ] *) -(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> *) -(* [ general_s_rewrite_in h b c ~new_goals:[] ] *) -(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> *) -(* [ general_s_rewrite_in h b c ~new_goals:l ] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddSetoid1 *) -(* [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> *) -(* [ add_setoid n a aeq t ] *) -(* | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> *) -(* [ new_named_morphism n m None ] *) -(* | [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> *) -(* [ new_named_morphism n m (Some s)] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddRelation1 *) -(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) (Some t') None ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) None None ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> *) -(* [ add_relation n a aeq None None None ] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddRelation2 *) -(* [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) -(* [ add_relation n a aeq None (Some t') None ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) -(* [ add_relation n a aeq None (Some t') (Some t'') ] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddRelation3 *) -(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) None (Some t') ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) (Some t') (Some t'') ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> *) -(* [ add_relation n a aeq None None (Some t) ] *) -(* END *) - -(* TACTIC EXTEND setoid_symmetry *) -(* [ "setoid_symmetry" ] -> [ setoid_symmetry ] *) -(* | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] *) -(* END *) - -(* TACTIC EXTEND setoid_reflexivity *) -(* [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] *) -(* END *) - -(* TACTIC EXTEND setoid_transitivity *) -(* [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] *) -(* END *) - (* Inversion lemmas (Leminv) *) open Inv diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml deleted file mode 100644 index fcb1d2bb5..000000000 --- a/tactics/setoid_replace.ml +++ /dev/null @@ -1,2023 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Tacmach -open Proof_type -open Libobject -open Reductionops -open Term -open Termops -open Names -open Entries -open Libnames -open Nameops -open Util -open Pp -open Printer -open Environ -open Clenv -open Unification -open Tactics -open Tacticals -open Vernacexpr -open Safe_typing -open Nametab -open Decl_kinds -open Constrintern -open Mod_subst - -let replace = ref (fun _ _ _ -> assert false) -let register_replace f = replace := f - -let general_rewrite = ref (fun _ _ -> assert false) -let register_general_rewrite f = general_rewrite := f - -(* util function; it should be in util.mli *) -let prlist_with_sepi sep elem = - let rec aux n = - function - | [] -> mt () - | [h] -> elem n h - | h::t -> - let e = elem n h and s = sep() and r = aux (n+1) t in - e ++ s ++ r - in - aux 1 - -type relation = - { rel_a: constr ; - rel_aeq: constr; - rel_refl: constr option; - rel_sym: constr option; - rel_trans : constr option; - rel_quantifiers_no: int (* it helps unification *); - rel_X_relation_class: constr; - rel_Xreflexive_relation_class: constr - } - -type 'a relation_class = - Relation of 'a (* the rel_aeq of the relation or the relation *) - | Leibniz of constr option (* the carrier (if eq is partially instantiated) *) - -type 'a morphism = - { args : (bool option * 'a relation_class) list; - output : 'a relation_class; - lem : constr; - morphism_theory : constr - } - -type funct = - { f_args : constr list; - f_output : constr - } - -type morphism_class = - ACMorphism of relation morphism - | ACFunction of funct - -let subst_mps_in_relation_class subst = - function - Relation t -> Relation (subst_mps subst t) - | Leibniz t -> Leibniz (Option.map (subst_mps subst) t) - -let subst_mps_in_argument_class subst (variance,rel) = - variance, subst_mps_in_relation_class subst rel - -let constr_relation_class_of_relation_relation_class = - function - Relation relation -> Relation relation.rel_aeq - | Leibniz t -> Leibniz t - - -let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c - -let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s -let gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s -let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s -let eval_reference dir s = EvalConstRef (destConst (constant dir s)) -let eval_init_reference dir s = EvalConstRef (destConst (gen_constant ("Init"::dir) s)) - -let current_constant id = - try - global_reference id - with Not_found -> - anomalylabstrm "" - (str "Setoid: cannot find " ++ pr_id id ++ - str "(if loading Setoid.v under coqtop, use option \"-top Coq.Setoids.Setoid_tac\")") - -(* From Setoid.v *) - -let coq_reflexive = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "reflexive") -let coq_symmetric = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "symmetric") -let coq_transitive = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "transitive") -let coq_relation = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "relation") - -let coq_Relation_Class = lazy(constant ["Setoid_tac"] "Relation_Class") -let coq_Argument_Class = lazy(constant ["Setoid_tac"] "Argument_Class") -let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory") -let coq_Morphism_Theory = lazy(constant ["Setoid_tac"] "Morphism_Theory") -let coq_Build_Morphism_Theory= lazy(constant ["Setoid_tac"] "Build_Morphism_Theory") -let coq_Compat = lazy(constant ["Setoid_tac"] "Compat") - -let coq_AsymmetricReflexive = lazy(constant ["Setoid_tac"] "AsymmetricReflexive") -let coq_SymmetricReflexive = lazy(constant ["Setoid_tac"] "SymmetricReflexive") -let coq_SymmetricAreflexive = lazy(constant ["Setoid_tac"] "SymmetricAreflexive") -let coq_AsymmetricAreflexive = lazy(constant ["Setoid_tac"] "AsymmetricAreflexive") -let coq_Leibniz = lazy(constant ["Setoid_tac"] "Leibniz") - -let coq_RAsymmetric = lazy(constant ["Setoid_tac"] "RAsymmetric") -let coq_RSymmetric = lazy(constant ["Setoid_tac"] "RSymmetric") -let coq_RLeibniz = lazy(constant ["Setoid_tac"] "RLeibniz") - -let coq_ASymmetric = lazy(constant ["Setoid_tac"] "ASymmetric") -let coq_AAsymmetric = lazy(constant ["Setoid_tac"] "AAsymmetric") - -let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl") -let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym") -let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans") - -let coq_variance = lazy(constant ["Setoid_tac"] "variance") -let coq_Covariant = lazy(constant ["Setoid_tac"] "Covariant") -let coq_Contravariant = lazy(constant ["Setoid_tac"] "Contravariant") -let coq_Left2Right = lazy(constant ["Setoid_tac"] "Left2Right") -let coq_Right2Left = lazy(constant ["Setoid_tac"] "Right2Left") -let coq_MSNone = lazy(constant ["Setoid_tac"] "MSNone") -let coq_MSCovariant = lazy(constant ["Setoid_tac"] "MSCovariant") -let coq_MSContravariant = lazy(constant ["Setoid_tac"] "MSContravariant") - -let coq_singl = lazy(constant ["Setoid_tac"] "singl") -let coq_cons = lazy(constant ["Setoid_tac"] "necons") - -let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_asymmetric_areflexive_transitive_relation") -let coq_equality_morphism_of_symmetric_areflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_symmetric_areflexive_transitive_relation") -let coq_equality_morphism_of_asymmetric_reflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_asymmetric_reflexive_transitive_relation") -let coq_equality_morphism_of_symmetric_reflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_symmetric_reflexive_transitive_relation") -let coq_make_compatibility_goal = - lazy(constant ["Setoid_tac"] "make_compatibility_goal") -let coq_make_compatibility_goal_eval_ref = - lazy(eval_reference ["Setoid_tac"] "make_compatibility_goal") -let coq_make_compatibility_goal_aux_eval_ref = - lazy(eval_reference ["Setoid_tac"] "make_compatibility_goal_aux") - -let coq_App = lazy(constant ["Setoid_tac"] "App") -let coq_ToReplace = lazy(constant ["Setoid_tac"] "ToReplace") -let coq_ToKeep = lazy(constant ["Setoid_tac"] "ToKeep") -let coq_ProperElementToKeep = lazy(constant ["Setoid_tac"] "ProperElementToKeep") -let coq_fcl_singl = lazy(constant ["Setoid_tac"] "fcl_singl") -let coq_fcl_cons = lazy(constant ["Setoid_tac"] "fcl_cons") - -let coq_setoid_rewrite = lazy(constant ["Setoid_tac"] "setoid_rewrite") -let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") -let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") -let coq_unit = lazy(gen_constant ["Init"; "Datatypes"] "unit") -let coq_tt = lazy(gen_constant ["Init"; "Datatypes"] "tt") -let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq") - -let coq_morphism_theory_of_function = - lazy(constant ["Setoid_tac"] "morphism_theory_of_function") -let coq_morphism_theory_of_predicate = - lazy(constant ["Setoid_tac"] "morphism_theory_of_predicate") -let coq_relation_of_relation_class = - lazy(eval_reference ["Setoid_tac"] "relation_of_relation_class") -let coq_directed_relation_of_relation_class = - lazy(eval_reference ["Setoid_tac"] "directed_relation_of_relation_class") -let coq_interp = lazy(eval_reference ["Setoid_tac"] "interp") -let coq_Morphism_Context_rect2 = - lazy(eval_reference ["Setoid_tac"] "Morphism_Context_rect2") -let coq_iff = lazy(gen_constant ["Init";"Logic"] "iff") -let coq_impl = lazy(constant ["Setoid_tac"] "impl") - - -(************************* Table of declared relations **********************) - - -(* Relations are stored in a table which is synchronised with the - Reset mechanism. The table maps the term denoting the relation to - the data of type relation that characterises the relation *) - -let relation_table = ref Gmap.empty - -let relation_table_add (s,th) = relation_table := Gmap.add s th !relation_table -let relation_table_find s = Gmap.find s !relation_table -let relation_table_mem s = Gmap.mem s !relation_table - -let prrelation s = - str "(" ++ pr_lconstr s.rel_a ++ str "," ++ pr_lconstr s.rel_aeq ++ str ")" - -let prrelation_class = - function - Relation eq -> - (try prrelation (relation_table_find eq) - with Not_found -> - str "[[ Error: " ++ pr_lconstr eq ++ - str " is not registered as a relation ]]") - | Leibniz (Some ty) -> pr_lconstr ty - | Leibniz None -> str "_" - -let prmorphism_argument_gen prrelation (variance,rel) = - prrelation rel ++ - match variance with - None -> str " ==> " - | Some true -> str " ++> " - | Some false -> str " --> " - -let prargument_class = prmorphism_argument_gen prrelation_class - -let pr_morphism_signature (l,c) = - prlist (prmorphism_argument_gen Ppconstr.pr_constr_expr) l ++ - Ppconstr.pr_constr_expr c - -let prmorphism k m = - pr_lconstr k ++ str ": " ++ - prlist prargument_class m.args ++ - prrelation_class m.output - - -(* A function that gives back the only relation_class on a given carrier *) -(*CSC: this implementation is really inefficient. I should define a new - map to make it efficient. However, is this really worth of? *) -let default_relation_for_carrier ?(filter=fun _ -> true) a = - let rng = Gmap.rng !relation_table in - match List.filter (fun ({rel_a=rel_a} as r) -> rel_a = a && filter r) rng with - [] -> Leibniz (Some a) - | relation::tl -> - if tl <> [] then - Flags.if_warn msg_warning - (str "There are several relations on the carrier \"" ++ - pr_lconstr a ++ str "\". The relation " ++ prrelation relation ++ - str " is chosen.") ; - Relation relation - -let find_relation_class rel = - try Relation (relation_table_find rel) - with - Not_found -> - let rel = Reduction.whd_betadeltaiota (Global.env ()) rel in - match kind_of_term rel with - | App (eq,[|ty|]) when eq_constr eq (Lazy.force coq_eq) -> Leibniz (Some ty) - | _ when eq_constr rel (Lazy.force coq_eq) -> Leibniz None - | _ -> raise Not_found - -let coq_iff_relation = lazy (find_relation_class (Lazy.force coq_iff)) -let coq_impl_relation = lazy (find_relation_class (Lazy.force coq_impl)) - -let relation_morphism_of_constr_morphism = - let relation_relation_class_of_constr_relation_class = - function - Leibniz t -> Leibniz t - | Relation aeq -> - Relation (try relation_table_find aeq with Not_found -> assert false) - in - function mor -> - let args' = - List.map - (fun (variance,rel) -> - variance, relation_relation_class_of_constr_relation_class rel - ) mor.args in - let output' = relation_relation_class_of_constr_relation_class mor.output in - {mor with args=args' ; output=output'} - -let subst_relation subst relation = - let rel_a' = subst_mps subst relation.rel_a in - let rel_aeq' = subst_mps subst relation.rel_aeq in - let rel_refl' = Option.map (subst_mps subst) relation.rel_refl in - let rel_sym' = Option.map (subst_mps subst) relation.rel_sym in - let rel_trans' = Option.map (subst_mps subst) relation.rel_trans in - let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in - let rel_Xreflexive_relation_class' = - subst_mps subst relation.rel_Xreflexive_relation_class - in - if rel_a' == relation.rel_a - && rel_aeq' == relation.rel_aeq - && rel_refl' == relation.rel_refl - && rel_sym' == relation.rel_sym - && rel_trans' == relation.rel_trans - && rel_X_relation_class' == relation.rel_X_relation_class - && rel_Xreflexive_relation_class'==relation.rel_Xreflexive_relation_class - then - relation - else - { rel_a = rel_a' ; - rel_aeq = rel_aeq' ; - rel_refl = rel_refl' ; - rel_sym = rel_sym'; - rel_trans = rel_trans'; - rel_quantifiers_no = relation.rel_quantifiers_no; - rel_X_relation_class = rel_X_relation_class'; - rel_Xreflexive_relation_class = rel_Xreflexive_relation_class' - } - -let equiv_list () = List.map (fun x -> x.rel_aeq) (Gmap.rng !relation_table) - -let _ = - Summary.declare_summary "relation-table" - { Summary.freeze_function = (fun () -> !relation_table); - Summary.unfreeze_function = (fun t -> relation_table := t); - Summary.init_function = (fun () -> relation_table := Gmap .empty); - Summary.survive_module = false; - Summary.survive_section = false } - -(* Declare a new type of object in the environment : "relation-theory". *) - -let (relation_to_obj, obj_to_relation)= - let cache_set (_,(s, th)) = - let th' = - if relation_table_mem s then - begin - let old_relation = relation_table_find s in - let th' = - {th with rel_sym = - match th.rel_sym with - None -> old_relation.rel_sym - | Some t -> Some t} in - Flags.if_warn msg_warning - (strbrk "The relation " ++ prrelation th' ++ - strbrk " is redeclared. The new declaration" ++ - (match th'.rel_refl with - None -> mt () - | Some t -> strbrk " (reflexivity proved by " ++ pr_lconstr t) ++ - (match th'.rel_sym with - None -> mt () - | Some t -> - (if th'.rel_refl = None then strbrk " (" else strbrk " and ") - ++ strbrk "symmetry proved by " ++ pr_lconstr t) ++ - (if th'.rel_refl <> None && th'.rel_sym <> None then - str ")" else str "") ++ - strbrk " replaces the old declaration" ++ - (match old_relation.rel_refl with - None -> str "" - | Some t -> strbrk " (reflexivity proved by " ++ pr_lconstr t) ++ - (match old_relation.rel_sym with - None -> str "" - | Some t -> - (if old_relation.rel_refl = None then - strbrk " (" else strbrk " and ") ++ - strbrk "symmetry proved by " ++ pr_lconstr t) ++ - (if old_relation.rel_refl <> None && old_relation.rel_sym <> None - then str ")" else str "") ++ - str "."); - th' - end - else - th - in - relation_table_add (s,th') - and subst_set (_,subst,(s,th as obj)) = - let s' = subst_mps subst s in - let th' = subst_relation subst th in - if s' == s && th' == th then obj else - (s',th') - and export_set x = Some x - in - declare_object {(default_object "relation-theory") with - cache_function = cache_set; - load_function = (fun i o -> cache_set o); - subst_function = subst_set; - classify_function = (fun (_,x) -> Substitute x); - export_function = export_set} - -(******************************* Table of declared morphisms ********************) - -(* Setoids are stored in a table which is synchronised with the Reset mechanism. *) - -let morphism_table = ref Gmap.empty - -let morphism_table_find m = Gmap.find m !morphism_table -let morphism_table_add (m,c) = - let old = - try - morphism_table_find m - with - Not_found -> [] - in - try - let old_morph = - List.find - (function mor -> mor.args = c.args && mor.output = c.output) old - in - Flags.if_warn msg_warning - (strbrk "The morphism " ++ prmorphism m old_morph ++ - strbrk " is redeclared. " ++ - strbrk "The new declaration whose compatibility is proved by " ++ - pr_lconstr c.lem ++ strbrk " replaces the old declaration whose" ++ - strbrk " compatibility was proved by " ++ - pr_lconstr old_morph.lem ++ str ".") - with - Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table - -let default_morphism ?(filter=fun _ -> true) m = - match List.filter filter (morphism_table_find m) with - [] -> raise Not_found - | m1::ml -> - if ml <> [] then - Flags.if_warn msg_warning - (strbrk "There are several morphisms associated to \"" ++ - pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ - strbrk " is randomly chosen."); - relation_morphism_of_constr_morphism m1 - -let subst_morph subst morph = - let lem' = subst_mps subst morph.lem in - let args' = list_smartmap (subst_mps_in_argument_class subst) morph.args in - let output' = subst_mps_in_relation_class subst morph.output in - let morphism_theory' = subst_mps subst morph.morphism_theory in - if lem' == morph.lem - && args' == morph.args - && output' == morph.output - && morphism_theory' == morph.morphism_theory - then - morph - else - { args = args' ; - output = output' ; - lem = lem' ; - morphism_theory = morphism_theory' - } - - -let _ = - Summary.declare_summary "morphism-table" - { Summary.freeze_function = (fun () -> !morphism_table); - Summary.unfreeze_function = (fun t -> morphism_table := t); - Summary.init_function = (fun () -> morphism_table := Gmap .empty); - Summary.survive_module = false; - Summary.survive_section = false } - -(* Declare a new type of object in the environment : "morphism-definition". *) - -let (morphism_to_obj, obj_to_morphism)= - let cache_set (_,(m, c)) = morphism_table_add (m, c) - and subst_set (_,subst,(m,c as obj)) = - let m' = subst_mps subst m in - let c' = subst_morph subst c in - if m' == m && c' == c then obj else - (m',c') - and export_set x = Some x - in - declare_object {(default_object "morphism-definition") with - cache_function = cache_set; - load_function = (fun i o -> cache_set o); - subst_function = subst_set; - classify_function = (fun (_,x) -> Substitute x); - export_function = export_set} - -(************************** Printing relations and morphisms **********************) - -let print_setoids () = - Gmap.iter - (fun k relation -> - assert (k=relation.rel_aeq) ; - ppnl (str"Relation " ++ prrelation relation ++ str";" ++ - (match relation.rel_refl with - None -> str "" - | Some t -> str" reflexivity proved by " ++ pr_lconstr t) ++ - (match relation.rel_sym with - None -> str "" - | Some t -> str " symmetry proved by " ++ pr_lconstr t) ++ - (match relation.rel_trans with - None -> str "" - | Some t -> str " transitivity proved by " ++ pr_lconstr t))) - !relation_table ; - Gmap.iter - (fun k l -> - List.iter - (fun ({lem=lem} as mor) -> - ppnl (str "Morphism " ++ prmorphism k mor ++ - str ". Compatibility proved by " ++ - pr_lconstr lem ++ str ".")) - l) !morphism_table -;; - -(***************** Adding a morphism to the database ****************************) - -(* We maintain a table of the currently edited proofs of morphism lemma - in order to add them in the morphism_table when the user does Save *) - -let edited = ref Gmap.empty - -let new_edited id m = - edited := Gmap.add id m !edited - -let is_edited id = - Gmap.mem id !edited - -let no_more_edited id = - edited := Gmap.remove id !edited - -let what_edited id = - Gmap.find id !edited - -(* also returns the triple (args_ty_quantifiers_rev,real_args_ty,real_output) - where the args_ty and the output are delifted *) -let check_is_dependent n args_ty output = - let m = List.length args_ty - n in - let args_ty_quantifiers, args_ty = Util.list_chop n args_ty in - let rec aux m t = - match kind_of_term t with - Prod (n,s,t) when m > 0 -> - if not (dependent (mkRel 1) t) then - let args,out = aux (m - 1) (subst1 (mkRel 1) (* dummy *) t) in - s::args,out - else - errorlabstrm "New Morphism" - (str "The morphism is not a quantified non dependent product.") - | _ -> [],t - in - let ty = compose_prod (List.rev args_ty) output in - let args_ty, output = aux m ty in - List.rev args_ty_quantifiers, args_ty, output - -let cic_relation_class_of_X_relation typ value = - function - {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} -> - mkApp ((Lazy.force coq_AsymmetricReflexive), - [| typ ; value ; rel_a ; rel_aeq; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_SymmetricReflexive), - [| typ ; rel_a ; rel_aeq; sym ; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} -> - mkApp ((Lazy.force coq_AsymmetricAreflexive), - [| typ ; value ; rel_a ; rel_aeq |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_SymmetricAreflexive), - [| typ ; rel_a ; rel_aeq; sym |]) - -let cic_relation_class_of_X_relation_class typ value = - function - Relation {rel_X_relation_class=x_relation_class} -> - mkApp (x_relation_class, [| typ ; value |]) - | Leibniz (Some t) -> - mkApp ((Lazy.force coq_Leibniz), [| typ ; t |]) - | Leibniz None -> assert false - - -let cic_precise_relation_class_of_relation = - function - {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} -> - mkApp ((Lazy.force coq_RAsymmetric), [| rel_a ; rel_aeq; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_RSymmetric), [| rel_a ; rel_aeq; sym ; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} -> - mkApp ((Lazy.force coq_AAsymmetric), [| rel_a ; rel_aeq |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_ASymmetric), [| rel_a ; rel_aeq; sym |]) - -let cic_precise_relation_class_of_relation_class = - function - Relation - {rel_aeq=rel_aeq; rel_Xreflexive_relation_class=lem; rel_refl=rel_refl } - -> - rel_aeq,lem,not(rel_refl=None) - | Leibniz (Some t) -> - mkApp ((Lazy.force coq_eq), [| t |]), - mkApp ((Lazy.force coq_RLeibniz), [| t |]), true - | Leibniz None -> assert false - -let cic_relation_class_of_relation_class rel = - cic_relation_class_of_X_relation_class - (Lazy.force coq_unit) (Lazy.force coq_tt) rel - -let cic_argument_class_of_argument_class (variance,arg) = - let coq_variant_value = - match variance with - None -> (Lazy.force coq_Covariant) (* dummy value, it won't be used *) - | Some true -> (Lazy.force coq_Covariant) - | Some false -> (Lazy.force coq_Contravariant) - in - cic_relation_class_of_X_relation_class (Lazy.force coq_variance) - coq_variant_value arg - -let cic_arguments_of_argument_class_list args = - let rec aux = - function - [] -> assert false - | [last] -> - mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class; last |]) - | he::tl -> - mkApp ((Lazy.force coq_cons), - [| Lazy.force coq_Argument_Class; he ; aux tl |]) - in - aux (List.map cic_argument_class_of_argument_class args) - -let gen_compat_lemma_statement quantifiers_rev output args m = - let output = cic_relation_class_of_relation_class output in - let args = cic_arguments_of_argument_class_list args in - args, output, - compose_prod quantifiers_rev - (mkApp ((Lazy.force coq_make_compatibility_goal), [| args ; output ; m |])) - -let morphism_theory_id_of_morphism_proof_id id = - id_of_string (string_of_id id ^ "_morphism_theory") - -(* apply_to_rels c [l1 ; ... ; ln] returns (c Rel1 ... reln) *) -let apply_to_rels c l = - if l = [] then c - else - let len = List.length l in - applistc c (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 l) - -let apply_to_relation subst rel = - if Array.length subst = 0 then rel - else - let new_quantifiers_no = rel.rel_quantifiers_no - Array.length subst in - assert (new_quantifiers_no >= 0) ; - { rel_a = mkApp (rel.rel_a, subst) ; - rel_aeq = mkApp (rel.rel_aeq, subst) ; - rel_refl = Option.map (fun c -> mkApp (c,subst)) rel.rel_refl ; - rel_sym = Option.map (fun c -> mkApp (c,subst)) rel.rel_sym; - rel_trans = Option.map (fun c -> mkApp (c,subst)) rel.rel_trans; - rel_quantifiers_no = new_quantifiers_no; - rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst); - rel_Xreflexive_relation_class = - mkApp (rel.rel_Xreflexive_relation_class, subst) } - -let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = - let lem = - match lemma_infos with - None -> - (* the Morphism_Theory object has already been created *) - let applied_args = - let len = List.length quantifiers_rev in - let subst = - Array.of_list - (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 quantifiers_rev) - in - List.map - (fun (v,rel) -> - match rel with - Leibniz (Some t) -> - assert (subst=[||]); - v, Leibniz (Some t) - | Leibniz None -> - assert (Array.length subst = 1); - v, Leibniz (Some (subst.(0))) - | Relation rel -> v, Relation (apply_to_relation subst rel)) args - in - compose_lam quantifiers_rev - (mkApp (Lazy.force coq_Compat, - [| cic_arguments_of_argument_class_list applied_args; - cic_relation_class_of_relation_class output; - apply_to_rels (current_constant mor_name) quantifiers_rev |])) - | Some (lem_name,argsconstr,outputconstr) -> - (* only the compatibility has been proved; we need to declare the - Morphism_Theory object *) - let mext = current_constant lem_name in - ignore ( - Declare.declare_internal_constant mor_name - (DefinitionEntry - {const_entry_body = - compose_lam quantifiers_rev - (mkApp ((Lazy.force coq_Build_Morphism_Theory), - [| argsconstr; outputconstr; apply_to_rels m quantifiers_rev ; - apply_to_rels mext quantifiers_rev |])); - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()}, - IsDefinition Definition)) ; - mext - in - let mmor = current_constant mor_name in - let args_constr = - List.map - (fun (variance,arg) -> - variance, constr_relation_class_of_relation_relation_class arg) args in - let output_constr = constr_relation_class_of_relation_relation_class output in - Lib.add_anonymous_leaf - (morphism_to_obj (m, - { args = args_constr; - output = output_constr; - lem = lem; - morphism_theory = mmor })); - Flags.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism") - -let error_cannot_unify_signature env k t t' = - errorlabstrm "New Morphism" - (str "One morphism argument or its output has type" ++ spc() ++ - pr_lconstr_env env t ++ strbrk " but the signature requires an argument" ++ - (if k = 0 then strbrk " of type " else - strbrk "whose type is an instance of ") ++ pr_lconstr_env env t' ++ - str ".") - -(* first order matching with a bit of conversion *) -let unify_relation_carrier_with_type env rel t = - let args = - match kind_of_term t with - App (he',args') -> - let argsno = Array.length args' - rel.rel_quantifiers_no in - let args1 = Array.sub args' 0 argsno in - let args2 = Array.sub args' argsno rel.rel_quantifiers_no in - if is_conv env Evd.empty rel.rel_a (mkApp (he',args1)) then - args2 - else - error_cannot_unify_signature env rel.rel_quantifiers_no t rel.rel_a - | _ -> - try - let args = - Clenv.clenv_conv_leq env Evd.empty t rel.rel_a rel.rel_quantifiers_no - in - Array.of_list args - with Reduction.NotConvertible -> - error_cannot_unify_signature env rel.rel_quantifiers_no t rel.rel_a - in - apply_to_relation args rel - -let unify_relation_class_carrier_with_type env rel t = - match rel with - Leibniz (Some t') -> - if is_conv env Evd.empty t t' then - rel - else - error_cannot_unify_signature env 0 t t' - | Leibniz None -> Leibniz (Some t) - | Relation rel -> Relation (unify_relation_carrier_with_type env rel t) - -exception Impossible - -(* first order matching with a bit of conversion *) -(* Note: the type checking operations performed by the function could *) -(* be done once and for all abstracting the morphism structure using *) -(* the quantifiers. Would the new structure be more suited than the *) -(* existent one for other tasks to? (e.g. pretty printing would expose *) -(* much more information: is it ok or is it too much information?) *) -let unify_morphism_with_arguments gl (c,av) - {args=args; output=output; lem=lem; morphism_theory=morphism_theory} t -= - let avlen = Array.length av in - let argsno = List.length args in - if avlen < argsno then raise Impossible; (* partial application *) - let al = Array.to_list av in - let quantifiers,al' = Util.list_chop (avlen - argsno) al in - let quantifiersv = Array.of_list quantifiers in - let c' = mkApp (c,quantifiersv) in - if dependent t c' then raise Impossible; - (* these are pf_type_of we could avoid *) - let al'_type = List.map (Tacmach.pf_type_of gl) al' in - let args' = - List.map2 - (fun (var,rel) ty -> - var,unify_relation_class_carrier_with_type (pf_env gl) rel ty) - args al'_type in - (* this is another pf_type_of we could avoid *) - let ty = Tacmach.pf_type_of gl (mkApp (c,av)) in - let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty in - let lem' = mkApp (lem,quantifiersv) in - let morphism_theory' = mkApp (morphism_theory,quantifiersv) in - ({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'}, - c',Array.of_list al') - -let new_morphism m signature id hook = - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - errorlabstrm "New Morphism" (pr_id id ++ str " already exists") - else - let env = Global.env() in - let typeofm = Typing.type_of env Evd.empty m in - let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in - let argsrev, output = - match signature with - None -> decompose_prod typ - | Some (_,output') -> - (* the carrier of the relation output' can be a Prod ==> - we must uncurry on the fly output. - E.g: A -> B -> C vs A -> (B -> C) - args output args output - *) - let rel = - try find_relation_class output' - with Not_found -> errorlabstrm "Add Morphism" - (str "Not a valid signature: " ++ pr_lconstr output' ++ - str " is neither a registered relation nor the Leibniz " ++ - str " equality.") in - let rel_a,rel_quantifiers_no = - match rel with - Relation rel -> rel.rel_a, rel.rel_quantifiers_no - | Leibniz (Some t) -> t, 0 - | Leibniz None -> let _,t = decompose_prod typ in t, 0 in - let rel_a_n = - clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a - in - try - let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in - let argsrev,_ = decompose_prod output_rel_a_n in - let n = List.length argsrev in - let argsrev',_ = decompose_prod typ in - let m = List.length argsrev' in - decompose_prod_n (m - n) typ - with UserError(_,_) -> - (* decompose_lam_n failed. This may happen when rel_a is an axiom, - a constructor, an inductive type, etc. *) - decompose_prod typ - in - let args_ty = List.rev argsrev in - let args_ty_len = List.length (args_ty) in - let args_ty_quantifiers_rev,args,args_instance,output,output_instance = - match signature with - None -> - if args_ty = [] then - errorlabstrm "New Morphism" - (str "The term " ++ pr_lconstr m ++ str " has type " ++ - pr_lconstr typeofm ++ str " that is not a product.") ; - ignore (check_is_dependent 0 args_ty output) ; - let args = - List.map - (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in - let output = default_relation_for_carrier output in - [],args,args,output,output - | Some (args,output') -> - assert (args <> []); - let number_of_arguments = List.length args in - let number_of_quantifiers = args_ty_len - number_of_arguments in - if number_of_quantifiers < 0 then - errorlabstrm "New Morphism" - (str "The morphism " ++ pr_lconstr m ++ str " has type " ++ - pr_lconstr typeofm ++ str " that expects at most " ++ int args_ty_len ++ - str " arguments. The signature that you specified requires " ++ - int number_of_arguments ++ str " arguments.") - else - begin - (* the real_args_ty returned are already delifted *) - let args_ty_quantifiers_rev, real_args_ty, real_output = - check_is_dependent number_of_quantifiers args_ty output in - let quantifiers_rel_context = - List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in - let env = push_rel_context quantifiers_rel_context env in - let find_relation_class t real_t = - try - let rel = find_relation_class t in - rel, unify_relation_class_carrier_with_type env rel real_t - with Not_found -> - errorlabstrm "Add Morphism" - (str "Not a valid signature: " ++ pr_lconstr t ++ - str " is neither a registered relation nor the Leibniz " ++ - str " equality.") - in - let find_relation_class_v (variance,t) real_t = - let relation,relation_instance = find_relation_class t real_t in - match relation, variance with - Leibniz _, None - | Relation {rel_sym = Some _}, None - | Relation {rel_sym = None}, Some _ -> - (variance, relation), (variance, relation_instance) - | Relation {rel_sym = None},None -> - errorlabstrm "Add Morphism" - (str "You must specify the variance in each argument " ++ - str "whose relation is asymmetric.") - | Leibniz _, Some _ - | Relation {rel_sym = Some _}, Some _ -> - errorlabstrm "Add Morphism" - (str "You cannot specify the variance of an argument " ++ - str "whose relation is symmetric.") - in - let args, args_instance = - List.split - (List.map2 find_relation_class_v args real_args_ty) in - let output,output_instance= find_relation_class output' real_output in - args_ty_quantifiers_rev, args, args_instance, output, output_instance - end - in - let argsconstr,outputconstr,lem = - gen_compat_lemma_statement args_ty_quantifiers_rev output_instance - args_instance (apply_to_rels m args_ty_quantifiers_rev) in - (* "unfold make_compatibility_goal" *) - let lem = - Reductionops.clos_norm_flags - (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref)) - env Evd.empty lem in - (* "unfold make_compatibility_goal_aux" *) - let lem = - Reductionops.clos_norm_flags - (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref)) - env Evd.empty lem in - (* "simpl" *) - let lem = Tacred.simpl env Evd.empty lem in - if Lib.is_modtype () then - begin - ignore - (Declare.declare_internal_constant id - (ParameterEntry (lem,false), IsAssumption Logical)) ; - let mor_name = morphism_theory_id_of_morphism_proof_id id in - let lemma_infos = Some (id,argsconstr,outputconstr) in - add_morphism lemma_infos mor_name - (m,args_ty_quantifiers_rev,args,output) - end - else - begin - new_edited id - (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr); - Pfedit.start_proof id (Global, Proof Lemma) - (Decls.clear_proofs (Global.named_context ())) - lem hook; - Flags.if_verbose msg (Printer.pr_open_subgoals ()); - end - -let morphism_hook _ ref = - let pf_id = id_of_global ref in - let mor_id = morphism_theory_id_of_morphism_proof_id pf_id in - let (m,quantifiers_rev,args,argsconstr,output,outputconstr) = - what_edited pf_id in - if (is_edited pf_id) - then - begin - add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id - (m,quantifiers_rev,args,output) ; - no_more_edited pf_id - end - -type morphism_signature = - (bool option * Topconstr.constr_expr) list * Topconstr.constr_expr - -let new_named_morphism id m sign = - Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - let sign = - match sign with - None -> None - | Some (args,out) -> - if args = [] then - error "Morphism signature expects at least one argument."; - Some - (List.map (fun (variance,ty) -> variance, constr_of ty) args, - constr_of out) - in - new_morphism (constr_of m) sign id morphism_hook - -(************************** Adding a relation to the database *********************) - -let check_a env a = - let typ = Typing.type_of env Evd.empty a in - let a_quantifiers_rev,_ = Reduction.dest_arity env typ in - a_quantifiers_rev - -let check_eq env a_quantifiers_rev a aeq = - let typ = - it_mkProd_or_LetIn - (mkApp ((Lazy.force coq_relation),[| apply_to_rels a a_quantifiers_rev |])) - a_quantifiers_rev in - if - not - (is_conv env Evd.empty (Typing.type_of env Evd.empty aeq) typ) - then - errorlabstrm "Add Relation Class" - (pr_lconstr aeq ++ str " should have type (" ++ pr_lconstr typ ++ str ")") - -let check_property env a_quantifiers_rev a aeq strprop coq_prop t = - if - not - (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (it_mkProd_or_LetIn - (mkApp ((Lazy.force coq_prop), - [| apply_to_rels a a_quantifiers_rev ; - apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev)) - then - errorlabstrm "Add Relation Class" - (str "Not a valid proof of " ++ str strprop ++ str ".") - -let check_refl env a_quantifiers_rev a aeq refl = - check_property env a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl - -let check_sym env a_quantifiers_rev a aeq sym = - check_property env a_quantifiers_rev a aeq "symmetry" coq_symmetric sym - -let check_trans env a_quantifiers_rev a aeq trans = - check_property env a_quantifiers_rev a aeq "transitivity" coq_transitive trans - -let check_setoid_theory env a_quantifiers_rev a aeq th = - if - not - (is_conv env Evd.empty (Typing.type_of env Evd.empty th) - (it_mkProd_or_LetIn - (mkApp ((Lazy.force coq_Setoid_Theory), - [| apply_to_rels a a_quantifiers_rev ; - apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev)) - then - errorlabstrm "Add Relation Class" - (str "Not a valid proof of symmetry") - -let int_add_relation id a aeq refl sym trans = - let env = Global.env () in - let a_quantifiers_rev = check_a env a in - check_eq env a_quantifiers_rev a aeq ; - Option.iter (check_refl env a_quantifiers_rev a aeq) refl ; - Option.iter (check_sym env a_quantifiers_rev a aeq) sym ; - Option.iter (check_trans env a_quantifiers_rev a aeq) trans ; - let quantifiers_no = List.length a_quantifiers_rev in - let aeq_rel = - { rel_a = a; - rel_aeq = aeq; - rel_refl = refl; - rel_sym = sym; - rel_trans = trans; - rel_quantifiers_no = quantifiers_no; - rel_X_relation_class = mkProp; (* dummy value, overwritten below *) - rel_Xreflexive_relation_class = mkProp (* dummy value, overwritten below *) - } in - let x_relation_class = - let subst = - let len = List.length a_quantifiers_rev in - Array.of_list - (Util.list_map_i (fun i _ -> mkRel (len - i + 2)) 0 a_quantifiers_rev) in - cic_relation_class_of_X_relation - (mkRel 2) (mkRel 1) (apply_to_relation subst aeq_rel) in - let _ = - Declare.declare_internal_constant id - (DefinitionEntry - {const_entry_body = - it_mkLambda_or_LetIn x_relation_class - ([ Name (id_of_string "v"),None,mkRel 1; - Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @ - a_quantifiers_rev); - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()}, - IsDefinition Definition) in - let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in - let xreflexive_relation_class = - let subst = - let len = List.length a_quantifiers_rev in - Array.of_list - (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 a_quantifiers_rev) - in - cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in - let _ = - Declare.declare_internal_constant id_precise - (DefinitionEntry - {const_entry_body = - it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, - IsDefinition Definition) in - let aeq_rel = - { aeq_rel with - rel_X_relation_class = current_constant id; - rel_Xreflexive_relation_class = current_constant id_precise } in - Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ; - Flags.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation"); - match trans with - None -> () - | Some trans -> - let mor_name = id_of_string (string_of_id id ^ "_morphism") in - let a_instance = apply_to_rels a a_quantifiers_rev in - let aeq_instance = apply_to_rels aeq a_quantifiers_rev in - let sym_instance = - Option.map (fun x -> apply_to_rels x a_quantifiers_rev) sym in - let refl_instance = - Option.map (fun x -> apply_to_rels x a_quantifiers_rev) refl in - let trans_instance = apply_to_rels trans a_quantifiers_rev in - let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output = - match sym_instance, refl_instance with - None, None -> - (Some false, Relation aeq_rel), - (Some true, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_asymmetric_areflexive_transitive_relation), - [| a_instance ; aeq_instance ; trans_instance |]), - Lazy.force coq_impl_relation - | None, Some refl_instance -> - (Some false, Relation aeq_rel), - (Some true, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_asymmetric_reflexive_transitive_relation), - [| a_instance ; aeq_instance ; refl_instance ; trans_instance |]), - Lazy.force coq_impl_relation - | Some sym_instance, None -> - (None, Relation aeq_rel), - (None, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_symmetric_areflexive_transitive_relation), - [| a_instance ; aeq_instance ; sym_instance ; trans_instance |]), - Lazy.force coq_iff_relation - | Some sym_instance, Some refl_instance -> - (None, Relation aeq_rel), - (None, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_symmetric_reflexive_transitive_relation), - [| a_instance ; aeq_instance ; refl_instance ; sym_instance ; - trans_instance |]), - Lazy.force coq_iff_relation in - let _ = - Declare.declare_internal_constant mor_name - (DefinitionEntry - {const_entry_body = it_mkLambda_or_LetIn lemma a_quantifiers_rev; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()}, - IsDefinition Definition) - in - let a_quantifiers_rev = - List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in - add_morphism None mor_name - (aeq,a_quantifiers_rev,[aeq_rel_class_and_var1; aeq_rel_class_and_var2], - output) - -(* The vernac command "Add Relation ..." *) -let add_relation id a aeq refl sym trans = - Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - int_add_relation id (constr_of a) (constr_of aeq) (Option.map constr_of refl) - (Option.map constr_of sym) (Option.map constr_of trans) - -(************************ Add Setoid ******************************************) - -(* The vernac command "Add Setoid" *) -let add_setoid id a aeq th = - Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - let a = constr_of a in - let aeq = constr_of aeq in - let th = constr_of th in - let env = Global.env () in - let a_quantifiers_rev = check_a env a in - check_eq env a_quantifiers_rev a aeq ; - check_setoid_theory env a_quantifiers_rev a aeq th ; - let a_instance = apply_to_rels a a_quantifiers_rev in - let aeq_instance = apply_to_rels aeq a_quantifiers_rev in - let th_instance = apply_to_rels th a_quantifiers_rev in - let refl = - it_mkLambda_or_LetIn - (mkApp ((Lazy.force coq_seq_refl), - [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in - let sym = - it_mkLambda_or_LetIn - (mkApp ((Lazy.force coq_seq_sym), - [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in - let trans = - it_mkLambda_or_LetIn - (mkApp ((Lazy.force coq_seq_trans), - [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in - int_add_relation id a aeq (Some refl) (Some sym) (Some trans) - - -(****************************** The tactic itself *******************************) - -type direction = - Left2Right - | Right2Left - -let prdirection = - function - Left2Right -> str "->" - | Right2Left -> str "<-" - -type constr_with_marks = - | MApp of constr * morphism_class * constr_with_marks array * direction - | ToReplace - | ToKeep of constr * relation relation_class * direction - -let is_to_replace = function - | ToKeep _ -> false - | ToReplace -> true - | MApp _ -> true - -let get_mark a = - Array.fold_left (||) false (Array.map is_to_replace a) - -let cic_direction_of_direction = - function - Left2Right -> Lazy.force coq_Left2Right - | Right2Left -> Lazy.force coq_Right2Left - -let opposite_direction = - function - Left2Right -> Right2Left - | Right2Left -> Left2Right - -let direction_of_constr_with_marks hole_direction = - function - MApp (_,_,_,dir) -> cic_direction_of_direction dir - | ToReplace -> hole_direction - | ToKeep (_,_,dir) -> cic_direction_of_direction dir - -type argument = - Toapply of constr (* apply the function to the argument *) - | Toexpand of name * types (* beta-expand the function w.r.t. an argument - of this type *) -let beta_expand c args_rev = - let rec to_expand = - function - [] -> [] - | (Toapply _)::tl -> to_expand tl - | (Toexpand (name,s))::tl -> (name,s)::(to_expand tl) in - let rec aux n = - function - [] -> [] - | (Toapply arg)::tl -> arg::(aux n tl) - | (Toexpand _)::tl -> (mkRel n)::(aux (n + 1) tl) - in - compose_lam (to_expand args_rev) - (mkApp (c, Array.of_list (List.rev (aux 1 args_rev)))) - -exception Optimize (* used to fall-back on the tactic for Leibniz equality *) - -let relation_class_that_matches_a_constr caller_name new_goals hypt = - let (heq, hargs) = decompose_app hypt in - let rec get_all_but_last_two = - function - [] - | [_] -> - errorlabstrm caller_name (pr_lconstr hypt ++ - str " is not a registered relation.") - | [_;_] -> [] - | he::tl -> he::(get_all_but_last_two tl) in - let all_aeq_args = get_all_but_last_two hargs in - let rec find_relation l subst = - let aeq = mkApp (heq,(Array.of_list l)) in - try - let rel = find_relation_class aeq in - match rel,new_goals with - Leibniz _,[] -> - assert (subst = []); - raise Optimize (* let's optimize the proof term size *) - | Leibniz (Some _), _ -> - assert (subst = []); - rel - | Leibniz None, _ -> - (* for well-typedness reasons it should have been catched by the - previous guard in the previous iteration. *) - assert false - | Relation rel,_ -> Relation (apply_to_relation (Array.of_list subst) rel) - with Not_found -> - if l = [] then - errorlabstrm caller_name - (pr_lconstr (mkApp (aeq, Array.of_list all_aeq_args)) ++ - str " is not a registered relation.") - else - let last,others = Util.list_sep_last l in - find_relation others (last::subst) - in - find_relation all_aeq_args [] - -(* rel1 is a subrelation of rel2 whenever - forall x1 x2, rel1 x1 x2 -> rel2 x1 x2 - The Coq part of the tactic, however, needs rel1 == rel2. - Hence the third case commented out. - Note: accepting user-defined subrelations seems to be the last - useful generalization that does not go against the original spirit of - the tactic. -*) -let subrelation gl rel1 rel2 = - match rel1,rel2 with - Relation {rel_aeq=rel_aeq1}, Relation {rel_aeq=rel_aeq2} -> - Tacmach.pf_conv_x gl rel_aeq1 rel_aeq2 - | Leibniz (Some t1), Leibniz (Some t2) -> - Tacmach.pf_conv_x gl t1 t2 - | Leibniz None, _ - | _, Leibniz None -> assert false -(* This is the commented out case (see comment above) - | Leibniz (Some t1), Relation {rel_a=t2; rel_refl = Some _} -> - Tacmach.pf_conv_x gl t1 t2 -*) - | _,_ -> false - -(* this function returns the list of new goals opened by a constr_with_marks *) -let rec collect_new_goals = - function - MApp (_,_,a,_) -> List.concat (List.map collect_new_goals (Array.to_list a)) - | ToReplace - | ToKeep (_,Leibniz _,_) - | ToKeep (_,Relation {rel_refl=Some _},_) -> [] - | ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) -> [mkApp(aeq,[|c ; c|])] - -(* two marked_constr are equivalent if they produce the same set of new goals *) -let marked_constr_equiv_or_more_complex to_marked_constr gl c1 c2 = - let glc1 = collect_new_goals (to_marked_constr c1) in - let glc2 = collect_new_goals (to_marked_constr c2) in - List.for_all (fun c -> List.exists (fun c' -> pf_conv_x gl c c') glc1) glc2 - -let pr_new_goals i c = - let glc = collect_new_goals c in - str " " ++ int i ++ str ") side conditions:" ++ - (if glc = [] then str " no side conditions" - else - (pr_fnl () ++ str " " ++ - prlist_with_sep (fun () -> str "\n ") - (fun c -> str " ... |- " ++ pr_lconstr c) glc)) - -(* given a list of constr_with_marks, it returns the list where - constr_with_marks than open more goals than simpler ones in the list - are got rid of *) -let elim_duplicates gl to_marked_constr = - let rec aux = - function - [] -> [] - | he:: tl -> - if List.exists - (marked_constr_equiv_or_more_complex to_marked_constr gl he) tl - then aux tl - else he::aux tl - in - aux - -let filter_superset_of_new_goals gl new_goals l = - List.filter - (fun (_,_,c) -> - List.for_all - (fun g -> List.exists (pf_conv_x gl g) (collect_new_goals c)) new_goals) l - -(* given the array of lists [| l1 ; ... ; ln |] it returns the list of arrays - [ c1 ; ... ; cn ] that is the cartesian product of the sets l1, ..., ln *) -let cartesian_product gl a = - let rec aux = - function - [] -> assert false - | [he] -> List.map (fun e -> [e]) he - | he::tl -> - let tl' = aux tl in - List.flatten - (List.map (function e -> List.map (function l -> e :: l) tl') he) - in - List.map Array.of_list - (aux (List.map (elim_duplicates gl identity) (Array.to_list a))) - -let mark_occur gl ~new_goals t in_c input_relation input_direction = - let rec aux output_relation output_directions in_c = - if eq_constr t in_c then - if List.mem input_direction output_directions - && subrelation gl input_relation output_relation then - [ToReplace] - else [] - else - match kind_of_term in_c with - | App (c,al) -> - let mors_and_cs_and_als = - let mors_and_cs_and_als = - let morphism_table_find c = - try morphism_table_find c with Not_found -> [] in - let rec aux acc = - function - [] -> - let c' = mkApp (c, Array.of_list acc) in - let al' = [||] in - List.map (fun m -> m,c',al') (morphism_table_find c') - | (he::tl) as l -> - let c' = mkApp (c, Array.of_list acc) in - let al' = Array.of_list l in - let acc' = acc @ [he] in - (List.map (fun m -> m,c',al') (morphism_table_find c')) @ - (aux acc' tl) - in - aux [] (Array.to_list al) in - let mors_and_cs_and_als = - List.map - (function (m,c,al) -> - relation_morphism_of_constr_morphism m, c, al) - mors_and_cs_and_als in - let mors_and_cs_and_als = - List.fold_left - (fun l (m,c,al) -> - try (unify_morphism_with_arguments gl (c,al) m t) :: l - with Impossible -> l - ) [] mors_and_cs_and_als - in - List.filter - (fun (mor,_,_) -> subrelation gl mor.output output_relation) - mors_and_cs_and_als - in - (* First we look for well typed morphisms *) - let res_mors = - List.fold_left - (fun res (mor,c,al) -> - let a = - let arguments = Array.of_list mor.args in - let apply_variance_to_direction = - function - None -> [Left2Right;Right2Left] - | Some true -> output_directions - | Some false -> List.map opposite_direction output_directions - in - Util.array_map2 - (fun a (variance,relation) -> - (aux relation (apply_variance_to_direction variance) a) - ) al arguments - in - let a' = cartesian_product gl a in - List.flatten (List.map (fun output_direction -> - (List.map - (function a -> - if not (get_mark a) then - ToKeep (in_c,output_relation,output_direction) - else - MApp (c,ACMorphism mor,a,output_direction)) a')) - output_directions) @ res - ) [] mors_and_cs_and_als in - (* Then we look for well typed functions *) - let res_functions = - (* the tactic works only if the function type is - made of non-dependent products only. However, here we - can cheat a bit by partially instantiating c to match - the requirement when the arguments to be replaced are - bound by non-dependent products only. *) - let typeofc = Tacmach.pf_type_of gl c in - let typ = nf_betaiota typeofc in - let rec find_non_dependent_function env c c_args_rev typ f_args_rev - a_rev - = - function - [] -> - if a_rev = [] then - List.map (fun output_direction -> - ToKeep (in_c,output_relation,output_direction)) - output_directions - else - let a' = - cartesian_product gl (Array.of_list (List.rev a_rev)) - in - List.fold_left - (fun res a -> - if not (get_mark a) then - List.map (fun output_direction -> - (ToKeep (in_c,output_relation,output_direction))) - output_directions @ res - else - let err = - match output_relation with - Leibniz (Some typ') when pf_conv_x gl typ typ' -> - false - | Leibniz None -> assert false - | _ when output_relation = Lazy.force coq_iff_relation - -> false - | _ -> true - in - if err then res - else - let mor = - ACFunction{f_args=List.rev f_args_rev;f_output=typ} in - let func = beta_expand c c_args_rev in - List.map (fun output_direction -> - (MApp (func,mor,a,output_direction))) - output_directions @ res - ) [] a' - | (he::tl) -> - let typnf = Reduction.whd_betadeltaiota env typ in - match kind_of_term typnf with - | Prod (name,s,t) -> - let env' = push_rel (name,None,s) env in - let he = - (aux (Leibniz (Some s)) [Left2Right;Right2Left] he) in - if he = [] then [] - else - let he0 = List.hd he in - begin - match noccurn 1 t, he0 with - _, ToKeep (arg,_,_) -> - (* invariant: if he0 = ToKeep (t,_,_) then every - element in he is = ToKeep (t,_,_) *) - assert - (List.for_all - (function - ToKeep(arg',_,_) when pf_conv_x gl arg arg' -> - true - | _ -> false) he) ; - (* generic product, to keep *) - find_non_dependent_function - env' c ((Toapply arg)::c_args_rev) - (subst1 arg t) f_args_rev a_rev tl - | true, _ -> - (* non-dependent product, to replace *) - find_non_dependent_function - env' c ((Toexpand (name,s))::c_args_rev) - (lift 1 t) (s::f_args_rev) (he::a_rev) tl - | false, _ -> - (* dependent product, to replace *) - (* This limitation is due to the reflexive - implementation and it is hard to lift *) - errorlabstrm "Setoid_replace" - (str "Cannot rewrite in the argument of a " ++ - str "dependent product. If you need this " ++ - str "feature, please report to the author.") - end - | _ -> assert false - in - find_non_dependent_function (Tacmach.pf_env gl) c [] typ [] [] - (Array.to_list al) - in - elim_duplicates gl identity (res_functions @ res_mors) - | Prod (_, c1, c2) -> - if (dependent (mkRel 1) c2) - then - if (occur_term t c2) - then errorlabstrm "Setoid_replace" - (str "Cannot rewrite in the type of a variable bound " ++ - str "in a dependent product.") - else - List.map (fun output_direction -> - ToKeep (in_c,output_relation,output_direction)) - output_directions - else - let typeofc1 = Tacmach.pf_type_of gl c1 in - if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then - (* to avoid this error we should introduce an impl relation - whose first argument is Type instead of Prop. However, - the type of the new impl would be Type -> Prop -> Prop - that is no longer a Relation_Definitions.relation. Thus - the Coq part of the tactic should be heavily modified. *) - errorlabstrm "Setoid_replace" - (str "Rewriting in a product A -> B is possible only when A " ++ - str "is a proposition (i.e. A is of type Prop). The type " ++ - pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++ - str " that is not convertible to Prop.") - else - aux output_relation output_directions - (mkApp ((Lazy.force coq_impl), - [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |])) - | _ -> - if occur_term t in_c then - errorlabstrm "Setoid_replace" - (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++ - str " that is not an applicative context.") - else - List.map (fun output_direction -> - ToKeep (in_c,output_relation,output_direction)) - output_directions - in - let aux2 output_relation output_direction = - List.map - (fun res -> output_relation,output_direction,res) - (aux output_relation [output_direction] in_c) in - let res = - (aux2 (Lazy.force coq_iff_relation) Right2Left) @ - (* [Left2Right] is the case of a prop of signature A ++> iff or B --> iff *) - (aux2 (Lazy.force coq_iff_relation) Left2Right) @ - (aux2 (Lazy.force coq_impl_relation) Right2Left) in - let res = elim_duplicates gl (function (_,_,t) -> t) res in - let res' = filter_superset_of_new_goals gl new_goals res in - match res' with - [] when res = [] -> - errorlabstrm "Setoid_rewrite" - (strbrk "Either the term " ++ pr_lconstr t ++ strbrk " that must be " ++ - strbrk "rewritten occurs in a covariant position or the goal is not" ++ - strbrk " made of morphism applications only. You can replace only " ++ - strbrk "occurrences that are in a contravariant position and such " ++ - strbrk "that the context obtained by abstracting them is made of " ++ - strbrk "morphism applications only.") - | [] -> - errorlabstrm "Setoid_rewrite" - (str "No generated set of side conditions is a superset of those " ++ - str "requested by the user. The generated sets of side conditions " ++ - str "are: " ++ - pr_fnl () ++ - prlist_with_sepi pr_fnl - (fun i (_,_,mc) -> pr_new_goals i mc) res) - | [he] -> he - | he::_ -> - Flags.if_warn msg_warning - (strbrk "The application of the tactic is subject to one of " ++ - strbrk "the following set of side conditions that the user needs " ++ - strbrk "to prove:" ++ - pr_fnl () ++ - prlist_with_sepi pr_fnl - (fun i (_,_,mc) -> pr_new_goals i mc) res' ++ pr_fnl () ++ - strbrk "The first set is randomly chosen. Use the syntax " ++ - strbrk "\"setoid_rewrite ... generate side conditions ...\" to choose " ++ - strbrk "a different set.") ; - he - -let cic_morphism_context_list_of_list hole_relation hole_direction out_direction -= - let check = - function - (None,dir,dir') -> - mkApp ((Lazy.force coq_MSNone), [| dir ; dir' |]) - | (Some true,dir,dir') -> - assert (dir = dir'); - mkApp ((Lazy.force coq_MSCovariant), [| dir |]) - | (Some false,dir,dir') -> - assert (dir <> dir'); - mkApp ((Lazy.force coq_MSContravariant), [| dir |]) in - let rec aux = - function - [] -> assert false - | [(variance,out),(value,direction)] -> - mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class ; out |]), - mkApp ((Lazy.force coq_fcl_singl), - [| hole_relation; hole_direction ; out ; - direction ; out_direction ; - check (variance,direction,out_direction) ; value |]) - | ((variance,out),(value,direction))::tl -> - let outtl, valuetl = aux tl in - mkApp ((Lazy.force coq_cons), - [| Lazy.force coq_Argument_Class ; out ; outtl |]), - mkApp ((Lazy.force coq_fcl_cons), - [| hole_relation ; hole_direction ; out ; outtl ; - direction ; out_direction ; - check (variance,direction,out_direction) ; - value ; valuetl |]) - in aux - -let rec cic_type_nelist_of_list = - function - [] -> assert false - | [value] -> - mkApp ((Lazy.force coq_singl), [| mkType (Termops.new_univ ()) ; value |]) - | value::tl -> - mkApp ((Lazy.force coq_cons), - [| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |]) - -let syntactic_but_representation_of_marked_but hole_relation hole_direction = - let rec aux out (rel_out,precise_out,is_reflexive) = - function - MApp (f, m, args, direction) -> - let direction = cic_direction_of_direction direction in - let morphism_theory, relations = - match m with - ACMorphism { args = args ; morphism_theory = morphism_theory } -> - morphism_theory,args - | ACFunction { f_args = f_args ; f_output = f_output } -> - let mt = - if eq_constr out (cic_relation_class_of_relation_class - (Lazy.force coq_iff_relation)) - then - mkApp ((Lazy.force coq_morphism_theory_of_predicate), - [| cic_type_nelist_of_list f_args; f|]) - else - mkApp ((Lazy.force coq_morphism_theory_of_function), - [| cic_type_nelist_of_list f_args; f_output; f|]) - in - mt,List.map (fun x -> None,Leibniz (Some x)) f_args in - let cic_relations = - List.map - (fun (variance,r) -> - variance, - r, - cic_relation_class_of_relation_class r, - cic_precise_relation_class_of_relation_class r - ) relations in - let cic_args_relations,argst = - cic_morphism_context_list_of_list hole_relation hole_direction direction - (List.map2 - (fun (variance,trel,t,precise_t) v -> - (variance,cic_argument_class_of_argument_class (variance,trel)), - (aux t precise_t v, - direction_of_constr_with_marks hole_direction v) - ) cic_relations (Array.to_list args)) - in - mkApp ((Lazy.force coq_App), - [|hole_relation ; hole_direction ; - cic_args_relations ; out ; direction ; - morphism_theory ; argst|]) - | ToReplace -> - mkApp ((Lazy.force coq_ToReplace), [| hole_relation ; hole_direction |]) - | ToKeep (c,_,direction) -> - let direction = cic_direction_of_direction direction in - if is_reflexive then - mkApp ((Lazy.force coq_ToKeep), - [| hole_relation ; hole_direction ; precise_out ; direction ; c |]) - else - let c_is_proper = - let typ = mkApp (rel_out, [| c ; c |]) in - mkCast (Evarutil.mk_new_meta (),DEFAULTcast, typ) - in - mkApp ((Lazy.force coq_ProperElementToKeep), - [| hole_relation ; hole_direction; precise_out ; - direction; c ; c_is_proper |]) - in aux - -let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h) - prop_direction m -= - let hole_relation = cic_relation_class_of_relation_class hole_relation in - let hyp,hole_direction = h,cic_direction_of_direction direction in - let cic_prop_relation = cic_relation_class_of_relation_class prop_relation in - let precise_prop_relation = - cic_precise_relation_class_of_relation_class prop_relation - in - mkApp ((Lazy.force coq_setoid_rewrite), - [| hole_relation ; hole_direction ; cic_prop_relation ; - prop_direction ; c1 ; c2 ; - syntactic_but_representation_of_marked_but hole_relation hole_direction - cic_prop_relation precise_prop_relation m ; hyp |]) - -let check_evar_map_of_evars_defs evd = - let metas = Evd.meta_list evd in - let check_freemetas_is_empty rebus = - Evd.Metaset.iter - (fun m -> - if Evd.meta_defined evd m then () else - raise (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) - in - List.iter - (fun (_,binding) -> - match binding with - Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) -> - check_freemetas_is_empty rebus freemetas - | Evd.Clval (_,({Evd.rebus=rebus1; Evd.freemetas=freemetas1},_), - {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) -> - check_freemetas_is_empty rebus1 freemetas1 ; - check_freemetas_is_empty rebus2 freemetas2 - ) metas - -(* For a correct meta-aware "rewrite in", we split unification - apart from the actual rewriting (Pierre L, 05/04/06) *) - -(* [unification_rewrite] searchs a match for [c1] in [but] and then - returns the modified objects (in particular [c1] and [c2]) *) - -let rewrite_unif_flags = { - modulo_conv_on_closed_terms = None; - use_metas_eagerly = true; - modulo_delta = empty_transparent_state; -} - -let rewrite2_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; - modulo_delta = empty_transparent_state; -} - -let unification_rewrite c1 c2 cl but gl = - let (env',c1) = - try - (* ~flags:(false,true) to allow to mark occurences that must not be - rewritten simply by replacing them with let-defined definitions - in the context *) - w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd - with - Pretype_errors.PretypeError _ -> - (* ~flags:(true,true) to make Ring work (since it really - exploits conversion) *) - w_unify_to_subterm ~flags:rewrite2_unif_flags - (pf_env gl) (c1,but) cl.evd - in - let cl' = {cl with evd = env' } in - let c2 = Clenv.clenv_nf_meta cl' c2 in - check_evar_map_of_evars_defs env' ; - env',Clenv.clenv_value cl', c1, c2 - -(* no unification is performed in this function. [sigma] is the - substitution obtained from an earlier unification. *) - -let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl = - let but = pf_concl gl in - try - let input_relation = - relation_class_that_matches_a_constr "Setoid_rewrite" - new_goals (Typing.mtype_of (pf_env gl) sigma (snd hyp)) in - let output_relation,output_direction,marked_but = - mark_occur gl ~new_goals c1 but input_relation (fst hyp) in - let cic_output_direction = cic_direction_of_direction output_direction in - let if_output_relation_is_iff gl = - let th = - apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp - cic_output_direction marked_but - in - let new_but = Termops.replace_term c1 c2 but in - let hyp1,hyp2,proj = - match output_direction with - Right2Left -> new_but, but, Lazy.force coq_proj1 - | Left2Right -> but, new_but, Lazy.force coq_proj2 - in - let impl1 = mkProd (Anonymous, hyp2, lift 1 hyp1) in - let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in - let th' = mkApp (proj, [|impl2; impl1; th|]) in - Tactics.refine - (mkApp (th',[|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|])) - gl in - let if_output_relation_is_if gl = - let th = - apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp - cic_output_direction marked_but - in - let new_but = Termops.replace_term c1 c2 but in - Tactics.refine - (mkApp (th, [|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|])) - gl in - if output_relation = (Lazy.force coq_iff_relation) then - if_output_relation_is_iff gl - else - if_output_relation_is_if gl - with - Optimize -> - !general_rewrite (fst hyp = Left2Right) all_occurrences (snd hyp) gl - -let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl = - let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl (pf_concl gl) gl in - relation_rewrite_no_unif c1 c2 (input_direction,cl) ~new_goals sigma gl - -let analyse_hypothesis gl c = - let ctype = pf_type_of gl c in - let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in - let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> - let l,res = split_last_two (y::z) in x::l, res - | _ -> error "The term provided is not an equivalence" in - let others,(c1,c2) = split_last_two args in - eqclause,mkApp (equiv, Array.of_list others),c1,c2 - -let general_s_rewrite lft2rgt occs c ~new_goals gl = - if occs <> all_occurrences then - warning "Rewriting at selected occurrences not supported"; - let eqclause,_,c1,c2 = analyse_hypothesis gl c in - if lft2rgt then - relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl - else - relation_rewrite c2 c1 (Right2Left,eqclause) ~new_goals gl - -let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl = - let hyp = pf_type_of gl (mkVar id) in - (* first, we find a match for c1 in the hyp *) - let (sigma,cl,c1,c2) = unification_rewrite c1 c2 eqclause hyp gl in - (* since we will actually rewrite in the opposite direction, we also need - to replace every occurrence of c2 (resp. c1) in hyp with something that - is convertible but not syntactically equal. To this aim we introduce a - let-in and then we will use the intro tactic to get rid of it. - Quite tricky to do properly since c1 can occur in c2 or vice-versa ! *) - let mangled_new_hyp = - let hyp = lift 2 hyp in - (* first, we backup every occurences of c1 in newly allocated (Rel 1) *) - let hyp = Termops.replace_term (lift 2 c1) (mkRel 1) hyp in - (* then, we factorize every occurences of c2 into (Rel 2) *) - let hyp = Termops.replace_term (lift 2 c2) (mkRel 2) hyp in - (* Now we substitute (Rel 1) (i.e. c1) for c2 *) - let hyp = subst1 (lift 1 c2) hyp in - (* Since subst1 has killed Rel 1 and decreased the other Rels, - Rel 1 is now coding for c2, we can build the let-in factorizing c2 *) - mkLetIn (Anonymous,c2,pf_type_of gl c2,hyp) - in - let new_hyp = Termops.replace_term c1 c2 hyp in - let oppdir = opposite_direction direction in - cut_replacing id new_hyp - (tclTHENLAST - (tclTHEN (change_in_concl None mangled_new_hyp) - (tclTHEN intro - (relation_rewrite_no_unif c2 c1 (oppdir,cl) ~new_goals sigma)))) - gl - -let general_s_rewrite_in id lft2rgt occs c ~new_goals gl = - if occs <> all_occurrences then - warning "Rewriting at selected occurrences not supported"; - let eqclause,_,c1,c2 = analyse_hypothesis gl c in - if lft2rgt then - relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl - else - relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl - - -(* - [general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals ] - common part of [setoid_replace] and [setoid_replace_in] (distinction is done using rewrite_tac). - - Algorith sketch: - 1- find the (setoid) relation [rel] between [c1] and [c2] using [relation] - 2- assert [H:rel c2 c1] - 3- replace [c1] with [c2] using [rewrite_tac] (should be [general_s_rewrite] if we want to replace in the - goal, and [general_s_rewrite_in id] if we want to replace in the hypothesis [id]). Possibly generate - new_goals if asked (cf general_s_rewrite) - 4- if [try_prove_eq_tac_opt] is [Some tac] try to complete [rel c2 c1] using tac and do nothing if - [try_prove_eq_tac_opt] is [None] -*) -let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals gl = - let try_prove_eq_tac = - match try_prove_eq_tac_opt with - | None -> Tacticals.tclIDTAC - | Some tac -> Tacticals.tclTRY (Tacticals.tclCOMPLETE tac ) - in - try - let carrier,args = decompose_app (pf_type_of gl c1) in - let relation = - match relation with - Some rel -> - (try - match find_relation_class rel with - Relation sa -> if not (eq_constr carrier sa.rel_a) then - errorlabstrm "Setoid_rewrite" - (str "the carrier of " ++ pr_lconstr rel ++ - str " does not match the type of " ++ pr_lconstr c1); - sa - | Leibniz _ -> raise Optimize - with - Not_found -> - errorlabstrm "Setoid_rewrite" - (pr_lconstr rel ++ str " is not a registered relation.")) - | None -> - match default_relation_for_carrier (pf_type_of gl c1) with - Relation sa -> sa - | Leibniz _ -> raise Optimize - in - let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in - let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in - let replace dir eq = - tclTHENS (assert_as false None eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac dir all_occurrences (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] - in - tclORELSE - (replace true eq_left_to_right) (replace false eq_right_to_left) gl - with - Optimize -> (* (!replace tac_opt c1 c2) gl *) - let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in - tclTHENS (assert_as false None eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac false all_occurrences (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] gl - -let setoid_replace = general_setoid_replace general_s_rewrite -let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = - general_setoid_replace (general_s_rewrite_in id) tac_opt relation c1 c2 ~new_goals gl - -(* [setoid_]{reflexivity,symmetry,transitivity} tactics *) - -(* let setoid_reflexivity gl = *) -(* try *) -(* let relation_class = *) -(* relation_class_that_matches_a_constr "Setoid_reflexivity" *) -(* [] (pf_concl gl) in *) -(* match relation_class with *) -(* Leibniz _ -> assert false (\* since [] is empty *\) *) -(* | Relation rel -> *) -(* match rel.rel_refl with *) -(* None -> *) -(* errorlabstrm "Setoid_reflexivity" *) -(* (str "The relation " ++ prrelation rel ++ str " is not reflexive.") *) -(* | Some refl -> apply refl gl *) -(* with *) -(* Optimize -> reflexivity_red true gl gl *) - -(* let setoid_symmetry gl = *) -(* try *) -(* let relation_class = *) -(* relation_class_that_matches_a_constr "Setoid_symmetry" *) -(* [] (pf_concl gl) in *) -(* match relation_class with *) -(* Leibniz _ -> assert false (\* since [] is empty *\) *) -(* | Relation rel -> *) -(* match rel.rel_sym with *) -(* None -> *) -(* errorlabstrm "Setoid_symmetry" *) -(* (str "The relation " ++ prrelation rel ++ str " is not symmetric.") *) -(* | Some sym -> apply sym gl *) -(* with *) -(* Optimize -> symmetry_red true gl *) - -(* let setoid_symmetry_in id gl = *) -(* let ctype = pf_type_of gl (mkVar id) in *) -(* let binders,concl = decompose_prod_assum ctype in *) -(* let (equiv, args) = decompose_app concl in *) -(* let rec split_last_two = function *) -(* | [c1;c2] -> [],(c1, c2) *) -(* | x::y::z -> let l,res = split_last_two (y::z) in x::l, res *) -(* | _ -> error "The term provided is not an equivalence" *) -(* in *) -(* let others,(c1,c2) = split_last_two args in *) -(* let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in *) -(* let new_hyp' = mkApp (he, [| c2 ; c1 |]) in *) -(* let new_hyp = it_mkProd_or_LetIn new_hyp' binders in *) -(* tclTHENS (cut new_hyp) *) -(* [ intro_replacing id; *) -(* tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ] *) -(* gl *) - -(* let setoid_transitivity c gl = *) -(* try *) -(* let relation_class = *) -(* relation_class_that_matches_a_constr "Setoid_transitivity" *) -(* [] (pf_concl gl) in *) -(* match relation_class with *) -(* Leibniz _ -> assert false (\* since [] is empty *\) *) -(* | Relation rel -> *) -(* let ctyp = pf_type_of gl c in *) -(* let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in *) -(* match rel'.rel_trans with *) -(* None -> *) -(* errorlabstrm "Setoid_transitivity" *) -(* (str "The relation " ++ prrelation rel ++ str " is not transitive.") *) -(* | Some trans -> *) -(* let transty = nf_betaiota (pf_type_of gl trans) in *) -(* let argsrev, _ = *) -(* Reductionops.splay_prod_n (pf_env gl) Evd.empty 2 transty in *) -(* let binder = *) -(* match List.rev argsrev with *) -(* _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2 *) -(* | _ -> assert false *) -(* in *) -(* apply_with_bindings *) -(* (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl *) -(* with *) -(* Optimize -> transitivity_red true c gl *) -(* ;; *) - diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli deleted file mode 100644 index e1ab9255d..000000000 --- a/tactics/setoid_replace.mli +++ /dev/null @@ -1,85 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -open Term -open Proof_type -open Topconstr -open Names -open Termops - -type relation = - { rel_a: constr ; - rel_aeq: constr; - rel_refl: constr option; - rel_sym: constr option; - rel_trans : constr option; - rel_quantifiers_no: int (* it helps unification *); - rel_X_relation_class: constr; - rel_Xreflexive_relation_class: constr - } - -type 'a relation_class = - Relation of 'a (* the [rel_aeq] of the relation or the relation*) - | Leibniz of constr option (* the [carrier] (if [eq] is partially instantiated)*) - -type 'a morphism = - { args : (bool option * 'a relation_class) list; - output : 'a relation_class; - lem : constr; - morphism_theory : constr - } - -type morphism_signature = (bool option * constr_expr) list * constr_expr - -val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds - -val register_replace : (tactic option -> constr -> constr -> tactic) -> unit -val register_general_rewrite : (bool -> occurrences -> constr -> tactic) -> unit - -val print_setoids : unit -> unit - -val equiv_list : unit -> constr list -val default_relation_for_carrier : - ?filter:(relation -> bool) -> types -> relation relation_class -(* [default_morphism] raises [Not_found] *) -val default_morphism : - ?filter:(constr morphism -> bool) -> constr -> relation morphism - -val setoid_replace : - tactic option -> constr option -> constr -> constr -> new_goals:constr list -> tactic -val setoid_replace_in : - tactic option -> - identifier -> constr option -> constr -> constr -> new_goals:constr list -> - tactic - -val general_s_rewrite : - bool -> occurrences -> constr -> new_goals:constr list -> tactic -val general_s_rewrite_in : - identifier -> bool -> occurrences -> constr -> new_goals:constr list -> tactic - -(* val setoid_reflexivity : tactic *) -(* val setoid_symmetry : tactic *) -(* val setoid_symmetry_in : identifier -> tactic *) -(* val setoid_transitivity : constr -> tactic *) - -val add_relation : - Names.identifier -> constr_expr -> constr_expr -> constr_expr option -> - constr_expr option -> constr_expr option -> unit - -val add_setoid : - Names.identifier -> constr_expr -> constr_expr -> constr_expr -> unit - -val new_named_morphism : - Names.identifier -> constr_expr -> morphism_signature option -> unit - -val relation_table_find : constr -> relation -val relation_table_mem : constr -> bool - -val prrelation : relation -> Pp.std_ppcmds diff --git a/theories/Setoids/Setoid_Prop.v b/theories/Setoids/Setoid_Prop.v deleted file mode 100644 index 9c0b4b2b6..000000000 --- a/theories/Setoids/Setoid_Prop.v +++ /dev/null @@ -1,79 +0,0 @@ - -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$: i*) - -Require Import Setoid_tac. - -(** * A few examples on [iff] *) - -(** [iff] as a relation *) - -Add Relation Prop iff - reflexivity proved by iff_refl - symmetry proved by iff_sym - transitivity proved by iff_trans -as iff_relation. - -(** [impl] as a relation *) - -Theorem impl_trans: transitive _ impl. -Proof. - hnf; unfold impl; tauto. -Qed. - -Add Relation Prop impl - reflexivity proved by impl_refl - transitivity proved by impl_trans -as impl_relation. - -(** [impl] is a morphism *) - -Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism. -Proof. - unfold impl; tauto. -Qed. - -(** [and] is a morphism *) - -Add Morphism and with signature iff ==> iff ==> iff as And_Morphism. - tauto. -Qed. - -(** [or] is a morphism *) - -Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism. -Proof. - tauto. -Qed. - -(** [not] is a morphism *) - -Add Morphism not with signature iff ==> iff as Not_Morphism. -Proof. - tauto. -Qed. - -(** The same examples on [impl] *) - -Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2. -Proof. - unfold impl; tauto. -Qed. - -Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2. -Proof. - unfold impl; tauto. -Qed. - -Add Morphism not with signature impl --> impl as Not_Morphism2. -Proof. - unfold impl; tauto. -Qed. - diff --git a/theories/Setoids/Setoid_tac.v b/theories/Setoids/Setoid_tac.v deleted file mode 100644 index 664316805..000000000 --- a/theories/Setoids/Setoid_tac.v +++ /dev/null @@ -1,595 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -Require Export Relation_Definitions. - -Set Implicit Arguments. - -(** * Definitions of [Relation_Class] and n-ary [Morphism_Theory] *) - -(* X will be used to distinguish covariant arguments whose type is an *) -(* Asymmetric* relation from contravariant arguments of the same type *) -Inductive X_Relation_Class (X: Type) : Type := - SymmetricReflexive : - forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> X_Relation_Class X - | AsymmetricReflexive : X -> forall A Aeq, reflexive A Aeq -> X_Relation_Class X - | SymmetricAreflexive : forall A Aeq, symmetric A Aeq -> X_Relation_Class X - | AsymmetricAreflexive : X -> forall A (Aeq : relation A), X_Relation_Class X - | Leibniz : Type -> X_Relation_Class X. - -Inductive variance : Set := - Covariant - | Contravariant. - -Definition Argument_Class := X_Relation_Class variance. -Definition Relation_Class := X_Relation_Class unit. - -Inductive Reflexive_Relation_Class : Type := - RSymmetric : - forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> Reflexive_Relation_Class - | RAsymmetric : - forall A Aeq, reflexive A Aeq -> Reflexive_Relation_Class - | RLeibniz : Type -> Reflexive_Relation_Class. - -Inductive Areflexive_Relation_Class : Type := - | ASymmetric : forall A Aeq, symmetric A Aeq -> Areflexive_Relation_Class - | AAsymmetric : forall A (Aeq : relation A), Areflexive_Relation_Class. - -Implicit Type Hole Out: Relation_Class. - -Definition relation_class_of_argument_class : Argument_Class -> Relation_Class. - destruct 1. - exact (SymmetricReflexive _ s r). - exact (AsymmetricReflexive tt r). - exact (SymmetricAreflexive _ s). - exact (AsymmetricAreflexive tt Aeq). - exact (Leibniz _ T). -Defined. - -Definition carrier_of_relation_class : forall X, X_Relation_Class X -> Type. - destruct 1. - exact A. - exact A. - exact A. - exact A. - exact T. -Defined. - -Definition relation_of_relation_class : - forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R -> Prop. - destruct R. - exact Aeq. - exact Aeq. - exact Aeq. - exact Aeq. - exact (@eq T). -Defined. - -Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class : - forall R, - carrier_of_relation_class (relation_class_of_argument_class R) = - carrier_of_relation_class R. - destruct R; reflexivity. -Defined. - -Inductive nelistT (A : Type) : Type := - singl : A -> nelistT A - | necons : A -> nelistT A -> nelistT A. - -Definition Arguments := nelistT Argument_Class. - -Implicit Type In: Arguments. - -Definition function_type_of_morphism_signature : - Arguments -> Relation_Class -> Type. - intros In Out. - induction In. - exact (carrier_of_relation_class a -> carrier_of_relation_class Out). - exact (carrier_of_relation_class a -> IHIn). -Defined. - -Definition make_compatibility_goal_aux: - forall In Out - (f g: function_type_of_morphism_signature In Out), Prop. - intros; induction In; simpl in f, g. - induction a; simpl in f, g. - exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). - destruct x. - exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). - exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)). - exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). - destruct x. - exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1) (g x2)). - exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f x1) (g x2)). - exact (forall x, relation_of_relation_class Out (f x) (g x)). - induction a; simpl in f, g. - exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). - destruct x. - exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). - exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)). - exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). - destruct x. - exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)). - exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)). - exact (forall x, IHIn (f x) (g x)). -Defined. - -Definition make_compatibility_goal := - (fun In Out f => make_compatibility_goal_aux In Out f f). - -Record Morphism_Theory In Out : Type := - { Function : function_type_of_morphism_signature In Out; - Compat : make_compatibility_goal In Out Function }. - - -(** The [iff] relation class *) - -Definition Iff_Relation_Class : Relation_Class. - eapply (@SymmetricReflexive unit _ iff). - exact iff_sym. - exact iff_refl. -Defined. - -(** The [impl] relation class *) - -Definition impl (A B: Prop) := A -> B. - -Theorem impl_refl: reflexive _ impl. -Proof. - hnf; unfold impl; tauto. -Qed. - -Definition Impl_Relation_Class : Relation_Class. - eapply (@AsymmetricReflexive unit tt _ impl). - exact impl_refl. -Defined. - -(** Every function is a morphism from Leibniz+ to Leibniz *) - -Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments. - induction 1. - exact (singl (Leibniz _ a)). - exact (necons (Leibniz _ a) IHX). -Defined. - -Definition morphism_theory_of_function : - forall (In: nelistT Type) (Out: Type), - let In' := list_of_Leibniz_of_list_of_types In in - let Out' := Leibniz _ Out in - function_type_of_morphism_signature In' Out' -> - Morphism_Theory In' Out'. - intros. - exists X. - induction In; unfold make_compatibility_goal; simpl. - reflexivity. - intro; apply (IHIn (X x)). -Defined. - -(** Every predicate is a morphism from Leibniz+ to Iff_Relation_Class *) - -Definition morphism_theory_of_predicate : - forall (In: nelistT Type), - let In' := list_of_Leibniz_of_list_of_types In in - function_type_of_morphism_signature In' Iff_Relation_Class -> - Morphism_Theory In' Iff_Relation_Class. - intros. - exists X. - induction In; unfold make_compatibility_goal; simpl. - intro; apply iff_refl. - intro; apply (IHIn (X x)). -Defined. - -(** * Utility functions to prove that every transitive relation is a morphism *) - -Definition equality_morphism_of_symmetric_areflexive_transitive_relation: - forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq), - let ASetoidClass := SymmetricAreflexive _ sym in - (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; split; eauto. -Defined. - -Definition equality_morphism_of_symmetric_reflexive_transitive_relation: - forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq) - (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in - (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; split; eauto. -Defined. - -Definition equality_morphism_of_asymmetric_areflexive_transitive_relation: - forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq), - let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in - let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in - (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; unfold impl; eauto. -Defined. - -Definition equality_morphism_of_asymmetric_reflexive_transitive_relation: - forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(trans: transitive _ Aeq), - let ASetoidClass1 := AsymmetricReflexive Contravariant refl in - let ASetoidClass2 := AsymmetricReflexive Covariant refl in - (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class). - intros. - exists Aeq. - unfold make_compatibility_goal; simpl; unfold impl; eauto. -Defined. - -(** * The CIC part of the reflexive tactic ([setoid_rewrite]) *) - -Inductive rewrite_direction : Type := - | Left2Right - | Right2Left. - -Implicit Type dir: rewrite_direction. - -Definition variance_of_argument_class : Argument_Class -> option variance. - destruct 1. - exact None. - exact (Some v). - exact None. - exact (Some v). - exact None. -Defined. - -Definition opposite_direction := - fun dir => - match dir with - | Left2Right => Right2Left - | Right2Left => Left2Right - end. - -Lemma opposite_direction_idempotent: - forall dir, (opposite_direction (opposite_direction dir)) = dir. -Proof. - destruct dir; reflexivity. -Qed. - -Inductive check_if_variance_is_respected : - option variance -> rewrite_direction -> rewrite_direction -> Prop := - | MSNone : forall dir dir', check_if_variance_is_respected None dir dir' - | MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant) dir dir - | MSContravariant : - forall dir, - check_if_variance_is_respected (Some Contravariant) dir (opposite_direction dir). - -Definition relation_class_of_reflexive_relation_class: - Reflexive_Relation_Class -> Relation_Class. - induction 1. - exact (SymmetricReflexive _ s r). - exact (AsymmetricReflexive tt r). - exact (Leibniz _ T). -Defined. - -Definition relation_class_of_areflexive_relation_class: - Areflexive_Relation_Class -> Relation_Class. - induction 1. - exact (SymmetricAreflexive _ s). - exact (AsymmetricAreflexive tt Aeq). -Defined. - -Definition carrier_of_reflexive_relation_class := - fun R => carrier_of_relation_class (relation_class_of_reflexive_relation_class R). - -Definition carrier_of_areflexive_relation_class := - fun R => carrier_of_relation_class (relation_class_of_areflexive_relation_class R). - -Definition relation_of_areflexive_relation_class := - fun R => relation_of_relation_class (relation_class_of_areflexive_relation_class R). - -Inductive Morphism_Context Hole dir : Relation_Class -> rewrite_direction -> Type := - | App : - forall In Out dir', - Morphism_Theory In Out -> Morphism_Context_List Hole dir dir' In -> - Morphism_Context Hole dir Out dir' - | ToReplace : Morphism_Context Hole dir Hole dir - | ToKeep : - forall S dir', - carrier_of_reflexive_relation_class S -> - Morphism_Context Hole dir (relation_class_of_reflexive_relation_class S) dir' - | ProperElementToKeep : - forall S dir' (x: carrier_of_areflexive_relation_class S), - relation_of_areflexive_relation_class S x x -> - Morphism_Context Hole dir (relation_class_of_areflexive_relation_class S) dir' -with Morphism_Context_List Hole dir : - rewrite_direction -> Arguments -> Type -:= - fcl_singl : - forall S dir' dir'', - check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' -> - Morphism_Context Hole dir (relation_class_of_argument_class S) dir' -> - Morphism_Context_List Hole dir dir'' (singl S) - | fcl_cons : - forall S L dir' dir'', - check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' -> - Morphism_Context Hole dir (relation_class_of_argument_class S) dir' -> - Morphism_Context_List Hole dir dir'' L -> - Morphism_Context_List Hole dir dir'' (necons S L). - -Scheme Morphism_Context_rect2 := Induction for Morphism_Context Sort Type -with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type. - -Definition product_of_arguments : Arguments -> Type. - induction 1. - exact (carrier_of_relation_class a). - exact (prod (carrier_of_relation_class a) IHX). -Defined. - -Definition get_rewrite_direction: rewrite_direction -> Argument_Class -> rewrite_direction. - intros dir R. - destruct (variance_of_argument_class R). - destruct v. - exact dir. (* covariant *) - exact (opposite_direction dir). (* contravariant *) - exact dir. (* symmetric relation *) -Defined. - -Definition directed_relation_of_relation_class: - forall dir (R: Relation_Class), - carrier_of_relation_class R -> carrier_of_relation_class R -> Prop. - destruct 1. - exact (@relation_of_relation_class unit). - intros; exact (relation_of_relation_class _ X0 X). -Defined. - -Definition directed_relation_of_argument_class: - forall dir (R: Argument_Class), - carrier_of_relation_class R -> carrier_of_relation_class R -> Prop. - intros dir R. - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class R). - exact (directed_relation_of_relation_class dir (relation_class_of_argument_class R)). -Defined. - - -Definition relation_of_product_of_arguments: - forall dir In, - product_of_arguments In -> product_of_arguments In -> Prop. - induction In. - simpl. - exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a). - - simpl; intros. - destruct X; destruct X0. - apply and. - exact - (directed_relation_of_argument_class (get_rewrite_direction dir a) a c c0). - exact (IHIn p p0). -Defined. - -Definition apply_morphism: - forall In Out (m: function_type_of_morphism_signature In Out) - (args: product_of_arguments In), carrier_of_relation_class Out. - intros. - induction In. - exact (m args). - simpl in m, args. - destruct args. - exact (IHIn (m c) p). -Defined. - -Theorem apply_morphism_compatibility_Right2Left: - forall In Out (m1 m2: function_type_of_morphism_signature In Out) - (args1 args2: product_of_arguments In), - make_compatibility_goal_aux _ _ m1 m2 -> - relation_of_product_of_arguments Right2Left _ args1 args2 -> - directed_relation_of_relation_class Right2Left _ - (apply_morphism _ _ m2 args1) - (apply_morphism _ _ m1 args2). - induction In; intros. - simpl in m1, m2, args1, args2, H0 |- *. - destruct a; simpl in H; hnf in H0. - apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - rewrite H0; apply H; exact H0. - - simpl in m1, m2, args1, args2, H0 |- *. - destruct args1; destruct args2; simpl. - destruct H0. - simpl in H. - destruct a; simpl in H. - apply IHIn. - apply H; exact H0. - exact H1. - destruct v. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - apply H; exact H0. - exact H1. - destruct v. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - apply H; exact H0. - exact H1. - rewrite H0; apply IHIn. - apply H. - exact H1. -Qed. - -Theorem apply_morphism_compatibility_Left2Right: - forall In Out (m1 m2: function_type_of_morphism_signature In Out) - (args1 args2: product_of_arguments In), - make_compatibility_goal_aux _ _ m1 m2 -> - relation_of_product_of_arguments Left2Right _ args1 args2 -> - directed_relation_of_relation_class Left2Right _ - (apply_morphism _ _ m1 args1) - (apply_morphism _ _ m2 args2). -Proof. - induction In; intros. - simpl in m1, m2, args1, args2, H0 |- *. - destruct a; simpl in H; hnf in H0. - apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - apply H; exact H0. - destruct v; simpl in H0; apply H; exact H0. - rewrite H0; apply H; exact H0. - - simpl in m1, m2, args1, args2, H0 |- *. - destruct args1; destruct args2; simpl. - destruct H0. - simpl in H. - destruct a; simpl in H. - apply IHIn. - apply H; exact H0. - exact H1. - destruct v. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - apply H; exact H0. - exact H1. - apply IHIn. - destruct v; simpl in H, H0; apply H; exact H0. - exact H1. - rewrite H0; apply IHIn. - apply H. - exact H1. -Qed. - -Definition interp : - forall Hole dir Out dir', carrier_of_relation_class Hole -> - Morphism_Context Hole dir Out dir' -> carrier_of_relation_class Out. - intros Hole dir Out dir' H t. - elim t using - (@Morphism_Context_rect2 Hole dir (fun S _ _ => carrier_of_relation_class S) - (fun _ L fcl => product_of_arguments L)); - intros. - exact (apply_morphism _ _ (Function m) X). - exact H. - exact c. - exact x. - simpl; - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - split. - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - exact X0. -Defined. - -(* CSC: interp and interp_relation_class_list should be mutually defined, since - the proof term of each one contains the proof term of the other one. However - I cannot do that interactively (I should write the Fix by hand) *) -Definition interp_relation_class_list : - forall Hole dir dir' (L: Arguments), carrier_of_relation_class Hole -> - Morphism_Context_List Hole dir dir' L -> product_of_arguments L. - intros Hole dir dir' L H t. - elim t using - (@Morphism_Context_List_rect2 Hole dir (fun S _ _ => carrier_of_relation_class S) - (fun _ L fcl => product_of_arguments L)); - intros. - exact (apply_morphism _ _ (Function m) X). - exact H. - exact c. - exact x. - simpl; - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - split. - rewrite <- - (about_carrier_of_relation_class_and_relation_class_of_argument_class S); - exact X. - exact X0. -Defined. - -Theorem setoid_rewrite: - forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole) - (E: Morphism_Context Hole dir Out dir'), - (directed_relation_of_relation_class dir Hole E1 E2) -> - (directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2 E)). -Proof. - intros. - elim E using - (@Morphism_Context_rect2 Hole dir - (fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1 E) (interp E2 E)) - (fun dir'' L fcl => - relation_of_product_of_arguments dir'' _ - (interp_relation_class_list E1 fcl) - (interp_relation_class_list E2 fcl))); intros. - change (directed_relation_of_relation_class dir'0 Out0 - (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0)) - (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))). - destruct dir'0. - apply apply_morphism_compatibility_Left2Right. - exact (Compat m). - exact H0. - apply apply_morphism_compatibility_Right2Left. - exact (Compat m). - exact H0. - - exact H. - - unfold interp, Morphism_Context_rect2. - (* CSC: reflexivity used here *) - destruct S; destruct dir'0; simpl; (apply r || reflexivity). - - destruct dir'0; exact r. - - destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *; - unfold get_rewrite_direction; simpl. - destruct dir'0; destruct dir''; - (exact H0 || - unfold directed_relation_of_argument_class; simpl; apply s; exact H0). - (* the following mess with generalize/clear/intros is to help Coq resolving *) - (* second order unification problems. *) - generalize m c H0; clear H0 m c; inversion c; - generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros; - (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3). - destruct dir'0; destruct dir''; - (exact H0 || - unfold directed_relation_of_argument_class; simpl; apply s; exact H0). - (* the following mess with generalize/clear/intros is to help Coq resolving *) - (* second order unification problems. *) - generalize m c H0; clear H0 m c; inversion c; - generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros; - (exact H3 || rewrite (opposite_direction_idempotent dir'0); apply H3). - destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0). - - change - (directed_relation_of_argument_class (get_rewrite_direction dir'' S) S - (eq_rect _ (fun T : Type => T) (interp E1 m) _ - (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) - (eq_rect _ (fun T : Type => T) (interp E2 m) _ - (about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\ - relation_of_product_of_arguments dir'' _ - (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)). - split. - clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction; simpl. - destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0). - inversion c. - rewrite <- H3; exact H0. - rewrite (opposite_direction_idempotent dir'0); exact H0. - destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0). - inversion c. - rewrite <- H3; exact H0. - rewrite (opposite_direction_idempotent dir'0); exact H0. - destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0). - exact H1. - Qed. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 37e9cf22a..ab3df8c0c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1092,7 +1092,6 @@ let vernac_print = function | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s | PrintHintDb -> Auto.print_searchtable () - | PrintSetoids -> Setoid_replace.print_setoids() | PrintScopes -> pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr)) | PrintScope s -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 9412a5981..aa6a48d66 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -60,7 +60,6 @@ type printable = | PrintHintDbName of string | PrintRewriteHintDbName of string | PrintHintDb - | PrintSetoids | PrintScopes | PrintScope of string | PrintVisibility of string option |