X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fsetoids.ml;h=d85df1c4b1e2de3b215524257ee15d71b2ec9474;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=5729b3ace1ace9af0092ab8161fa6d5d4a22a03e;hpb=d7e33f1609c2d990eb52c3e30784a2aa7bdd9b32;p=helm.git diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml index 5729b3ace..d85df1c4b 100644 --- a/helm/software/components/tactics/setoids.ml +++ b/helm/software/components/tactics/setoids.ml @@ -74,14 +74,14 @@ let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c (*COQ let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s -*) let constant dir s = assert false +*) let constant dir s = Cic.Implicit None (*COQ let gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s -*) let gen_constant dir s = assert false +*) let gen_constant dir s = Cic.Implicit None (*COQ let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s let eval_reference dir s = EvalConstRef (destConst (constant dir s)) -*) let eval_reference dir s = assert false +*) let eval_reference dir s = Cic.Implicit None (*COQ let eval_init_reference dir s = EvalConstRef (destConst (gen_constant ("Init"::dir) s)) *) @@ -91,7 +91,7 @@ let current_constant id = try global_reference id with Not_found -> - anomaly ("Setoid: cannot find " ^ (string_of_id id)) + anomaly ("Setoid: cannot find " ^ id) *) let current_constant id = assert false (* From Setoid.v *) @@ -265,7 +265,7 @@ let find_relation_class rel = (*COQ 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 coq_iff_relation = assert false let coq_impl_relation = assert false +*) let coq_iff_relation = Obj.magic 0 let coq_impl_relation = Obj.magic 0 let relation_morphism_of_constr_morphism = let relation_relation_class_of_constr_relation_class = @@ -288,9 +288,7 @@ let equiv_list () = (* Declare a new type of object in the environment : "relation-theory". *) -(*COQ -let (relation_to_obj, obj_to_relation)= - let cache_set (_,(s, th)) = +let relation_to_obj (s, th) = let th' = if relation_table_mem s then begin @@ -299,8 +297,8 @@ let (relation_to_obj, obj_to_relation)= {th with rel_sym = match th.rel_sym with None -> old_relation.rel_sym - | Some t -> Some t} in -(*COQ + | Some t -> Some t} + in prerr_endline ("Warning: The relation " ^ prrelation th' ^ " is redeclared. The new declaration" ^ @@ -327,22 +325,12 @@ let (relation_to_obj, obj_to_relation)= (if old_relation.rel_refl <> None && old_relation.rel_sym <> None then ")" else "") ^ "."); -*) th' end else th in relation_table_add (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 ********************) @@ -658,18 +646,21 @@ let unify_relation_carrier_with_type env rel t = let argsno = List.length args' - rel.rel_quantifiers_no in let args1 = list_sub args' 0 argsno in let args2 = list_sub args' argsno rel.rel_quantifiers_no in - if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) CicUniv.empty_ugraph) then + if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) + CicUniv.oblivion_ugraph) then args2 else raise_error rel.rel_quantifiers_no | _ -> - if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] rel.rel_a t CicUniv.empty_ugraph) then + if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] + rel.rel_a t CicUniv.oblivion_ugraph) then [] else begin (*COQ let evars,args,instantiated_rel_a = - let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a CicUniv.empty_ugraph in + let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a + CicUniv.oblivion_ugraph in let evd = Evd.create_evar_defs Evd.empty in let evars,args,concl = Clenv.clenv_environments_evars env evd @@ -694,7 +685,7 @@ let unify_relation_carrier_with_type env rel t = let unify_relation_class_carrier_with_type env rel t = match rel with Leibniz (Some t') -> - if fst (CicReduction.are_convertible [] t t' CicUniv.empty_ugraph) then + if fst (CicReduction.are_convertible [] t t' CicUniv.oblivion_ugraph) then rel else raise (ProofEngineTypes.Fail (lazy @@ -901,13 +892,15 @@ let new_named_morphism id m sign = (************************** Adding a relation to the database *********************) +let check_a a = (*COQ -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 +*) assert false -let check_eq env a_quantifiers_rev a aeq = +let check_eq a_quantifiers_rev a aeq = +(*COQ let typ = Sign.it_mkProd_or_LetIn (Cic.Appl [coq_relation ; apply_to_rels a a_quantifiers_rev]) @@ -918,8 +911,10 @@ let check_eq env a_quantifiers_rev a aeq = then raise (ProofEngineTypes.Fail (lazy (CicPp.ppterm aeq ^ " should have type (" ^ CicPp.ppterm typ ^ ")"))) +*) (assert false : unit) -let check_property env a_quantifiers_rev a aeq strprop coq_prop t = +let check_property a_quantifiers_rev a aeq strprop coq_prop t = +(*COQ if not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) @@ -931,23 +926,27 @@ let check_property env a_quantifiers_rev a aeq strprop coq_prop t = then raise (ProofEngineTypes.Fail (lazy ("Not a valid proof of " ^ strprop ^ "."))) +*) assert false -let check_refl env a_quantifiers_rev a aeq refl = - check_property env a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl +let check_refl a_quantifiers_rev a aeq refl = + check_property 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_sym a_quantifiers_rev a aeq sym = + check_property 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_trans a_quantifiers_rev a aeq trans = + check_property a_quantifiers_rev a aeq "transitivity" coq_transitive trans +;; let int_add_relation id a aeq refl sym trans = +(*COQ 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 a_quantifiers_rev = check_a a in + check_eq a_quantifiers_rev a aeq ; + HExtlib.iter_option (check_refl a_quantifiers_rev a aeq) refl ; + HExtlib.iter_option (check_sym a_quantifiers_rev a aeq) sym ; + HExtlib.iter_option (check_trans a_quantifiers_rev a aeq) trans ; let quantifiers_no = List.length a_quantifiers_rev in let aeq_rel = { rel_a = a; @@ -966,18 +965,20 @@ let int_add_relation id a aeq refl sym trans = cic_relation_class_of_X_relation (Cic.Rel 2) (Cic.Rel 1) (apply_to_relation subst aeq_rel) in let _ = +(*COQ Declare.declare_internal_constant id (DefinitionEntry {const_entry_body = Sign.it_mkLambda_or_LetIn x_relation_class - ([ Name (id_of_string "v"),None,Cic.Rel 1; - Name (id_of_string "X"),None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @ + ([ Name "v",None,Cic.Rel 1; + Name "X",None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @ a_quantifiers_rev); const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()}, IsDefinition Definition) in - let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in +*) () in + let id_precise = id ^ "_precise_relation_class" in let xreflexive_relation_class = let subst = let len = List.length a_quantifiers_rev in @@ -985,6 +986,7 @@ let int_add_relation id a aeq refl sym trans = in cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in let _ = +(*COQ Declare.declare_internal_constant id_precise (DefinitionEntry {const_entry_body = @@ -993,16 +995,17 @@ let int_add_relation id a aeq refl sym trans = const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions() }, IsDefinition Definition) in +*) () 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)) ; - Options.if_verbose prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation"); + relation_to_obj (aeq, aeq_rel) ; + prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation"); match trans with None -> () | Some trans -> - let mor_name = id_of_string (string_of_id id ^ "_morphism") in + let mor_name = 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 = @@ -1042,6 +1045,7 @@ let int_add_relation id a aeq refl sym trans = trans_instance], coq_iff_relation in let _ = +(*COQ Declare.declare_internal_constant mor_name (DefinitionEntry {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev; @@ -1049,20 +1053,17 @@ let int_add_relation id a aeq refl sym trans = const_entry_opaque = false; const_entry_boxed = Options.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 = -(*COQ - int_add_relation id (constr_of a) (constr_of aeq) (HExtlib.map_option constr_of refl) - (HExtlib.map_option constr_of sym) (HExtlib.map_option constr_of trans) -*) assert false + int_add_relation id a aeq refl sym trans (****************************** The tactic itself *******************************) @@ -1747,7 +1748,7 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl = let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in (* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels, Rel 1 is now coding for c2, we can build the let-in factorizing c2 *) - Cic.LetIn (Cic.Anonymous,c2,hyp) + Cic.LetIn (Cic.Anonymous,c2,assert false,hyp) in let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in let oppdir = opposite_direction direction in @@ -1816,37 +1817,47 @@ let setoid_replace_in id relation c1 c2 ~new_goals (*COQgl*) = (* [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let setoid_reflexivity (*COQgl*) = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_reflexivity" - [] ((*COQ pf_concl gl*) assert false) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_refl with - None -> - raise (ProofEngineTypes.Fail (lazy - ("The relation " ^ prrelation rel ^ " is not reflexive."))) - | Some refl -> (*COQ apply refl gl*) assert false - with - Optimize -> (*COQ reflexivity gl*) assert false +let setoid_reflexivity_tac = + let tac ((proof,goal) as status) = + let (_,metasenv,_subst,_,_, _) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + try + let relation_class = + relation_class_that_matches_a_constr "Setoid_reflexivity" [] ty in + match relation_class with + Leibniz _ -> assert false (* since [] is empty *) + | Relation rel -> + match rel.rel_refl with + None -> + raise (ProofEngineTypes.Fail (lazy + ("The relation " ^ prrelation rel ^ " is not reflexive."))) + | Some refl -> + ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac refl) + status + with + Optimize -> + ProofEngineTypes.apply_tactic EqualityTactics.reflexivity_tac status + in + ProofEngineTypes.mk_tactic tac -let setoid_symmetry (*COQgl*) = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_symmetry" - [] ((*COQ pf_concl gl*) assert false) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_sym with - None -> - raise (ProofEngineTypes.Fail (lazy - ("The relation " ^ prrelation rel ^ " is not symmetric."))) - | Some sym -> (*COQ apply sym gl*) assert false - with - Optimize -> (*COQ symmetry gl*) assert false +let setoid_symmetry = + let tac status = + try + let relation_class = + relation_class_that_matches_a_constr "Setoid_symmetry" + [] ((*COQ pf_concl gl*) assert false) in + match relation_class with + Leibniz _ -> assert false (* since [] is empty *) + | Relation rel -> + match rel.rel_sym with + None -> + raise (ProofEngineTypes.Fail (lazy + ("The relation " ^ prrelation rel ^ " is not symmetric."))) + | Some sym -> (*COQ apply sym gl*) assert false + with + Optimize -> (*COQ symmetry gl*) assert false + in + ProofEngineTypes.mk_tactic tac let setoid_symmetry_in id (*COQgl*) = (*COQ