diff options
| -rw-r--r-- | tactics/setoid_replace.ml | 1240 | ||||
| -rw-r--r-- | tactics/setoid_replace.mli | 3 | ||||
| -rw-r--r-- | theories/Setoids/Setoid.v | 372 |
3 files changed, 941 insertions, 674 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 4a44e72d2..a5f5f742d 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -33,21 +33,22 @@ open Constrintern let replace = ref (fun _ _ -> assert false) let register_replace f = replace := f -type setoid = - { set_a : constr; - set_aeq : constr; - set_th : constr - } - -type 'a setoid_class = - ACSetoid of 'a (*the equivalence relation of the setoid or the setoid*) - | ACLeibniz of constr (*the carrier of the setoid*) +type reflexive_relation = + { refl_a: constr ; + refl_aeq: constr; + refl_refl: constr; + refl_sym: constr option + } + +type 'a relation_class = + ACReflexive of 'a (* the relation of the reflexive_relation + or the reflexive_relation*) + | ACLeibniz of constr (* the carrier *) type 'a morphism = - { lem : constr; - args : 'a setoid_class list; - output : 'a setoid_class; - lem2 : constr option + { args : 'a relation_class list; + output : 'a relation_class; + lem : constr; } type funct = @@ -56,25 +57,27 @@ type funct = } type morphism_class = - ACMorphism of setoid morphism + ACMorphism of reflexive_relation morphism | ACFunction of funct -let subst_mps_in_setoid_class subst = +let subst_mps_in_relation_class subst = function - ACSetoid t -> ACSetoid (subst_mps subst t) + ACReflexive t -> ACReflexive (subst_mps subst t) | ACLeibniz t -> ACLeibniz (subst_mps subst t) -let constr_setoid_class_of_setoid_setoid_class = +let constr_relation_class_of_relation_relation_class = function - ACSetoid setoid -> ACSetoid setoid.set_aeq + ACReflexive relation -> ACReflexive relation.refl_aeq | ACLeibniz t -> ACLeibniz 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 global_constant dir s =Coqlib.gen_constant "Setoid_replace" ("Init"::dir) s +let init_constant dir s = Coqlib.gen_constant "Setoid_replace" ("Init"::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 (init_constant dir s)) let current_constant id = try @@ -82,134 +85,196 @@ let current_constant id = with Not_found -> anomaly ("Setoid: cannot find " ^ (string_of_id id)) -(* Setoid_theory *) +(* From Setoid.v *) +let coq_is_reflexive = lazy(constant ["Setoid"] "is_reflexive") + +let coq_Relation_Class = lazy(constant ["Setoid"] "Relation_Class") let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory") +let coq_Morphism_Theory = lazy(constant ["Setoid"] "Morphism_Theory") +let coq_Build_Morphism_Theory= lazy(constant ["Setoid"] "Build_Morphism_Theory") + +let coq_Reflexive = lazy(constant ["Setoid"] "Reflexive") +let coq_Leibniz = lazy(constant ["Setoid"] "Leibniz") 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_fleche = lazy(constant ["Setoid"] "fleche") +let coq_singl = lazy(constant ["Setoid"] "singl") +let coq_cons = lazy(constant ["Setoid"] "cons") -(* Coq constants *) +let coq_equality_morphism_of_setoid_theory = + lazy(constant ["Setoid"] "equality_morphism_of_setoid_theory") +let coq_make_compatibility_goal = + lazy(constant ["Setoid"] "make_compatibility_goal") +let coq_make_compatibility_goal_ref = + lazy(reference ["Setoid"] "make_compatibility_goal") +let coq_make_compatibility_goal_aux_ref = + lazy(reference ["Setoid"] "make_compatibility_goal_aux") -let coqiff = lazy(global_constant ["Logic"] "iff") +let coq_App = lazy(constant ["Setoid"] "App") +let coq_Toreplace = lazy(constant ["Setoid"] "Toreplace") +let coq_Tokeep = lazy(constant ["Setoid"] "Tokeep") +let coq_Imp = lazy(constant ["Setoid"] "Imp") +let coq_fcl_singl = lazy(constant ["Setoid"] "fcl_singl") +let coq_fcl_cons = lazy(constant ["Setoid"] "fcl_cons") -let coqeq = lazy(global_constant ["Logic"] "eq") +let coq_setoid_rewrite = lazy(constant ["Setoid"] "setoid_rewrite") +let coq_proj2 = lazy(init_constant ["Logic"] "proj2") -let coqconj = lazy(global_constant ["Logic"] "conj") -let coqand = lazy(global_constant ["Logic"] "and") -let coqproj1 = lazy(global_constant ["Logic"] "proj1") -let coqproj2 = lazy(global_constant ["Logic"] "proj2") +let coq_morphism_theory_of_function = + lazy(constant ["Setoid"] "morphism_theory_of_function") +let coq_morphism_theory_of_predicate = + lazy(constant ["Setoid"] "morphism_theory_of_predicate") +let coq_relation_of_relation_class = + lazy(eval_reference ["Setoid"] "relation_of_relation_class") +let coq_interp = lazy(eval_reference ["Setoid"] "interp") +let coq_Morphism_Context_rect2 = + lazy(eval_reference ["Setoid"] "Morphism_Context_rect2") +let coq_iff = lazy(eval_init_reference ["Logic"] "iff") -(************************* Table of declared setoids **********************) +let coq_prop_relation = + lazy ( + ACReflexive { + refl_a = mkProp ; + refl_aeq = init_constant ["Logic"] "iff" ; + refl_refl = init_constant ["Logic"] "iff_refl"; + refl_sym = Some (init_constant ["Logic"] "iff_sym") + }) -(* Setoids are stored in a table which is synchronised with the Reset mechanism. *) +(************************* Table of declared relations **********************) + -let setoid_table = ref Gmap.empty +(* Relations are stored in a table which is synchronised with the Reset mechanism. *) -let setoid_table_add (s,th) = setoid_table := Gmap.add s th !setoid_table -let setoid_table_find s = Gmap.find s !setoid_table -let setoid_table_mem s = Gmap.mem s !setoid_table +let relation_table = ref Gmap.empty -let prsetoid s = - str "(" ++ prterm s.set_a ++ str "," ++ prterm s.set_aeq ++ str ")" +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 prsetoid_class = +let prrelation s = + str "(" ++ prterm s.refl_a ++ str "," ++ prterm s.refl_aeq ++ str ")" + +let prrelation_class = function - ACSetoid eq -> - (try prsetoid (setoid_table_find eq) + ACReflexive eq -> + (try prrelation (relation_table_find eq) with Not_found -> + (*CSC: still "setoid" in the error message *) str "[[ Error: setoid on equality " ++ prterm eq ++ str " not found! ]]") | ACLeibniz ty -> prterm ty let prmorphism k m = prterm k ++ str ": " ++ - prlist_with_sep (fun () -> str " -> ") prsetoid_class m.args ++ - str " -> " ++ prsetoid_class m.output + prlist_with_sep (fun () -> str " -> ") prrelation_class m.args ++ + str " -> " ++ prrelation_class m.output -(* A function that gives back the only setoid on a given carrier *) +(* 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_setoid_for_carrier a = - let rng = Gmap.rng !setoid_table in - match List.filter (fun {set_a=set_a} -> set_a = a) rng with +let default_relation_for_carrier a = + let rng = Gmap.rng !relation_table in + match List.filter (fun {refl_a=refl_a} -> refl_a = a) rng with [] -> ACLeibniz a - | setoid::tl -> + | relation::tl -> if tl <> [] then msg_warning + (*CSC: still "setoid" in the error message *) (str "There are several setoids whose carrier is " ++ prterm a ++ - str ". The setoid " ++ prsetoid setoid ++ + str ". The setoid " ++ prrelation relation ++ str " is randomly chosen.") ; - ACSetoid setoid + ACReflexive relation -let setoid_morphism_of_constr_morphism = - let setoid_setoid_class_of_constr_setoid_class = +let relation_morphism_of_constr_morphism = + let relation_relation_class_of_constr_relation_class = function ACLeibniz t -> ACLeibniz t - | ACSetoid aeq -> - ACSetoid (try setoid_table_find aeq with Not_found -> assert false) + | ACReflexive aeq -> + ACReflexive (try relation_table_find aeq with Not_found -> assert false) in function mor -> - let args' = List.map setoid_setoid_class_of_constr_setoid_class mor.args in - let output' = setoid_setoid_class_of_constr_setoid_class mor.output in + let args' = List.map relation_relation_class_of_constr_relation_class mor.args in + let output' = relation_relation_class_of_constr_relation_class mor.output in {mor with args=args' ; output=output'} -let subst_setoid subst setoid = - let set_a' = subst_mps subst setoid.set_a in - let set_aeq' = subst_mps subst setoid.set_aeq in - let set_th' = subst_mps subst setoid.set_th in - if set_a' == setoid.set_a - && set_aeq' == setoid.set_aeq - && set_th' == setoid.set_th +let subst_relation subst relation = + let refl_a' = subst_mps subst relation.refl_a in + let refl_aeq' = subst_mps subst relation.refl_aeq in + let refl_refl' = subst_mps subst relation.refl_refl in + let refl_sym' = option_app (subst_mps subst) relation.refl_sym in + if refl_a' == relation.refl_a + && refl_aeq' == relation.refl_aeq + && refl_refl' == relation.refl_refl + && refl_sym' == relation.refl_sym then - setoid + relation else - { set_a = set_a' ; - set_aeq = set_aeq' ; - set_th = set_th' ; + { refl_a = refl_a' ; + refl_aeq = refl_aeq' ; + refl_refl = refl_refl' ; + refl_sym = refl_sym' } -let equiv_list () = List.map (fun x -> x.set_aeq) (Gmap.rng !setoid_table) +let equiv_list () = List.map (fun x -> x.refl_aeq) (Gmap.rng !relation_table) let _ = - Summary.declare_summary "setoid-table" - { Summary.freeze_function = (fun () -> !setoid_table); - Summary.unfreeze_function = (fun t -> setoid_table := t); - Summary.init_function = (fun () -> setoid_table := Gmap .empty); + 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 = true; Summary.survive_section = false } -(* Declare a new type of object in the environment : "setoid-theory". *) +(* Declare a new type of object in the environment : "relation-theory". *) -let (setoid_to_obj, obj_to_setoid)= +let (relation_to_obj, obj_to_relation)= let cache_set (_,(s, th)) = - if setoid_table_mem s then - begin - let old_setoid = setoid_table_find s in - msg_warning - (str "The setoid " ++ prsetoid th ++ str " is redeclared. " ++ - str "The new declaration justified by " ++ - prterm th.set_th ++ str " replaces the old declaration justified by "++ - prterm old_setoid.set_th ++ str ".") - end ; - setoid_table_add (s,th) + let th' = + if relation_table_mem s then + begin + let old_relation = relation_table_find s in + let th' = + {th with refl_sym = + match th.refl_sym with + None -> old_relation.refl_sym + | Some t -> Some t} in + (*CSC: still "setoid" in the error message *) + msg_warning + (str "The setoid " ++ prrelation th' ++ str " is redeclared. " ++ + str "The new declaration (reflevity proved by " ++ + prterm th'.refl_refl ++ + (match th'.refl_sym with + None -> str "" + | Some t -> str " and symmetry proved by " ++ prterm t) ++ + str ") replaces the old declaration (reflexivity proved by "++ + prterm old_relation.refl_refl ++ + (match old_relation.refl_sym with + None -> str "" + | Some t -> str " and symmetry proved by " ++ prterm t) ++ + 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_setoid subst th in + let th' = subst_relation subst th in if s' == s && th' == th then obj else - (s',th') + (s',th') and export_set x = Some x in - declare_object {(default_object "setoid-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} + 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 ********************) @@ -233,47 +298,25 @@ let morphism_table_add (m,c) = msg_warning (str "The morphism " ++ prmorphism m old_morph ++ str " is redeclared. " ++ str "The new declaration whose compatibility is granted by " ++ - prterm c.lem ++ - (match c.lem2 with None -> str "" | Some t-> str " and " ++ prterm t) - ++ str " replaces the old declaration whose" ++ + prterm c.lem ++ str " replaces the old declaration whose" ++ str " compatibility was granted by " ++ - prterm old_morph.lem ++ - (match old_morph.lem2 with - None -> str "" - | Some t-> str " and "++ prterm t) ++ str ".") + prterm old_morph.lem ++ str ".") with Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table -let find_morphism_fleche () = - let fleche_constr = (Lazy.force coq_fleche) in - try - let mor = - List.find - (function {args=args; output=output} as morphism -> - output = ACSetoid (Lazy.force coqiff) && - List.for_all (function c -> c = ACSetoid (Lazy.force coqiff)) args) - (morphism_table_find fleche_constr) - in - setoid_morphism_of_constr_morphism mor - with - Not_found -> assert false - let subst_morph subst morph = let lem' = subst_mps subst morph.lem in - let args' = list_smartmap (subst_mps_in_setoid_class subst) morph.args in - let output' = subst_mps_in_setoid_class subst morph.output in - let lem2' = option_smartmap (subst_mps subst) morph.lem2 in + let args' = list_smartmap (subst_mps_in_relation_class subst) morph.args in + let output' = subst_mps_in_relation_class subst morph.output in if lem' == morph.lem && args' == morph.args && output' == morph.output - && lem2' == morph.lem2 then morph else - { lem = lem' ; - args = args' ; - output = output' ; - lem2 = lem2' + { args = args' ; + output = output' ; + lem = lem' } @@ -293,144 +336,65 @@ let (morphism_to_obj, obj_to_morphism)= let m' = subst_mps subst m in let c' = subst_morph subst c in if m' == m && c' == c then obj else - (m',c') + (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} + 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 setoids and morphisms **********************) +(************************** Printing relations and morphisms **********************) +(*CSC: still "setoids" in the name *) let print_setoids () = Gmap.iter - (fun k setoid -> - assert (k=setoid.set_aeq) ; - ppnl (str"Setoid " ++ prsetoid setoid ++ str"; equivalence relation properties granted by " ++ - prterm setoid.set_th)) - !setoid_table ; + (fun k relation -> + assert (k=relation.refl_aeq) ; + (*CSC: still "Setoid" in the error message *) + ppnl (str"Setoid " ++ prrelation relation ++ + str"; reflexivity granted by " ++ prterm relation.refl_refl ++ + (match relation.refl_sym with + None -> str "" + | Some t -> str " symmetry granted by " ++ prterm t))) + !relation_table ; Gmap.iter (fun k l -> List.iter - (fun ({lem=lem ; lem2=lem2} as mor) -> + (fun ({lem=lem} as mor) -> ppnl (str "Morphism " ++ prmorphism k mor ++ str ". Compatibility granted by " ++ - prterm lem ++ - (match lem2 with None -> str"" | Some t -> str " and " ++ prterm t) ++ - str ".")) + prterm lem ++ str ".")) l) !morphism_table ;; -(************************** Adding a setoid to the database *********************) - -(* Add a Setoid to the database after a type verification. *) - -let eq_lem_common_sign env a eq = - let na = named_hd env a Anonymous in - let ne = named_hd env eq Anonymous in - [(ne,None,mkApp (eq, [|(mkRel 3);(mkRel 2)|])); - (ne,None,mkApp (eq, [|(mkRel 4);(mkRel 3)|])); - (na,None,a);(na,None,a);(na,None,a);(na,None,a)] - -(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->(eq a c)->(eq b d) *) -let eq_lem_proof env a eq sym trans = - let sign = eq_lem_common_sign env a eq in - let ne = named_hd env eq Anonymous in - let sign = (ne,None,mkApp (eq, [|(mkRel 6);(mkRel 4)|]))::sign in - let ccl = mkApp (eq, [|(mkRel 6);(mkRel 4)|]) in - let body = - mkApp (trans, - [|(mkRel 6);(mkRel 7);(mkRel 4); - (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|])); - (mkApp (trans, - [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]) in - let p = it_mkLambda_or_LetIn body sign in - let t = it_mkProd_or_LetIn ccl sign in - (p,t) - -(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->((eq a c)<->(eq b d)) *) -let eq_lem2_proof env a eq sym trans = - let sign = eq_lem_common_sign env a eq in - let ccl1 = - mkArrow - (mkApp (eq, [|(mkRel 6);(mkRel 4)|])) - (mkApp (eq, [|(mkRel 6);(mkRel 4)|])) in - let ccl2 = - mkArrow - (mkApp (eq, [|(mkRel 5);(mkRel 3)|])) - (mkApp (eq, [|(mkRel 7);(mkRel 5)|])) in - let ccl = mkApp (Lazy.force coqand, [|ccl1;ccl2|]) in - let body = - mkApp ((Lazy.force coqconj), - [|ccl1;ccl2; - lambda_create env - (mkApp (eq, [|(mkRel 6);(mkRel 4)|]), - (mkApp (trans, - [|(mkRel 6);(mkRel 7);(mkRel 4); - (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|])); - (mkApp (trans, - [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]))); - lambda_create env - (mkApp (eq, [|(mkRel 5);(mkRel 3)|]), - (mkApp (trans, - [|(mkRel 7);(mkRel 6);(mkRel 5);(mkRel 3); - (mkApp (trans, - [|(mkRel 6);(mkRel 4);(mkRel 5);(mkRel 1); - (mkApp (sym, [|(mkRel 5);(mkRel 4);(mkRel 2)|]))|]))|])))|]) - in - let p = it_mkLambda_or_LetIn body sign in - let t = it_mkProd_or_LetIn ccl sign in - (p,t) - -let gen_eq_lem_name = - let i = ref 0 in - function () -> - incr i; - make_ident "setoid_eq_ext" (Some !i) - -let add_setoid a aeq th = - let env = Global.env () in - if (is_conv env Evd.empty (Typing.type_of env Evd.empty th) - (mkApp ((Lazy.force coq_Setoid_Theory), [| a; aeq |]))) - then (Lib.add_anonymous_leaf - (setoid_to_obj - (aeq, { set_a = a; - set_aeq = aeq; - set_th = th})); - let sym = mkApp ((Lazy.force coq_seq_sym), [|a; aeq; th|]) in - let trans = mkApp ((Lazy.force coq_seq_trans), [|a; aeq; th|]) in - let (eq_morph, eq_morph_typ) = eq_lem_proof env a aeq sym trans in - let (eq_morph2, eq_morph2_typ) = eq_lem2_proof env a aeq sym trans in - Options.if_verbose ppnl (prterm a ++str " is registered as a setoid"); - let eq_ext_name = gen_eq_lem_name () in - let eq_ext_name2 = gen_eq_lem_name () in - let _ = Declare.declare_constant eq_ext_name - ((DefinitionEntry {const_entry_body = eq_morph; - const_entry_type = Some eq_morph_typ; - const_entry_opaque = true}), - IsProof Lemma) in - let _ = Declare.declare_constant eq_ext_name2 - ((DefinitionEntry {const_entry_body = eq_morph2; - const_entry_type = Some eq_morph2_typ; - const_entry_opaque = true}), - IsProof Lemma) in - let eqmorph = (current_constant eq_ext_name) in - let eqmorph2 = (current_constant eq_ext_name2) in - (Lib.add_anonymous_leaf - (morphism_to_obj (aeq, - { lem = eqmorph; - args = [ACSetoid aeq; ACSetoid aeq]; - output = ACSetoid (Lazy.force coqiff); - lem2 = (Some eqmorph2)}))); - Options.if_verbose ppnl (prterm aeq ++str " is registered as a morphism")) - else errorlabstrm "Add Setoid" (str "Not a valid setoid theory") - -(* The vernac command "Add Setoid" *) -let add_setoid a aeq th = - add_setoid (constr_of a) (constr_of aeq) (constr_of th) +(************************** Adding a relation to the database *********************) + +let int_add_relation a aeq refl sym = + match refl with + None -> assert false (*CSC: unimplemented yet*) + | Some refl -> + let env = Global.env () in + if + (is_conv env Evd.empty (Typing.type_of env Evd.empty refl) + (mkApp ((Lazy.force coq_is_reflexive), [| a; aeq |]))) + then + Lib.add_anonymous_leaf + (relation_to_obj + (aeq, { refl_a = a; + refl_aeq = aeq; + refl_refl = refl; + refl_sym = sym})) + else + errorlabstrm "Add Relation Class" + (str "Not a valid proof of reflexivity") + +(* The vernac command "Add Relation ..." *) +let add_relation a aeq refl sym = + int_add_relation (constr_of a) (constr_of aeq) (option_app constr_of refl) + (option_app constr_of sym) (***************** Adding a morphism to the database ****************************) @@ -458,64 +422,33 @@ let check_is_dependent t n = else false in aux t 0 n -let gen_lem_name m = match kind_of_term m with - | Var id -> add_suffix id "_ext" - | Const kn -> add_suffix (id_of_label (label kn)) "_ext" - | Ind (kn, i) -> add_suffix (id_of_label (label kn)) ((string_of_int i)^"_ext") - | Construct ((kn,i),j) -> add_suffix - (id_of_label (label kn)) ((string_of_int i)^(string_of_int j)^"_ext") - | _ -> errorlabstrm "New Morphism" (str "The term " ++ prterm m ++ str "is not a known name") - -let gen_lemma_tail m args body n = - let l = (List.length args) in - let a1 = Array.create l (mkRel 0) in - let a2 = Array.create l (mkRel 0) in - let rec aux i n = function - | (ACSetoid _)::tl -> - a1.(i) <- (mkRel n); - a2.(i) <- (mkRel (n-1)); - aux (i+1) (n-2) tl - | (ACLeibniz _)::tl -> - a1.(i) <- (mkRel n); - a2.(i) <- (mkRel n); - aux (i+1) (n-1) tl - | [] -> () in - aux 0 n args; - if (match body with ACSetoid setoid when setoid.set_aeq = Lazy.force coqiff -> true | _ -> false) - then mkArrow (mkApp (m,a1)) (lift 1 (mkApp (m, a2))) - else - match body with - ACSetoid setoid -> - mkApp (setoid.set_aeq, [|(mkApp (m, a1)); (mkApp (m, a2))|]) - | ACLeibniz t -> - mkApp ((Lazy.force coqeq), [|t; (mkApp (m, a1)); (mkApp (m, a2))|]) - -let gen_lemma_middle m args body n = - let rec aux i n = - function - | [] -> gen_lemma_tail m args body n - | (ACSetoid setoid)::tl -> - let t = setoid.set_a in - mkArrow (mkApp (setoid.set_aeq, - [|(mkRel i); (mkRel (i-1))|])) (aux (i-1) (n+1) tl) - | (ACLeibniz t)::tl -> aux (i-1) n tl - in aux n n args - -let gen_compat_lemma env m body args = - let rec aux n = - function - (ACSetoid setoid)::tl -> - let t = setoid.set_a in - prod_create env (t,(prod_create env (t, (aux (n+2) tl)))) - | (ACLeibniz t)::tl -> - prod_create env (t, (aux (n+1) tl)) - | [] -> gen_lemma_middle m args body n - in aux 0 args +(*CSC: I do not like this very much. I would prefer relation classes + to be CIC objects. Keeping backward compatibility, however, is annoying. *) +let cic_relation_class_of_relation_class = + function + ACReflexive {refl_a = refl_a; refl_aeq = refl_aeq; refl_refl = refl_refl} -> + mkApp ((Lazy.force coq_Reflexive), [| refl_a ; refl_aeq; refl_refl |]) + | ACLeibniz t -> mkApp ((Lazy.force coq_Leibniz), [| t |]) + +let gen_compat_lemma_statement output args m = + let rec mk_signature = + function + [] -> assert false + | [last] -> + mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Relation_Class; last |]) + | he::tl -> + mkApp ((Lazy.force coq_cons), + [| Lazy.force coq_Relation_Class; he ; mk_signature tl |]) + in + let output = cic_relation_class_of_relation_class output in + let args= mk_signature (List.map cic_relation_class_of_relation_class args) in + args, output, + mkApp ((Lazy.force coq_make_compatibility_goal), [| args ; output ; m |]) let new_morphism m id hook = let env = Global.env() in let typeofm = (Typing.type_of env Evd.empty m) in - let typ = (nf_betaiota typeofm) in (* nf_bdi avant, mais bug *) + let typ = (nf_betaiota typeofm) in let (argsrev, output) = (decompose_prod typ) in let args_ty = (List.map snd (List.rev argsrev)) in if (args_ty=[]) @@ -524,371 +457,420 @@ let new_morphism m id hook = else if (check_is_dependent typ (List.length args_ty)) then errorlabstrm "New Morphism" (str "The term " ++ prterm m ++ str" should not be a dependent product") - else ( - let args = List.map default_setoid_for_carrier args_ty in - let output = default_setoid_for_carrier output in - let lem = (gen_compat_lemma env m output args) in - new_edited id (m,args,output); - Pfedit.start_proof id (IsGlobal (Proof Lemma)) - (Declare.clear_proofs (Global.named_context ())) - lem hook; - (Options.if_verbose msg (Pfedit.pr_open_subgoals ()))) - -let rec sub_bool n = function - | [] -> [] - | (ACSetoid setoid)::tl -> (setoid, n)::(sub_bool (n-2) tl) - | (ACLeibniz _)::tl -> (sub_bool (n-1) tl) - -let gen_lemma_iff_tail m mext args n k = - let a1 = Array.create k (mkRel 0) in - let a2 = Array.create k (mkRel 0) in - let nb = List.length args in - let b1 = Array.create nb (mkRel 0) in - let b2 = Array.create nb (mkRel 0) in - let rec aux i j = function - |[] -> () - |(ACSetoid _)::tl -> - (a1.(i) <- (mkRel j); - a1.(i+1) <- (mkRel (j-1)); - a2.(i) <- (mkRel (j-1)); - a2.(i+1) <- (mkRel j); - aux (i+2) (j-2) tl) - |(ACLeibniz _)::tl -> - (a1.(i) <- (mkRel j); - a2.(i) <- (mkRel j); - aux (i+1) (j-1) tl) in - let rec aux2 i j = function - | ({set_a=a; set_th=th; set_aeq=aeq},p)::tl -> - a1.(i) <- (mkRel j); - a2.(i) <- mkApp ((Lazy.force coq_seq_sym), - [|a; aeq; th; (mkRel p); (mkRel (p-1)); (mkRel j)|]); - aux2 (i+1) (j-1) tl - | [] -> () in - let rec aux3 i j = function - | (ACSetoid _)::tl -> - b1.(i) <- (mkRel j); - b2.(i) <- (mkRel (j-1)); - aux3 (i+1) (j-2) tl - | (ACLeibniz _)::tl -> - b1.(i) <- (mkRel j); - b2.(i) <- (mkRel j); - aux3 (i+1) (j-1) tl - | [] -> () in - aux 0 k args; - aux2 n (k-n) (sub_bool k args); - aux3 0 k args; - mkApp ((Lazy.force coqconj), - [|(mkArrow (mkApp (m,b1)) (lift 1 (mkApp (m, b2)))); - (mkArrow (mkApp (m,b2)) (lift 1 (mkApp (m, b1)))); - (mkApp (mext, a1));(mkApp (mext, a2))|]) - -let gen_lemma_iff_middle env m mext args n = - let rec aux i k = - function - [] -> gen_lemma_iff_tail m mext args n k - | (ACSetoid setoid)::tl -> - lambda_create env - ((mkApp (setoid.set_aeq, [|(mkRel i); (mkRel (i-1))|])), - (aux (i-1) (k+1) tl)) - | (ACLeibniz t)::tl -> aux (i-1) k tl - in aux n n args - -let gen_lem_iff env m mext args = - let rec aux n = - function - (ACSetoid setoid)::tl -> - let t = setoid.set_a in - lambda_create env (t,(lambda_create env (t, (aux (n+2) tl)))) - | (ACLeibniz t)::tl -> - lambda_create env (t, (aux (n+1) tl)) - | [] -> gen_lemma_iff_middle env m mext args n - in aux 0 args - -let add_morphism lem_name (m,args,output) = - let env = Global.env() in - let mext = (current_constant lem_name) in - let args_constr= List.map constr_setoid_class_of_setoid_setoid_class args in - let output_constr = constr_setoid_class_of_setoid_setoid_class output in - (if (match output with ACSetoid setoid when setoid.set_aeq = Lazy.force coqiff -> true | _ -> false) - then - (let lem_2 = gen_lem_iff env m mext args in - let lem2_name = add_suffix lem_name "2" in - let _ = Declare.declare_constant lem2_name - ((DefinitionEntry {const_entry_body = lem_2; - const_entry_type = None; - const_entry_opaque = true}), - IsProof Lemma) in - let lem2 = (current_constant lem2_name) in - (Lib.add_anonymous_leaf - (morphism_to_obj (m, - { lem = mext; - args = args_constr; - output = output_constr; - lem2 = (Some lem2)}))); - Options.if_verbose message ((string_of_id lem2_name) ^ " is defined")) else - (Lib.add_anonymous_leaf - (morphism_to_obj (m, - { lem = mext; - args = args_constr; - output = output_constr; - lem2 = None})))); - Options.if_verbose ppnl (prterm m ++str " is registered as a morphism") + begin + let args = List.map default_relation_for_carrier args_ty in + let output = default_relation_for_carrier output in + let argsconstr,outputconstr,lem = + gen_compat_lemma_statement output args m + in + new_edited id (m,args,argsconstr,output,outputconstr); + Pfedit.start_proof id (IsGlobal (Proof Lemma)) + (Declare.clear_proofs (Global.named_context ())) + lem hook; + (* "unfold make_compatibility_goal" *) + Pfedit.by + (Tactics.unfold_constr + (Lazy.force coq_make_compatibility_goal_ref)) ; + (* "unfold make_compatibility_goal_aux" *) + Pfedit.by + (Tactics.unfold_constr + (Lazy.force coq_make_compatibility_goal_aux_ref)) ; + (* "simpl" *) + Pfedit.by Tactics.simpl_in_concl ; + Options.if_verbose msg (Pfedit.pr_open_subgoals ()); + end + +let add_morphism lemma_infos mor_name (m,args,output) = + let env = Global.env() in + begin + match lemma_infos with + None -> () (* the Morphism_Theory object has alrady been created *) + | 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_constant mor_name + (DefinitionEntry + {const_entry_body = + mkApp ((Lazy.force coq_Build_Morphism_Theory), + [| argsconstr; outputconstr; m ; mext |]); + const_entry_type = None; + const_entry_opaque = false}, + IsDefinition)) + end ; + let mmor = current_constant mor_name in + let args_constr = + List.map constr_relation_class_of_relation_relation_class 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 = mmor })); + Options.if_verbose ppnl (prterm m ++ str " is registered as a morphism") let morphism_hook stre ref = let pf_id = id_of_global ref in + let mor_id = id_of_string (string_of_id pf_id ^ "_morphism_theory") in + let (m,args,argsconstr,output,outputconstr) = what_edited pf_id in if (is_edited pf_id) then - (add_morphism pf_id (what_edited pf_id); no_more_edited pf_id) + add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id + (m,args,output); no_more_edited pf_id let new_named_morphism id m = new_morphism (constr_of m) id morphism_hook +(************************ Add Setoid ******************************************) + +(*CSC: I do not like this. I would prefer more self-describing constant names *) +let gen_morphism_name = + let i = ref 0 in + function () -> + incr i; + make_ident "morphism_of_setoid_equality" (Some !i) + +(* The vernac command "Add Setoid" *) +let add_setoid a aeq th = + let a = constr_of a in + let aeq = constr_of aeq in + let th = constr_of th in + let env = Global.env () in + if is_conv env Evd.empty (Typing.type_of env Evd.empty th) + (mkApp ((Lazy.force coq_Setoid_Theory), [| a; aeq |])) + then + begin + let refl = mkApp ((Lazy.force coq_seq_refl), [| a; aeq; th |]) in + let sym = mkApp ((Lazy.force coq_seq_sym), [| a; aeq; th |]) in + int_add_relation a aeq (Some refl) (Some sym) ; + let mor_name = gen_morphism_name () in + let _ = + Declare.declare_constant mor_name + (DefinitionEntry + {const_entry_body = + mkApp + ((Lazy.force coq_equality_morphism_of_setoid_theory), + [| a; aeq; th |]) ; + const_entry_type = None; + const_entry_opaque = false}, + IsDefinition) in + let aeq_rel = + ACReflexive + {refl_a = a ; refl_aeq = aeq ; refl_refl = refl ; refl_sym = (Some sym)} + in + add_morphism None mor_name + (aeq,[aeq_rel;aeq_rel],Lazy.force coq_prop_relation) + end + else + errorlabstrm "Add Setoid" (str "Not a valid setoid theory") + + (****************************** The tactic itself *******************************) type constr_with_marks = - | MApp of morphism_class Lazy.t * constr_with_marks array - | Toreplace of setoid - | Tokeep + | MApp of constr * morphism_class * constr_with_marks array + | Toreplace + | Tokeep of constr | Mimp of constr_with_marks * constr_with_marks let is_to_replace = function - | Tokeep -> false - | Toreplace _ -> true + | Tokeep _ -> false + | Toreplace -> true | MApp _ -> true | Mimp _ -> true let get_mark a = Array.fold_left (||) false (Array.map is_to_replace a) -exception Use_replace +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)))) -let mark_occur gl hyp = +let relation_of_hypothesis_and_term_to_rewrite gl (_,h) t = + let hypt = pf_type_of gl h in + let (heq, hargs) = decompose_app hypt in + let rec get_all_but_last_two = + function + [] + | [_] -> assert false + | [_;_] -> [] + | he::tl -> he::(get_all_but_last_two tl) in + let aeq = mkApp (heq,(Array.of_list (get_all_but_last_two hargs))) in + try + relation_table_find aeq + with Not_found -> + (*CSC: still "setoid" in the error message *) + errorlabstrm "Setoid_rewrite" + (prterm aeq ++ str " is not a setoid equality.") + +let mark_occur t in_c = let rec aux t in_c = - if (eq_constr t in_c) then - let sa = - match hyp with - None -> - (match default_setoid_for_carrier (pf_type_of gl t) with - ACSetoid sa -> sa - | ACLeibniz _ -> raise Use_replace) - | Some h -> - let hypt = pf_type_of gl h in - let (heq, hargs) = decompose_app hypt in - let rec get_all_but_last_two = - function - [] - | [_] -> assert false - | [_;_] -> [] - | he::tl -> he::(get_all_but_last_two tl) in - let aeq = mkApp (heq,(Array.of_list (get_all_but_last_two hargs))) in - try - setoid_table_find aeq - with Not_found -> - errorlabstrm "Setoid_rewrite" - (prterm aeq ++ str " is not a setoid equality.") - in - Toreplace sa + if eq_constr t in_c then + Toreplace else match kind_of_term in_c with | App (c,al) -> - let a = Array.map (aux t) al in - let mor = - lazy - (try - begin - match morphism_table_find c with - [] -> assert false - | morphism::tl -> - if tl <> [] then - msg_warning - (str "There are several morphisms declared for " ++ - prterm c ++ - str ". The morphism " ++ prmorphism c morphism ++ - str " is randomly chosen.") ; - ACMorphism (setoid_morphism_of_constr_morphism morphism) - end - with Not_found -> - let env = Global.env() in - let typeofc = (Typing.type_of env Evd.empty c) in - let typ = nf_betaiota typeofc in - let (argsrev, output) = decompose_prod typ in - ACFunction - {f_args=List.rev (List.map snd argsrev); f_output=output}) - in - if (get_mark a) then MApp (mor,a) else Tokeep + let a = Array.map (aux t) al in + if not (get_mark a) then Tokeep in_c + else + let mor = + try + begin + match morphism_table_find c with + [] -> assert false + | morphism::tl -> + if tl <> [] then + msg_warning + (str "There are several morphisms declared for " ++ + prterm c ++ + str ". The morphism " ++ prmorphism c morphism ++ + str " is randomly chosen.") ; + Some + (ACMorphism + (relation_morphism_of_constr_morphism morphism)) + end + with Not_found -> None + in + (match mor with + Some mor -> MApp (c,mor,a) + | None -> + (* the tactic works only if the function type is + made of non-dependent products only. However, here we + can cheat a bit by partially istantiating c to match + the requirement when the arguments to be replaced are + bound by non-dependent products only. *) + let env = Global.env() in + let typeofc = (Typing.type_of env Evd.empty 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 + [] -> + let mor = + ACFunction {f_args=List.rev f_args_rev ; f_output=typ} in + let func = beta_expand c c_args_rev in + MApp (func,mor,Array.of_list (List.rev a_rev)) + | (he::tl) as a-> + let typnf = Reduction.whd_betadeltaiota env typ in + match kind_of_term typnf with + Cast (typ,_) -> + find_non_dependent_function env c c_args_rev typ + f_args_rev a_rev a + | Prod (name,s,t) -> + let env' = push_rel (name,None,s) env in + begin + match noccurn 1 t, he with + _, Tokeep arg -> + (* 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 *) + (*CSC: 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 authors.") + end + | _ -> assert false + in + find_non_dependent_function env c [] typ [] [] + (Array.to_list a)) | Prod (_, c1, c2) -> - if (dependent (mkRel 1) c2) - then Tokeep - else - let c1m = aux t c1 in - let c2m = aux t c2 in - if ((is_to_replace c1m)||(is_to_replace c2m)) - then (Mimp (c1m, c2m)) - else Tokeep - | _ -> Tokeep + if (dependent (mkRel 1) c2) + then Tokeep in_c + else + let c1m = aux t c1 in + let c2m = aux t c2 in + if ((is_to_replace c1m)||(is_to_replace c2m)) + then (Mimp (c1m, c2m)) + else Tokeep in_c + | _ -> Tokeep in_c + in aux t in_c + +let cic_morphism_context_list_of_list hole_relation = + let rec aux = + function + [] -> assert false + | [out,value] -> + mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Relation_Class ; out |]), + mkApp ((Lazy.force coq_fcl_singl), [| hole_relation; out ; value |]) + | (out,value)::tl -> + let outtl, valuetl = aux tl in + mkApp ((Lazy.force coq_cons), + [| Lazy.force coq_Relation_Class ; out ; outtl |]), + mkApp ((Lazy.force coq_fcl_cons), + [| hole_relation ; out ; outtl ; value ; valuetl |]) in aux -let create_args ca ma args c1 c2 = - let rec aux i = function - | [] -> [] - | (ACSetoid _)::tl -> - if is_to_replace ma.(i) - then (replace_term c1 c2 ca.(i))::ca.(i)::(aux (i+1) tl) - else ca.(i)::ca.(i)::(aux (i+1) tl) - | (ACLeibniz _)::tl -> - if is_to_replace ma.(i) - then - let newarg = replace_term c1 c2 ca.(i) in - newarg::(aux (i+1) tl) - else ca.(i)::(aux (i+1) tl) - in - aux 0 args - -let res_tac sa c hyp glll = - let fin = match hyp with - | None -> Auto.full_trivial - | Some h -> - tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0 "")) - (tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0 "")) - Auto.full_trivial) +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 = + let rec aux out = + function + MApp (f, m, args) -> + let morphism_theory, relations = + match m with + ACMorphism { args = args ; lem = lem } -> lem,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_prop_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 -> ACLeibniz x) f_args in + let cic_relations = + List.map cic_relation_class_of_relation_class relations in + let cic_args_relations,argst = + cic_morphism_context_list_of_list hole_relation + (List.combine cic_relations + (List.map2 (fun t v -> aux t v) cic_relations + (Array.to_list args))) + in + mkApp ((Lazy.force coq_App), + [|hole_relation ; cic_args_relations ; out ; morphism_theory ; argst|]) + | Toreplace -> + mkApp ((Lazy.force coq_Toreplace), [| hole_relation |]) + | Tokeep c -> + mkApp ((Lazy.force coq_Tokeep), [| hole_relation ; out ; c |]) + | Mimp (source, target) -> + mkApp ((Lazy.force coq_Imp), + [| hole_relation ; aux out source ; aux out target |]) + in aux + +let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m = + let {refl_aeq=hole_equality; refl_sym=hole_symmetry} = hole_relation in + let hole_relation = + cic_relation_class_of_relation_class (ACReflexive hole_relation) in + let prop_relation = + cic_relation_class_of_relation_class (Lazy.force coq_prop_relation) in + let hyp = + if lft2rgt then h else + match hole_symmetry with + Some sym -> + mkApp (sym, [| c2 ; c1 ; h |]) + | None -> + errorlabstrm "Setoid_rewrite" + (str "Rewriting from right to left not permitted since the " ++ + str "relation " ++ prterm hole_equality ++ str " is not known " ++ + str "to be symmetric. Either declare it as a symmetric " ++ + str "relation or use setoid_replace or (setoid_)rewrite from " ++ + str "left to right only.") + in + mkApp ((Lazy.force coq_setoid_rewrite), + [| hole_relation ; prop_relation ; c1 ; c2 ; + syntactic_but_representation_of_marked_but hole_relation + prop_relation m ; hyp |]) + +let relation_rewrite c1 c2 (lft2rgt,cl) gl = + let but = pf_concl gl in + let (hyp,c1,c2) = + let (cl',_) = Clenv.unify_to_subterm cl (c1,but) in + let c1 = Clenv.clenv_instance_term cl' c1 in + let c2 = Clenv.clenv_instance_term cl' c2 in + (lft2rgt,Clenv.clenv_instance_template cl'), c1, c2 + in + let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in + let marked_but = mark_occur c1 but in + let th = + apply_coq_setoid_rewrite input_relation c1 c2 hyp marked_but in - tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0 "")) - (tclORELSE assumption - (tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|])))) assumption) - fin)) - -let id_res_tac (*c*) sa = - (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th(*; c*)|]))) - -(* An exception to catchs errors *) - -exception Nothing_found of constr;; - -(* special case of replace_where_needed_gen where all the arguments - are of class (ACLeibniz _) *) -let rec replace_where_needed hyp ca ma c1 c2 = - let rec aux i = function - | [] -> tclIDTAC - | he::tl -> - if is_to_replace he then - let dummy = mkProp in (* dummy will never be used *) + let thty = pf_type_of gl th in + let simplified_thty = + pf_unfoldn [[], Lazy.force coq_iff] gl + (pf_unfoldn [[], Lazy.force coq_relation_of_relation_class] gl thty) + in + let ty1,ty2 = + match destApplication simplified_thty with + (_ (*and*),[|ty1;ty2|]) -> ty1,ty2 + | _ -> assert false + in + let th' = mkApp ((Lazy.force coq_proj2), [|ty1; ty2; th|]) in + let hyp2 = Termops.replace_term c1 c2 but in + let simplified_thty' = mkProd (Anonymous, hyp2, lift 1 but) in + (*CSC: the next line does not work because simplified_thty' is not + used to generate the type of the new goals ;-( + Tactics.apply (mkCast (th',simplified_thty')) gl + Thus I am using the following longer (and less accurate) code *) tclTHENS - (!replace ca.(i) (replace_term c1 c2 ca.(i))) - [aux (i+1) tl; zapply (Some(ACLeibniz dummy)) false ca.(i) he c1 c2 hyp] - else - (aux (i+1) tl) - in - aux 0 ma -and replace_where_needed_gen hyp ca ma args c1 c2 = - let rec aux i = function - | [] -> tclIDTAC - | ((ACLeibniz _) as he)::tl -> - if is_to_replace ma.(i) then - tclTHENS - (!replace ca.(i) (replace_term c1 c2 ca.(i))) - [aux (i+1) tl ; zapply (Some he) false ca.(i) ma.(i) c1 c2 hyp ] - else - aux (i+1) tl - | (ACSetoid _)::tl -> aux (i+1) tl - in - aux 0 args -and create_tac_list i a al c1 c2 hyp = function - | [] -> [] - | (ACLeibniz _)::tl -> create_tac_list (i+1) a al c1 c2 hyp tl - | ((ACSetoid setoid) as he)::tl -> - if (is_to_replace a.(i)) - then (zapply (Some he) false al.(i) a.(i) c1 c2 hyp)::(create_tac_list (i+1) a al c1 c2 hyp tl) - else (id_res_tac (*al.(i)*) setoid)::(create_tac_list (i+1) a al c1 c2 hyp tl) - -and zapply close is_r gl gl_m c1 c2 hyp glll = - (match ((kind_of_term gl), gl_m) with - | ((App (c,al)),(MApp (m,a))) -> - (match Lazy.force m with - ACMorphism m -> - let args = Array.of_list (create_args al a m.args c1 c2) in - tclTHENS - (replace_where_needed_gen hyp al a m.args c1 c2) - [if is_r - then tclTHENS (apply (mkApp (m.lem, args))) - ((create_tac_list 0 a al c1 c2 hyp m.args)@[tclIDTAC]) - else - match m.lem2 with - None -> - tclTHENS (apply (mkApp (m.lem, args))) - (create_tac_list 0 a al c1 c2 hyp m.args) - | Some xom -> - tclTHENS (apply (mkApp (xom, args))) - (create_tac_list 0 a al c1 c2 hyp m.args)] - | ACFunction f -> - tclTHENS - (replace_where_needed hyp al (Array.to_list a) c1 c2) - [match close with - None -> tclIDTAC - | Some (ACLeibniz _) -> reflexivity - | Some (ACSetoid setoid) -> id_res_tac setoid]) - | ((Prod (_,hh, cc)),(Mimp (hhm, ccm))) -> - let al = [|hh; cc|] in - let a = [|hhm; ccm|] in - let fleche_constr = (Lazy.force coq_fleche) in - let fleche_cp = destConst fleche_constr in - let new_concl = (mkApp (fleche_constr, al)) in - let m = find_morphism_fleche () in - if is_r - then - let args = Array.of_list (create_args al a m.args c1 c2) in - tclTHEN (change_in_concl None new_concl) - (tclTHENS (apply (mkApp (m.lem, args))) - ((create_tac_list 0 a al c1 c2 hyp m.args)@[unfold_constr (ConstRef fleche_cp)])) - else - (zapply (Some m.output) is_r new_concl - (MApp (lazy (ACMorphism m),a)) c1 c2 hyp) - | (_, Toreplace setoid) -> - if is_r - then (match hyp with - | None -> errorlabstrm "Setoid_replace" - (str "You should use the tactic Replace here") - | Some h -> - let hypt = pf_type_of glll h in - let (heq, hargs) = decompose_app hypt in - let rec get_last_two = function - | [c1;c2] -> (c1, c2) - | x::y::z -> get_last_two (y::z) - | _ -> assert false in - let (hc1,hc2) = get_last_two hargs in - if c1 = hc1 - then - apply (mkApp (Lazy.force coqproj2,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|])) - else - apply (mkApp (Lazy.force coqproj1,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|])) - ) - else (res_tac setoid gl hyp glll) - | (_, Tokeep) -> (match hyp with - | None -> errorlabstrm "Setoid_replace" - (str "No replacable occurence of " ++ prterm c1 ++ str " found") - | Some _ ->errorlabstrm "Setoid_replace" - (str "No rewritable occurence of " ++ prterm c1 ++ str " found")) - | _ -> assert false) glll - -let setoid_replace c1 c2 hyp gl = - let but = (pf_concl gl) in - try - (zapply None true but (mark_occur gl hyp c1 but) c1 c2 hyp) gl - with - Use_replace -> (!replace c1 c2) gl + (Tactics.apply (mkCast (th',simplified_thty'))) + [Tactics.change_in_concl None hyp2] gl + (*CSC: this is another way to proceed, but the generated proof_term + would be much bigger than possible + Tactics.forward true Anonymous (mkCast (th',simplified_thty')) gl + (... followed by the application of the introduced hypothesis ...) + *) let general_s_rewrite lft2rgt c gl = - let ctype = pf_type_of gl c in - let (equiv, args) = decompose_app ctype in - let rec get_last_two = function - | [c1;c2] -> (c1, c2) - | x::y::z -> get_last_two (y::z) - | _ -> error "The term provided is not an equivalence" in - let (c1,c2) = get_last_two args in - if lft2rgt - then setoid_replace c1 c2 (Some c) gl - else setoid_replace c2 c1 (Some c) gl - -let setoid_replace c1 c2 = setoid_replace c1 c2 None + let (wc,_) = Evar_refiner.startWalk gl in + let ctype = pf_type_of gl c in + let eqclause = + Clenv.make_clenv_binding wc (c,ctype) Rawterm.NoBindings in + let (equiv, args) = + decompose_app (Clenv.clenv_instance_template_type eqclause) in + let rec get_last_two = function + | [c1;c2] -> (c1, c2) + | x::y::z -> get_last_two (y::z) + | _ -> error "The term provided is not an equivalence" in + let (c1,c2) = get_last_two args in + if lft2rgt + then relation_rewrite c1 c2 (lft2rgt,eqclause) gl + else relation_rewrite c2 c1 (lft2rgt,eqclause) gl + +exception Use_replace + +(*CSC: the name should be changed *) +let setoid_replace c1 c2 gl = + try + let relation = + match default_relation_for_carrier (pf_type_of gl c1) with + ACReflexive sa -> sa + | ACLeibniz _ -> raise Use_replace + in + let eq = mkApp (relation.refl_aeq, [| c1 ; c2 |]) in + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN + (general_s_rewrite true (mkVar id)) + (clear [id])); + Tacticals.tclIDTAC] gl + with + Use_replace -> (!replace c1 c2) gl let setoid_rewriteLR = general_s_rewrite true diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 02046c55b..e41728ead 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -27,6 +27,9 @@ val setoid_rewriteRL : constr -> tactic val general_s_rewrite : bool -> constr -> tactic +val add_relation : + constr_expr -> constr_expr -> constr_expr option -> constr_expr option -> unit + val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit val new_named_morphism : Names.identifier -> constr_expr -> unit diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index bca2bf9de..bf54f0567 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -1,3 +1,4 @@ + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -8,64 +9,345 @@ (*i $Id$: i*) -Section Setoid. +Set Implicit Arguments. + +(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *) + +Definition is_reflexive (A: Type) (Aeq: A -> A -> Prop) : Prop := + forall x:A, Aeq x x. + +Definition is_symmetric (A: Type) (Aeq: A -> A -> Prop) : Prop := + forall (x y:A), Aeq x y -> Aeq y x. + +Inductive Relation_Class : Type := + Reflexive : forall A Aeq, (@is_reflexive A Aeq) -> Relation_Class + | Leibniz : Type -> Relation_Class. + +Implicit Type Hole Out: Relation_Class. + +Definition carrier_of_relation_class : Relation_Class -> Type. + intro; case X; intros. + exact A. + exact T. +Defined. + +Inductive nelistT (A : Type) : Type := + singl : A -> (nelistT A) + | cons : A -> (nelistT A) -> (nelistT A). + +Implicit Type In: (nelistT Relation_Class). + +Definition function_type_of_morphism_signature : + (nelistT Relation_Class) -> 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; destruct Out; simpl in f, g. + exact (forall (x1 x2: A), (Aeq x1 x2) -> (Aeq0 (f x1) (g x2))). + exact (forall (x1 x2: A), (Aeq x1 x2) -> f x1 = g x2). + exact (forall (x: T), (Aeq (f x) (g x))). + exact (forall (x: T), f x = g x). + induction a; simpl in f, g. + exact (forall (x1 x2: A), (Aeq x1 x2) -> IHIn (f x1) (g x2)). + exact (forall (x: T), 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}. + +Definition list_of_Leibniz_of_list_of_types: + nelistT Type -> nelistT Relation_Class. + induction 1. + exact (singl (Leibniz a)). + exact (cons (Leibniz a) IHX). +Defined. + +(* every function is a morphism from Leibniz+ to Leibniz *) +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. + +(* THE Prop RELATION CLASS *) + +Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym. + +Definition Prop_Relation_Class : Relation_Class. + eapply (@Reflexive _ iff). + exact iff_refl. +Defined. + +(* every predicate is morphism from Leibniz+ to Prop_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' Prop_Relation_Class -> + Morphism_Theory In' Prop_Relation_Class. + intros. + exists X. + induction In; unfold make_compatibility_goal; simpl. + intro; apply iff_refl. + intro; apply (IHIn (X x)). +Defined. + +(* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *) + +Inductive Morphism_Context Hole : Relation_Class -> Type := + App : forall In Out, + Morphism_Theory In Out -> Morphism_Context_List Hole In -> + Morphism_Context Hole Out + | Toreplace : Morphism_Context Hole Hole + | Tokeep : + forall (S: Relation_Class), + carrier_of_relation_class S -> Morphism_Context Hole S + | Imp : + Morphism_Context Hole Prop_Relation_Class -> + Morphism_Context Hole Prop_Relation_Class -> + Morphism_Context Hole Prop_Relation_Class +with Morphism_Context_List Hole: nelistT Relation_Class -> Type := + fcl_singl : + forall (S: Relation_Class), Morphism_Context Hole S -> + Morphism_Context_List Hole (singl S) + | fcl_cons : + forall (S: Relation_Class) (L: nelistT Relation_Class), + Morphism_Context Hole S -> Morphism_Context_List Hole L -> + Morphism_Context_List Hole (cons S L). + +Scheme Morphism_Context_rect2 := Induction for Morphism_Context Sort Type +with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type. + +Inductive prodT (A B: Type) : Type := + pairT : A -> B -> prodT A B. + +Definition product_of_relation_class_list : nelistT Relation_Class -> Type. + induction 1. + exact (carrier_of_relation_class a). + exact (prodT (carrier_of_relation_class a) IHX). +Defined. -Variable A : Type. -Variable Aeq : A -> A -> Prop. +Definition relation_of_relation_class: + forall Out, + carrier_of_relation_class Out -> carrier_of_relation_class Out -> Prop. + destruct Out. + exact Aeq. + exact (@eq T). +Defined. -Record Setoid_Theory : Prop := +Definition relation_of_product_of_relation_class_list: + forall In, + product_of_relation_class_list In -> product_of_relation_class_list In -> Prop. + induction In. + exact (relation_of_relation_class a). + + simpl; intros. + destruct X; destruct X0. + exact (relation_of_relation_class a c c0 /\ IHIn p p0). +Defined. + +Definition apply_morphism: + forall In Out (m: function_type_of_morphism_signature In Out) + (args: product_of_relation_class_list 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: + forall In Out (m1 m2: function_type_of_morphism_signature In Out) + (args1 args2: product_of_relation_class_list In), + make_compatibility_goal_aux _ _ m1 m2 -> + relation_of_product_of_relation_class_list _ args1 args2 -> + relation_of_relation_class _ + (apply_morphism _ _ m1 args1) + (apply_morphism _ _ m2 args2). + intros. + induction In. + simpl; simpl in m1, m2, args1, args2, H0. + destruct a; destruct Out. + apply H; exact H0. + simpl; apply H; exact H0. + simpl; rewrite H0; apply H. + simpl; rewrite H0; apply H. + simpl in 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. + rewrite H0; apply IHIn. + apply H. + exact H1. +Qed. + +Definition interp : + forall Hole Out, carrier_of_relation_class Hole -> + Morphism_Context Hole Out -> carrier_of_relation_class Out. + intros Hole Out H t. + elim t using + (@Morphism_Context_rect2 Hole (fun S _ => carrier_of_relation_class S) + (fun L fcl => product_of_relation_class_list L)); + intros. + exact (apply_morphism _ _ (Function m) X). + exact H. + exact c. + exact (X -> X0). + exact X. + split; [ 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 (L: nelistT Relation_Class), carrier_of_relation_class Hole -> + Morphism_Context_List Hole L -> product_of_relation_class_list L. + intros Hole L H t. + elim t using + (@Morphism_Context_List_rect2 Hole (fun S _ => carrier_of_relation_class S) + (fun L fcl => product_of_relation_class_list L)); + intros. + exact (apply_morphism _ _ (Function m) X). + exact H. + exact c. + exact (X -> X0). + exact X. + split; [ exact X | exact X0 ]. +Defined. + +Theorem setoid_rewrite: + forall Hole Out (E1 E2: carrier_of_relation_class Hole) + (E: Morphism_Context Hole Out), + (relation_of_relation_class Hole E1 E2) -> + (relation_of_relation_class Out (interp E1 E) (interp E2 E)). + intros. + elim E using + (@Morphism_Context_rect2 Hole + (fun S E => relation_of_relation_class S (interp E1 E) (interp E2 E)) + (fun L fcl => + relation_of_product_of_relation_class_list _ + (interp_relation_class_list E1 fcl) + (interp_relation_class_list E2 fcl))); + intros. + change (relation_of_relation_class Out0 + (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0)) + (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))). + apply apply_morphism_compatibility. + exact (Compat m). + exact H0. + + exact H. + + unfold interp, Morphism_Context_rect2. + (*CSC: reflexivity used here*) + destruct S. + apply i. + simpl; reflexivity. + + change + (relation_of_relation_class Prop_Relation_Class + (interp E1 m -> interp E1 m0) (interp E2 m -> interp E2 m0)). + simpl; simpl in H0, H1. + tauto. + + exact H0. + + change + (relation_of_relation_class _ (interp E1 m) (interp E2 m) /\ + relation_of_product_of_relation_class_list _ + (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)). + split. + exact H0. + exact H1. +Qed. + +(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *) + +Record Setoid_Theory (A: Type) (Aeq: A -> A -> Prop) : Prop := {Seq_refl : forall x:A, Aeq x x; Seq_sym : forall x y:A, Aeq x y -> Aeq y x; Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z}. -End Setoid. +Definition relation_class_of_setoid_theory: + forall (A: Type) (Aeq: A -> A -> Prop), + Setoid_Theory Aeq -> Relation_Class. + intros. + apply (@Reflexive _ Aeq). + exact (Seq_refl H). +Defined. -Definition Prop_S : Setoid_Theory Prop iff. -split; [ exact iff_refl | exact iff_sym | exact iff_trans ]. -Qed. +Definition equality_morphism_of_setoid_theory: + forall (A: Type) (Aeq: A -> A -> Prop) (ST: Setoid_Theory Aeq), + let ASetoidClass := relation_class_of_setoid_theory ST in + (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) + Prop_Relation_Class). + intros. + exists Aeq. + pose (sym := Seq_sym ST); clearbody sym. + pose (trans := Seq_trans ST); clearbody trans. + (*CSC: symmetry and transitivity used here *) + unfold make_compatibility_goal; simpl; split; eauto. +Defined. -Add Setoid Prop iff Prop_S. +(* END OF UTILITY/BACKWARD COMPATIBILITY PART *) -Hint Resolve (Seq_refl Prop iff Prop_S): setoid. -Hint Resolve (Seq_sym Prop iff Prop_S): setoid. -Hint Resolve (Seq_trans Prop iff Prop_S): setoid. +(* A FEW EXAMPLES *) -Add Morphism or : or_ext. -intros. -inversion H1. -left. -inversion H. -apply (H3 H2). +Add Morphism iff : Iff_Morphism. + tauto. +Defined. -right. -inversion H0. -apply (H3 H2). -Qed. +(* impl IS A MORPHISM *) -Add Morphism and : and_ext. -intros. -inversion H1. -split. -inversion H. -apply (H4 H2). +Definition impl (A B: Prop) := A -> B. -inversion H0. -apply (H4 H3). -Qed. +Add Morphism impl : Impl_Morphism. +unfold impl; tauto. +Defined. -Add Morphism not : not_ext. -red in |- *; intros. -apply H0. -inversion H. -apply (H3 H1). -Qed. +(* and IS A MORPHISM *) -Definition fleche (A B:Prop) := A -> B. +Add Morphism and : And_Morphism. + tauto. +Defined. -Add Morphism fleche : fleche_ext. -unfold fleche in |- *. -intros. -inversion H0. -inversion H. -apply (H3 (H1 (H6 H2))). -Qed. +(* or IS A MORPHISM *) + +Add Morphism or : Or_Morphism. + tauto. +Defined. + +(* not IS A MORPHISM *) + +Add Morphism not : Not_Morphism. + tauto. +Defined. + +(* FOR BACKWARD COMPATIBILITY *) +Implicit Arguments Setoid_Theory []. +Implicit Arguments Seq_refl []. +Implicit Arguments Seq_sym []. +Implicit Arguments Seq_trans []. |