From ec7717f5e0dd4c295ba1cfd57a0a6a46170490ef Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 9 Jun 2006 14:39:14 +0000 Subject: [PATCH] 1. the default for the default equality/absurd/true/false URIs used to be the Coq ones; now it is None 2. legacy/coq.ma changed to set the default URIs for Coq 3. generation of inversion principles is now branched again --- components/cic/libraryObjects.ml | 40 ++++++++----------- components/cic/libraryObjects.mli | 8 ++-- components/library/librarySync.ml | 2 +- components/tactics/discriminationTactics.ml | 14 +++++-- components/tactics/equalityTactics.ml | 7 +++- components/tactics/inversion.ml | 7 +++- components/tactics/inversion.mli | 1 + components/tactics/inversion_principle.ml | 5 ++- components/tactics/metadataQuery.ml | 23 ++++++----- components/tactics/negationTactics.ml | 15 +++++-- components/tactics/paramodulation/equality.ml | 8 ++-- components/tactics/paramodulation/indexing.ml | 4 +- .../tactics/paramodulation/inference.ml | 4 +- .../tactics/paramodulation/saturation.ml | 8 ++-- components/tactics/paramodulation/utils.ml | 16 +++++--- components/tactics/paramodulation/utils.mli | 1 + matita/library/legacy/coq.ma | 14 +++++++ 17 files changed, 111 insertions(+), 66 deletions(-) diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml index 223b24edd..df653eb9a 100644 --- a/components/cic/libraryObjects.ml +++ b/components/cic/libraryObjects.ml @@ -27,28 +27,17 @@ (**** TABLES ****) -let default_eq_URIs = - [HelmLibraryObjects.Logic.eq_URI, - HelmLibraryObjects.Logic.sym_eq_URI, - HelmLibraryObjects.Logic.trans_eq_URI, - HelmLibraryObjects.Logic.eq_ind_URI, - HelmLibraryObjects.Logic.eq_ind_r_URI];; - -let default_true_URIs = [HelmLibraryObjects.Logic.true_URI] -let default_false_URIs = [HelmLibraryObjects.Logic.false_URI] -let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI] +let default_eq_URIs = [] +let default_true_URIs = [] +let default_false_URIs = [] +let default_absurd_URIs = [] (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *) -let eq_URIs_ref = - ref [HelmLibraryObjects.Logic.eq_URI, - HelmLibraryObjects.Logic.sym_eq_URI, - HelmLibraryObjects.Logic.trans_eq_URI, - HelmLibraryObjects.Logic.eq_ind_URI, - HelmLibraryObjects.Logic.eq_ind_r_URI];; +let eq_URIs_ref = ref default_eq_URIs;; -let true_URIs_ref = ref [HelmLibraryObjects.Logic.true_URI] -let false_URIs_ref = ref [HelmLibraryObjects.Logic.false_URI] -let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI] +let true_URIs_ref = ref default_true_URIs +let false_URIs_ref = ref default_false_URIs +let absurd_URIs_ref = ref default_absurd_URIs (**** SET_DEFAULT ****) @@ -86,7 +75,9 @@ let reset_defaults () = (**** LOOKUP FUNCTIONS ****) -let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq +let eq_URI () = + try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq + with Failure "hd" -> None let is_eq_URI uri = List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref @@ -121,6 +112,9 @@ let eq_ind_r_URI ~eq:uri = let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) -let true_URI () = List.hd !true_URIs_ref -let false_URI () = List.hd !false_URIs_ref -let absurd_URI () = List.hd !absurd_URIs_ref +let true_URI () = + try Some (List.hd !true_URIs_ref) with Failure "hd" -> None +let false_URI () = + try Some (List.hd !false_URIs_ref) with Failure "hd" -> None +let absurd_URI () = + try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli index 1fa0dcc83..7c31bf2bf 100644 --- a/components/cic/libraryObjects.mli +++ b/components/cic/libraryObjects.mli @@ -26,7 +26,7 @@ val set_default : string -> UriManager.uri list -> unit val reset_defaults : unit -> unit -val eq_URI : unit -> UriManager.uri +val eq_URI : unit -> UriManager.uri option val is_eq_URI : UriManager.uri -> bool val is_eq_ind_URI : UriManager.uri -> bool @@ -42,7 +42,7 @@ val trans_eq_URI : eq:UriManager.uri -> UriManager.uri val sym_eq_URI : eq:UriManager.uri -> UriManager.uri -val false_URI : unit -> UriManager.uri -val true_URI : unit -> UriManager.uri -val absurd_URI : unit -> UriManager.uri +val false_URI : unit -> UriManager.uri option +val true_URI : unit -> UriManager.uri option +val absurd_URI : unit -> UriManager.uri option diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index a09baafe1..413cc986c 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -336,7 +336,7 @@ let add_obj refinement_toolkit uri obj = | Cic.InductiveDefinition (_,_,_,attrs) -> uris := !uris @ generate_elimination_principles uri refinement_toolkit; - (* uris := !uris @ generate_inversion refinement_toolkit uri obj; *) + uris := !uris @ generate_inversion refinement_toolkit uri obj; let rec get_record_attrs = function | [] -> None diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index 0ffa2c52b..4c7f5148d 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -206,6 +206,14 @@ let discriminate'_tac ~term = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in + let true_URI = + match LibraryObjects.true_URI () with + Some uri -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in + let false_URI = + match LibraryObjects.false_URI () with + Some uri -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in let find_discriminating_consno t1 t2 = let rec aux t1 t2 = @@ -259,8 +267,8 @@ let discriminate'_tac ~term = C.Lambda (binder, source, (aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd(LibraryObjects.false_URI (),0,[])) - else (C.MutInd(LibraryObjects.true_URI (),0,[])) + then (C.MutInd(false_URI,0,[])) + else (C.MutInd(true_URI,0,[])) in (CicSubstitution.lift 1 (aux red_ty 1))) constructor_list @@ -294,7 +302,7 @@ let discriminate'_tac ~term = let (proof',goals') = ProofEngineTypes.apply_tactic (EliminationTactics.elim_type_tac - (C.MutInd (LibraryObjects.false_URI (), 0, []))) + (C.MutInd (false_URI, 0, []))) status in (match goals' with diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index cca2c1a59..b1727fb7d 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -206,6 +206,11 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = let uri,metasenv,pbo,pty = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in assert (hyps_pat = []); (*CSC: not implemented yet *) + let eq_URI = + match LibraryObjects.eq_URI () with + Some uri -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command")) + in let context_len = List.length context in let subst,metasenv,u,_,selected_terms_with_context = ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph @@ -269,7 +274,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ~start:( P.cut_tac (C.Appl [ - (C.MutInd (LibraryObjects.eq_URI (), 0, [])) ; + (C.MutInd (eq_URI, 0, [])) ; ty_of_with_what ; what ; with_what])) diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml index f5e2a8476..74117f710 100644 --- a/components/tactics/inversion.ml +++ b/components/tactics/inversion.ml @@ -171,6 +171,7 @@ let isSetType paramty = ((Pervasives.compare (get_sort_type paramty) (Cic.Sort Cic.Prop)) != 0) +exception EqualityNotDefinedYet let private_inversion_tac ~term = let module T = CicTypeChecker in let module R = CicReduction in @@ -181,7 +182,11 @@ let private_inversion_tac ~term = (*DEBUG*) debug_print (lazy ("private inversion begins")); let (_,metasenv,_,_) = proof in - let uri_of_eq = LibraryObjects.eq_URI () in + let uri_of_eq = + match LibraryObjects.eq_URI () with + None -> raise EqualityNotDefinedYet + | Some uri -> uri + in let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in let uri = baseuri_of_term termty in diff --git a/components/tactics/inversion.mli b/components/tactics/inversion.mli index 1471f5dbc..2c8b996ff 100644 --- a/components/tactics/inversion.mli +++ b/components/tactics/inversion.mli @@ -24,5 +24,6 @@ *) val isSetType: Cic.term -> bool +exception EqualityNotDefinedYet (* raised by private_inversion_tac only *) val private_inversion_tac: term: Cic.term -> ProofEngineTypes.tactic val inversion_tac: term: Cic.term -> ProofEngineTypes.tactic diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml index b16b133ba..8031e7bbd 100644 --- a/components/tactics/inversion_principle.ml +++ b/components/tactics/inversion_principle.ml @@ -145,7 +145,7 @@ let build_inversion uri obj = if List.length (list_of_prod arity) = (nleft + 1) then None else - begin + try let arity_l = cut_last (list_of_prod arity) in let rightparam_tys = cut_first nleft arity_l in let theorem = build_theorem rightparam_tys arity_l arity cons_list @@ -194,7 +194,8 @@ let build_inversion uri obj = Some (inversor_uri, Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[])) - end + with + Inversion.EqualityNotDefinedYet -> None ;; let init () = ();; diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml index b9c053653..8822c527c 100644 --- a/components/tactics/metadataQuery.ml +++ b/components/tactics/metadataQuery.ml @@ -205,19 +205,22 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = (* match main with *) (* None -> raise Goal_is_not_an_equation *) (* | Some (m,l) -> *) - let m, l = + let l = let eq_URI = - let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in - UriManager.uri_of_string (us ^ "#xpointer(1/1)") + match LibraryObjects.eq_URI () with + None -> None + | Some s -> + Some + (UriManager.uri_of_string + (UriManager.string_of_uri s ^ "#xpointer(1/1)")) in - match main with - | None -> eq_URI, [] - | Some (m, l) when UriManager.eq m eq_URI -> m, l - | Some (m, l) -> eq_URI, [] + match eq_URI,main with + | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l + | _,_ -> [] in Printf.printf "\nSome (m, l): %s, [%s]\n\n" - (UriManager.string_of_uri m) - (String.concat "; " (List.map UriManager.string_of_uri l)); + (UriManager.string_of_uri (List.hd l)) + (String.concat "; " (List.map UriManager.string_of_uri (List.tl l))); (* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *) let set = signature_of_hypothesis context in (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *) @@ -226,7 +229,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *) let set = close_with_constructors set metasenv context in (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *) - let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in + let set = List.fold_right Constr.UriManagerSet.remove l set in let uris = sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in let uris = List.filter nonvar (List.map snd uris) in diff --git a/components/tactics/negationTactics.ml b/components/tactics/negationTactics.ml index 7ee79e534..c973d75f4 100644 --- a/components/tactics/negationTactics.ml +++ b/components/tactics/negationTactics.ml @@ -33,13 +33,18 @@ let absurd_tac ~term = let module P = PrimitiveTactics in let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in + let absurd_URI = + match LibraryObjects.absurd_URI () with + Some uri -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command")) + in let ty_term,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *) then ProofEngineTypes.apply_tactic (P.apply_tac ~term:( - C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ; + C.Appl [(C.Const (absurd_URI, [] )) ; term ; ty]) ) status @@ -55,6 +60,11 @@ let contradiction_tac = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in + let false_URI = + match LibraryObjects.false_URI () with + Some uri -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) + in try ProofEngineTypes.apply_tactic ( T.then_ @@ -62,8 +72,7 @@ let contradiction_tac = ~continuation:( T.then_ ~start: - (EliminationTactics.elim_type_tac - (C.MutInd (LibraryObjects.false_URI (), 0, []))) + (EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, []))) ~continuation: VariousTactics.assumption_tac)) status with diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 3979c0529..3bff5b574 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -737,7 +737,7 @@ let build_goal_proof l initial ty se = let refl_proof ty term = Cic.Appl [Cic.MutConstruct - (LibraryObjects.eq_URI (), 0, 1, []); + (Utils.eq_URI (), 0, 1, []); ty; term] ;; @@ -912,14 +912,14 @@ let meta_convertibility t1 t2 = exception TermIsNotAnEquality;; let term_is_equality term = - let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in + let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in match term with | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true | _ -> false ;; let equality_of_term proof term = - let eq_uri = LibraryObjects.eq_URI () in + let eq_uri = Utils.eq_URI () in let iseq uri = UriManager.eq uri eq_uri in match term with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> @@ -951,7 +951,7 @@ let term_of_equality equality = let argsno = List.length menv in let t = CicSubstitution.lift argsno - (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right]) + (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right]) in snd ( List.fold_right diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 9c5ea281b..e72ed64da 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -583,7 +583,7 @@ let rec demodulation_equality ?from newmeta env table sign target = let name = C.Name "x" in let bo' = let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in - C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); + C.Appl [C.MutInd (Utils.eq_URI (), 0, []); S.lift 1 eq_ty; l; r] in if sign = Utils.Positive then @@ -900,7 +900,7 @@ let superposition_right let bo'' = let l, r = if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); + C.Appl [C.MutInd (Utils.eq_URI (), 0, []); S.lift 1 eq_ty; l; r] in bo', diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index 6a21bb173..91fcee8a2 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -211,7 +211,7 @@ let find_equalities context proof = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let eq_uri = LibraryObjects.eq_URI () in + let eq_uri = Utils.eq_URI () in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let ok_types ty menv = List.for_all (fun (_, _, mt) -> mt = ty) menv @@ -349,7 +349,7 @@ let find_library_equalities dbd context status maxmeta = eqs) in let eq_uri1 = eq_XURI () - and eq_uri2 = LibraryObjects.eq_URI () in + and eq_uri2 = Utils.eq_URI () in let iseq uri = (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2) in diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index a26ec0f73..1282ed27f 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -889,7 +889,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = *) match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] - when UriManager.eq uri (LibraryObjects.eq_URI ()) -> + when UriManager.eq uri (Utils.eq_URI ()) -> (let goal_equation = Equality.mk_equality (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) @@ -946,7 +946,7 @@ let rec given_clause_fullred dbd env goals theorems ~passive active = (* in *) let ok, proof = (* apply_goal_to_theorems dbd env theorems ~passive active goals in *) - let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in + let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in match fst goals with | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_ when left = right && iseq uri -> @@ -1195,7 +1195,7 @@ let given_clause_fullred dbd env goals theorems passive active = (given_clause_fullred dbd env goals theorems passive) active *) -let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ());; +let iseq uri = UriManager.eq uri (Utils.eq_URI ());; let check_if_goal_is_identity env = function | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) @@ -1671,7 +1671,7 @@ let saturate context_hyp @ thms, [] else let refl_equal = - let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + let us = UriManager.string_of_uri (Utils.eq_URI ()) in UriManager.uri_of_string (us ^ "#xpointer(1/1/1)") in let t = CicUtil.term_of_uri refl_equal in diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 072d64f66..c2b1905f8 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -724,14 +724,18 @@ let string_of_pos = function | Right -> "Right" ;; - -let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ()) -let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ()) -let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ()) +let eq_URI () = + match LibraryObjects.eq_URI () with + None -> assert false + | Some uri -> uri + +let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(eq_URI ()) +let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(eq_URI ()) +let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(eq_URI ()) let eq_XURI () = - let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + let s = UriManager.string_of_uri (eq_URI ()) in UriManager.uri_of_string (s ^ "#xpointer(1/1/1)") -let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ()) +let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(eq_URI ()) let metas_of_term t = List.map fst (CicUtil.metas_of_term t) diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli index f44cab460..2f1533e69 100644 --- a/components/tactics/paramodulation/utils.mli +++ b/components/tactics/paramodulation/utils.mli @@ -87,6 +87,7 @@ val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int val debug_print: string Lazy.t -> unit +val eq_URI: unit -> UriManager.uri val eq_ind_URI: unit -> UriManager.uri val eq_ind_r_URI: unit -> UriManager.uri val sym_eq_URI: unit -> UriManager.uri diff --git a/matita/library/legacy/coq.ma b/matita/library/legacy/coq.ma index 76da7d898..e7a5615d9 100644 --- a/matita/library/legacy/coq.ma +++ b/matita/library/legacy/coq.ma @@ -14,6 +14,20 @@ set "baseuri" "cic:/matita/legacy/coq/". +default "equality" + cic:/Coq/Init/Logic/eq.ind + cic:/Coq/Init/Logic/sym_eq.con + cic:/Coq/Init/Logic/trans_eq.con + cic:/Coq/Init/Logic/eq_ind.con + cic:/Coq/Init/Logic/eq_ind_r.con. + +default "true" + cic:/Coq/Init/Logic/True.ind. +default "false" + cic:/Coq/Init/Logic/False.ind. +default "absurd" + cic:/Coq/Init/Logic/absurd.con. + (* aritmetic operators *) interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y). -- 2.39.2