From 3d0c94cd30c5ed2d6d8cb52b3c127ef29d4f3846 Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 6 Oct 2004 15:08:25 +0000 Subject: added transitivity git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6187 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/setoid_replace.ml | 53 ++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 46 insertions(+), 7 deletions(-) (limited to 'tactics/setoid_replace.ml') diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 1646bfa5f..12afbeec5 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -55,6 +55,7 @@ type relation = rel_aeq: constr; rel_refl: constr option; rel_sym: constr option; + rel_trans : constr option; rel_quantifiers_no: int (* it helps unification *) } @@ -111,6 +112,8 @@ 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") @@ -193,6 +196,7 @@ let coq_prop_relation = rel_aeq = gen_constant ["Init"; "Logic"] "iff"; rel_refl = Some (gen_constant ["Init"; "Logic"] "iff_refl"); rel_sym = Some (gen_constant ["Init"; "Logic"] "iff_sym"); + rel_trans = Some (gen_constant ["Init"; "Logic"] "iff_trans"); rel_quantifiers_no = 0 }) @@ -203,6 +207,7 @@ let coq_prop_relation2 = rel_aeq = Lazy.force coq_impl; rel_refl = Some (constant ["Setoid"] "impl_refl"); rel_sym = None; + rel_trans = Some (constant ["Setoid"] "impl_trans"); rel_quantifiers_no = 0 }) @@ -253,16 +258,16 @@ let prmorphism k m = (* 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 a = +let default_relation_for_carrier ?(filter=fun _ -> true) a = let rng = Gmap.rng !relation_table in - match List.filter (fun {rel_a=rel_a} -> rel_a = a) rng with + 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 ppnl (*CSC: still "setoid" in the error message *) - (str "Warning: There are several setoids whose carrier is "++ prterm a ++ - str ". The setoid " ++ prrelation relation ++ + (str "Warning: There are several setoids whose carrier is \""++ prterm a ++ + str "\". The setoid " ++ prrelation relation ++ str " is randomly chosen.") ; Relation relation @@ -297,17 +302,20 @@ let subst_relation subst relation = let rel_aeq' = subst_mps subst relation.rel_aeq in let rel_refl' = option_app (subst_mps subst) relation.rel_refl in let rel_sym' = option_app (subst_mps subst) relation.rel_sym in + let rel_trans' = option_app (subst_mps subst) relation.rel_trans 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 then relation else { rel_a = rel_a' ; rel_aeq = rel_aeq' ; rel_refl = rel_refl' ; - rel_sym = rel_sym' ; + rel_sym = rel_sym'; + rel_trans = rel_trans'; rel_quantifiers_no = relation.rel_quantifiers_no } @@ -410,6 +418,17 @@ let morphism_table_add (m,c) = 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 + ppnl + (str "Warning: There are several morphisms associated to \"" ++ + prterm m ++ str"\". Morphism " ++ prmorphism m m1 ++ + str " 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 @@ -525,6 +544,18 @@ let check_sym env a_quantifiers_rev a aeq sym = errorlabstrm "Add Relation Class" (str "Not a valid proof of symmetry") +let check_trans env a_quantifiers_rev a aeq trans = + if + not + (is_conv env Evd.empty (Typing.type_of env Evd.empty trans) + (Sign.it_mkProd_or_LetIn + (mkApp ((Lazy.force coq_transitive), + [| 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 transitivity") + let check_setoid_theory env a_quantifiers_rev a aeq th = if not @@ -537,24 +568,26 @@ let check_setoid_theory env a_quantifiers_rev a aeq th = errorlabstrm "Add Relation Class" (str "Not a valid proof of symmetry") -let int_add_relation a aeq refl sym = +let int_add_relation 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 ; Lib.add_anonymous_leaf (relation_to_obj (aeq, { rel_a = a; rel_aeq = aeq; rel_refl = refl; rel_sym = sym; + rel_trans = trans; rel_quantifiers_no = List.length a_quantifiers_rev })) (* 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) + (option_app constr_of sym) None (***************** Adding a morphism to the database ****************************) @@ -720,6 +753,7 @@ let apply_to_relation subst rel = rel_aeq = mkApp (rel.rel_aeq, subst) ; rel_refl = option_app (fun c -> mkApp (c,subst)) rel.rel_refl ; rel_sym = option_app (fun c -> mkApp (c,subst)) rel.rel_sym; + rel_trans = option_app (fun c -> mkApp (c,subst)) rel.rel_trans; rel_quantifiers_no = new_quantifiers_no } (* first order matching with a bit of conversion *) @@ -938,11 +972,16 @@ let add_setoid id a aeq th = Sign.it_mkLambda_or_LetIn (mkApp ((Lazy.force coq_seq_sym), [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in + let trans = + Sign.it_mkLambda_or_LetIn + (mkApp ((Lazy.force coq_seq_trans), + [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in let aeq_rel = { rel_a = a ; rel_aeq = aeq ; rel_refl = Some refl ; rel_sym = Some sym ; + rel_trans = Some trans; rel_quantifiers_no = List.length a_quantifiers_rev } in let aeq_rel_class_and_var = None, Relation aeq_rel in Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ; -- cgit v1.2.3