From: Stefano Zacchiroli Date: Tue, 28 Jan 2003 10:23:03 +0000 (+0000) Subject: moved tactics from gTopLevel to the new module ocaml/tactics X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=261ccc2ead2f1816d1f0293f7505e04f7a68b5cd;p=helm.git moved tactics from gTopLevel to the new module ocaml/tactics --- diff --git a/helm/ocaml/tactics/.cvsignore b/helm/ocaml/tactics/.cvsignore new file mode 100644 index 000000000..f83e2a8d0 --- /dev/null +++ b/helm/ocaml/tactics/.cvsignore @@ -0,0 +1,7 @@ +*.cmi +*.cma +*.cmo +*.cmx +*.cmxa +*.o +*.a diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend new file mode 100644 index 000000000..7643367bb --- /dev/null +++ b/helm/ocaml/tactics/.depend @@ -0,0 +1,68 @@ +proofEngineHelpers.cmi: proofEngineTypes.cmo +tacticals.cmi: proofEngineTypes.cmo +reductionTactics.cmi: proofEngineTypes.cmo +proofEngineStructuralRules.cmi: proofEngineTypes.cmo +primitiveTactics.cmi: proofEngineTypes.cmo +variousTactics.cmi: proofEngineTypes.cmo +introductionTactics.cmi: proofEngineTypes.cmo +eliminationTactics.cmi: proofEngineTypes.cmo +negationTactics.cmi: proofEngineTypes.cmo +equalityTactics.cmi: proofEngineTypes.cmo +ring.cmi: proofEngineTypes.cmo +fourierR.cmi: proofEngineTypes.cmo +proofEngineReduction.cmo: proofEngineReduction.cmi +proofEngineReduction.cmx: proofEngineReduction.cmi +proofEngineHelpers.cmo: proofEngineHelpers.cmi +proofEngineHelpers.cmx: proofEngineHelpers.cmi +fourier.cmo: fourier.cmi +fourier.cmx: fourier.cmi +tacticals.cmo: proofEngineTypes.cmo tacticals.cmi +tacticals.cmx: proofEngineTypes.cmx tacticals.cmi +reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi +reductionTactics.cmx: proofEngineReduction.cmx reductionTactics.cmi +proofEngineStructuralRules.cmo: proofEngineTypes.cmo \ + proofEngineStructuralRules.cmi +proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ + proofEngineStructuralRules.cmi +primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ + proofEngineTypes.cmo reductionTactics.cmi tacticals.cmi \ + primitiveTactics.cmi +primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ + proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ + primitiveTactics.cmi +variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ + proofEngineTypes.cmo tacticals.cmi variousTactics.cmi +variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ + proofEngineTypes.cmx tacticals.cmx variousTactics.cmi +introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \ + introductionTactics.cmi +introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ + introductionTactics.cmi +eliminationTactics.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ + tacticals.cmi eliminationTactics.cmi +eliminationTactics.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ + tacticals.cmx eliminationTactics.cmi +negationTactics.cmo: eliminationTactics.cmi primitiveTactics.cmi \ + proofEngineTypes.cmo tacticals.cmi variousTactics.cmi negationTactics.cmi +negationTactics.cmx: eliminationTactics.cmx primitiveTactics.cmx \ + proofEngineTypes.cmx tacticals.cmx variousTactics.cmx negationTactics.cmi +equalityTactics.cmo: introductionTactics.cmi primitiveTactics.cmi \ + proofEngineHelpers.cmi proofEngineReduction.cmi \ + proofEngineStructuralRules.cmi proofEngineTypes.cmo reductionTactics.cmi \ + tacticals.cmi equalityTactics.cmi +equalityTactics.cmx: introductionTactics.cmx primitiveTactics.cmx \ + proofEngineHelpers.cmx proofEngineReduction.cmx \ + proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \ + tacticals.cmx equalityTactics.cmi +ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \ + proofEngineStructuralRules.cmi proofEngineTypes.cmo tacticals.cmi \ + ring.cmi +ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \ + proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \ + ring.cmi +fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ + proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \ + tacticals.cmi fourierR.cmi +fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ + proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ + tacticals.cmx fourierR.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile new file mode 100644 index 000000000..285c8ed18 --- /dev/null +++ b/helm/ocaml/tactics/Makefile @@ -0,0 +1,19 @@ +PACKAGE = tactics +REQUIRES = helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification + +INTERFACE_FILES = \ + proofEngineReduction.mli proofEngineHelpers.mli \ + tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ + primitiveTactics.mli variousTactics.mli introductionTactics.mli \ + eliminationTactics.mli negationTactics.mli equalityTactics.mli ring.mli \ + fourierR.mli +IMPLEMENTATION_FILES = \ + proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml \ + fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml \ + primitiveTactics.ml variousTactics.ml introductionTactics.ml \ + eliminationTactics.ml negationTactics.ml equalityTactics.ml ring.ml \ + fourierR.ml + + +include ../Makefile.common + diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml new file mode 100644 index 000000000..fc6906cbc --- /dev/null +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -0,0 +1,220 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* +let induction_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + let module U = UriManager in + let (_,metasenv,_,_) = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *) + + T.then_ ~start:(T.repeat_tactic + ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *) + ~continuation:(P.intros)) + ~continuation:(P.elim_intros_simpl ~term) + ~status +;; +*) + + +let elim_type_tac ~term ~status = + let module C = Cic in + let module P = PrimitiveTactics in + let module T = Tacticals in + T.thens + ~start: (P.cut_tac ~term) + ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ] + ~status +;; + +(* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-) +let elim_type_tac ~term ~status = + warn "in Ring.elim_type_tac"; + Tacticals.thens ~start:(cut_tac ~term) + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status +*) + + +(* PROVE DI DECOMPOSE *) +(* guardare quali sono i tipi induttivi decomponibili presenti in +profondita' nel term; chiamare una funzione di call-back passando questa +lista e ritornando la lista di termini che l'utente vuole decomporre; +decomporre. *) + + +exception InteractiveUserUriChoiceNotRegistered + +let interactive_user_uri_choice = + (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) : + (selection_mode:[`SINGLE | `EXTENDED] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> string list -> string list) ref) +;; + +exception IllFormedUri of string + +let cic_textual_parser_uri_of_string uri' = + try + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then + CicTextualParser0.ConUri (UriManager.uri_of_string uri') + else + if String.sub uri' (String.length uri' - 4) 4 = ".var" then + CicTextualParser0.VarUri (UriManager.uri_of_string uri') + else + (try + (* Inductive Type *) + let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in + CicTextualParser0.IndTyUri (uri'',typeno) + with + _ -> + (* Constructor of an Inductive Type *) + let uri'',typeno,consno = + CicTextualLexer.indconuri_of_uri uri' + in + CicTextualParser0.IndConUri (uri'',typeno,consno) + ) + with + _ -> raise (IllFormedUri uri') +;; + +let constructor_uri_of_string uri = + match cic_textual_parser_uri_of_string uri with + CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) + | _ -> assert false +;; + +let call_back uris = +(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) + let module U = UriManager in + List.map + (constructor_uri_of_string) + (!interactive_user_uri_choice + ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false + ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" + (List.map + (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)) + uris) + ) +;; + + +let decompose_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + let _,metasenv,_,_ = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let old_context_len = List.length context in +(* let nr_of_hyp_still_to_elim = ref 1 in *) + let termty = CicTypeChecker.type_of_aux' metasenv context term in + + let rec make_list termty = +(* altamente inefficente? *) + let rec search_inductive_types urilist termty = + (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) + match termty with + (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> + (uri,typeno,exp_named_subst)::urilist + | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> + (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist) + | _ -> urilist + (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *) + in + let rec purge_duplicates urilist = + let rec aux triple urilist = + match urilist with + [] -> [] + | hd::tl -> + if (hd = triple) + then aux triple tl + else hd::(aux triple tl) + in + match urilist with + [] -> [] + | hd::tl -> hd::(purge_duplicates (aux hd tl)) + in + purge_duplicates (search_inductive_types [] termty) + in + + let urilist = + (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *) + (* N.B.: due to a bug in call_back exp_named_subst are not significant (they all are []) *) + call_back (make_list termty) in + + let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) = +prerr_endline ("%%%%%%% nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)); + if nr_of_hyp_still_to_elim <> 0 then + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let old_context_len = List.length context in + let termty = CicTypeChecker.type_of_aux' metasenv context term' in +prerr_endline ("%%%%%%% elim_clear termty= " ^ CicPp.ppterm termty); + match termty with + C.MutInd (uri,typeno,exp_named_subst) + | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) + when (List.mem (uri,typeno,exp_named_subst) urilist) -> +prerr_endline ("%%%%%%% elim " ^ CicPp.ppterm termty); + T.then_ + ~start:(P.elim_intros_simpl_tac ~term:term') + ~continuation:( + (* clear the hyp that has just been eliminated *) + (fun ~status:((proof,goal) as status) -> + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let new_context_len = List.length context in +prerr_endline ("%%%%%%% newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); + let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in + T.then_ + ~start:( + if (term'==term) (* this is the first application of elim: there's no need to clear the hyp *) + then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end + else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end) + ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim) + ~status + )) + ~status + | _ -> + let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in +prerr_endline ("%%%%%%% fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)); + elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status + else (* raise (ProofEngineTypes.Fail "Decomopse: finished decomposing"); *) T.id_tac ~status + + in +(* T.repeat_tactic ~tactic: *) + (elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1) + ~status +;; + + + diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli new file mode 100644 index 000000000..a49c77158 --- /dev/null +++ b/helm/ocaml/tactics/eliminationTactics.mli @@ -0,0 +1,33 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic + +val interactive_user_uri_choice: ( selection_mode:[`SINGLE | `EXTENDED] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> string list -> string list) ref + +val decompose_tac: term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml new file mode 100644 index 000000000..79b5b1dbe --- /dev/null +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -0,0 +1,238 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[]) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[]) + in + eqT_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) +;; + + +let rewrite_simpl_tac ~term ~status = + Tacticals.then_ + ~start:(rewrite_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status +;; + + +let rewrite_back_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[]) + in + eq_ind_r,ty,t2,t1 + | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[]) + in + eqT_ind_r,ty,t2,t1 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) + +;; + + +let rewrite_back_simpl_tac ~term ~status = + Tacticals.then_ + ~start:(rewrite_back_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status +;; + + +let replace_tac ~what ~with_what ~status:((proof, goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let wty = CicTypeChecker.type_of_aux' metasenv context what in + try + if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what)) + then T.thens + ~start:( + P.cut_tac + ~term:( + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *) + wty ; + what ; + with_what])) + ~continuations:[ + T.then_ + ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *) + ~continuation:( + ProofEngineStructuralRules.clear + ~hyp:(List.hd context)) ; +(* (Some(C.Name "dummy_for_replace" , C.Def (CicTypeChecker.type_of_aux' metasenv context (C.Rel 1)) (* NOOOO!!!!! tipo di dummy *) )))) ; *) + T.id_tac] + ~status + else raise (ProofEngineTypes.Fail "Replace: terms not replaceable") + with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context") +;; + + +(* All these tacs do is applying the right constructor/theorem *) + +let reflexivity_tac = + IntroductionTactics.constructor_tac ~n:1 +;; + + +let symmetry_tac ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", [])) + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", [])) + + | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") +;; + + +let transitivity_tac ~term ~status:((proof, goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let module T = Tacticals in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + T.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", []))) + ~continuations: + [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac] + ~status + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + T.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", []))) + ~continuations: + [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term] + ~status + + | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") +;; + + diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli new file mode 100644 index 000000000..7d57a0c11 --- /dev/null +++ b/helm/ocaml/tactics/equalityTactics.mli @@ -0,0 +1,35 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic + +val reflexivity_tac: ProofEngineTypes.tactic +val symmetry_tac: ProofEngineTypes.tactic +val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic + diff --git a/helm/ocaml/tactics/fourier.ml b/helm/ocaml/tactics/fourier.ml new file mode 100644 index 000000000..d7728c0b3 --- /dev/null +++ b/helm/ocaml/tactics/fourier.ml @@ -0,0 +1,244 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* match ie.coef with + [] -> raise (Failure "empty ineq") + |(c::r) -> if rinf c r0 + then pop ie lneg + else if rinf r0 c then pop ie lpos + else pop ie lnul) + s; + [!lneg;!lnul;!lpos] +;; +(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): +(add_hist [(equation 1, s1);...;(équation n, sn)]) += +[{équation 1, [1;0;...;0], s1}; + {équation 2, [0;1;...;0], s2}; + ... + {équation n, [0;0;...;1], sn}] +*) +let add_hist le = + let n = List.length le in + let i=ref 0 in + List.map (fun (ie,s) -> + let h =ref [] in + for k=1 to (n-(!i)-1) do pop r0 h; done; + pop r1 h; + for k=1 to !i do pop r0 h; done; + i:=!i+1; + {coef=ie;hist=(!h);strict=s}) + le +;; +(* additionne deux inéquations *) +let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef; + hist=List.map2 rplus ie1.hist ie2.hist; + strict=ie1.strict || ie2.strict} +;; +(* multiplication d'une inéquation par un rationnel (positif) *) +let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef; + hist=List.map (fun x -> rmult a x) ie.hist; + strict= ie.strict} +;; +(* on enlève le premier coefficient *) +let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict} +;; +(* le premier coefficient: "tête" de l'inéquation *) +let hd_coef ie = List.hd ie.coef +;; + +(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. +*) +let deduce_add lneg lpos = + let res=ref [] in + List.iter (fun i1 -> + List.iter (fun i2 -> + let a = rop (hd_coef i1) in + let b = hd_coef i2 in + pop (ie_tl (ie_add (ie_emult b i1) + (ie_emult a i2))) res) + lpos) + lneg; + !res +;; +(* élimination de la première variable à partir d'une liste d'inéquations: +opération qu'on itère dans l'algorithme de Fourier. +*) +let deduce1 s i= + match (partitionne s) with + [lneg;lnul;lpos] -> + let lnew = deduce_add lneg lpos in + (match lneg with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->(); + match lpos with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->()); + (List.map ie_tl lnul)@lnew + |_->assert false +;; +(* algorithme de Fourier: on élimine successivement toutes les variables. +*) +let deduce lie = + let n = List.length (fst (List.hd lie)) in + let lie=ref (add_hist lie) in + for i=1 to n-1 do + lie:= deduce1 !lie i; + done; + !lie +;; + +(* donne [] si le système a des find solutions, +sinon donne [c,s,lc] +où lc est la combinaison linéaire des inéquations de départ +qui donne 0 < c si s=true + ou 0 <= c sinon +cette inéquation étant absurde. +*) +(** Tryes to find if the system admits solutions. + @param lie the list of inequations + @return a list that can be empty if the system has solutions. Otherwise it returns a + one elements list [\[(c,s,lc)\]]. {b c} is the rational that can be obtained solving the system, + {b s} is true if the inequation that proves that the system is absurd is of type [c < 0], false if + [c <= 0], {b lc} is a list of rational that represents the liear combination to obtain the + absurd inequation *) +let unsolvable lie = + let lr = deduce lie in + let res = ref [] in + (try (List.iter (fun e -> + match e with + {coef=[c];hist=lc;strict=s} -> + if (rinf c r0 && (not s)) || (rinfeq c r0 && s) + then (res := [c,s,lc]; + raise (Failure "contradiction found")) + |_->assert false) + lr) + with _ -> ()); + !res +;; + +(* Exemples: + +let test1=[[r1;r1;r0],true;[rop r1;r1;r1],false;[r0;rop r1;rop r1],false];; +deduce test1;; +unsolvable test1;; + +let test2=[ +[r1;r1;r0;r0;r0],false; +[r0;r1;r1;r0;r0],false; +[r0;r0;r1;r1;r0],false; +[r0;r0;r0;r1;r1],false; +[r1;r0;r0;r0;r1],false; +[rop r1;rop r1;r0;r0;r0],false; +[r0;rop r1;rop r1;r0;r0],false; +[r0;r0;rop r1;rop r1;r0],false; +[r0;r0;r0;rop r1;rop r1],false; +[rop r1;r0;r0;r0;rop r1],false +];; +deduce test2;; +unsolvable test2;; + +*) diff --git a/helm/ocaml/tactics/fourier.mli b/helm/ocaml/tactics/fourier.mli new file mode 100644 index 000000000..8b26bc21a --- /dev/null +++ b/helm/ocaml/tactics/fourier.mli @@ -0,0 +1,27 @@ +type rational = { num : int; den : int; } +val print_rational : rational -> unit +val pgcd : int -> int -> int +val r0 : rational +val r1 : rational +val rnorm : rational -> rational +val rop : rational -> rational +val rplus : rational -> rational -> rational +val rminus : rational -> rational -> rational +val rmult : rational -> rational -> rational +val rinv : rational -> rational +val rdiv : rational -> rational -> rational +val rinf : rational -> rational -> bool +val rinfeq : rational -> rational -> bool +type ineq = { coef : rational list; hist : rational list; strict : bool; } +val pop : 'a -> 'a list ref -> unit +val partitionne : ineq list -> ineq list list +val add_hist : (rational list * bool) list -> ineq list +val ie_add : ineq -> ineq -> ineq +val ie_emult : rational -> ineq -> ineq +val ie_tl : ineq -> ineq +val hd_coef : ineq -> rational +val deduce_add : ineq list -> ineq list -> ineq list +val deduce1 : ineq list -> int -> ineq list +val deduce : (rational list * bool) list -> ineq list +val unsolvable : + (rational list * bool) list -> (rational * bool * rational list) list diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml new file mode 100644 index 000000000..370b5db50 --- /dev/null +++ b/helm/ocaml/tactics/fourierR.ml @@ -0,0 +1,1297 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +(******************** OTHER USEFUL TACTICS **********************) +(* Galla: moved in variousTactics.ml + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[]) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[]) + in + eqT_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) +;; + + +let rewrite_simpl_tac ~term ~status = + Tacticals.then_ ~start:(rewrite_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status +;; +*) + +(******************** THE FOURIER TACTIC ***********************) + +(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients +des inéquations et équations sont entiers. En attendant la tactique Field. +*) + +open Fourier + + +let debug x = print_string ("____ "^x) ; flush stdout;; + +let debug_pcontext x = + let str = ref "" in + List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^ + a ^ " " | _ ->()) x ; + debug ("contesto : "^ (!str) ^ "\n") +;; + +(****************************************************************************** +Operations on linear combinations. + +Opérations sur les combinaisons linéaires affines. +La partie homogène d'une combinaison linéaire est en fait une table de hash +qui donne le coefficient d'un terme du calcul des constructions, +qui est zéro si le terme n'y est pas. +*) + + + +(** + The type for linear combinations +*) +type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational} +;; + +(** + @return an empty flin +*) +let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0} +;; + +(** + @param f a flin + @param x a Cic.term + @return the rational associated with x (coefficient) +*) +let flin_coef f x = + try + (Hashtbl.find f.fhom x) + with + _ -> r0 +;; + +(** + Adds c to the coefficient of x + @param f a flin + @param x a Cic.term + @param c a rational + @return the new flin +*) +let flin_add f x c = + match x with + Cic.Rel(n) ->( + let cx = flin_coef f x in + Hashtbl.remove f.fhom x; + Hashtbl.add f.fhom x (rplus cx c); + f) + |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n"); + let cx = flin_coef f x in + Hashtbl.remove f.fhom x; + Hashtbl.add f.fhom x (rplus cx c); + f +;; +(** + Adds c to f.fcste + @param f a flin + @param c a rational + @return the new flin +*) +let flin_add_cste f c = + {fhom=f.fhom; + fcste=rplus f.fcste c} +;; + +(** + @return a empty flin with r1 in fcste +*) +let flin_one () = flin_add_cste (flin_zero()) r1;; + +(** + Adds two flin +*) +let flin_plus f1 f2 = + let f3 = flin_zero() in + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; + flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste; +;; + +(** + Substracts two flin +*) +let flin_minus f1 f2 = + let f3 = flin_zero() in + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; + flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste); +;; + +(** + @return a times f +*) +let flin_emult a f = + let f2 = flin_zero() in + Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; + flin_add_cste f2 (rmult a f.fcste); +;; + + +(*****************************************************************************) + + +(** + @param t a term + @raise Failure if conversion is impossible + @return rational proiection of t +*) +let rec rational_of_term t = + (* fun to apply f to the first and second rational-term of l *) + let rat_of_binop f l = + let a = List.hd l and + b = List.hd(List.tl l) in + f (rational_of_term a) (rational_of_term b) + in + (* as before, but f is unary *) + let rat_of_unop f l = + f (rational_of_term (List.hd l)) + in + match t with + | Cic.Cast (t1,t2) -> (rational_of_term t1) + | Cic.Appl (t1::next) -> + (match t1 with + Cic.Const (u,boh) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> + rat_of_unop rop next + |"cic:/Coq/Reals/Rdefinitions/Rinv.con" -> + rat_of_unop rinv next + |"cic:/Coq/Reals/Rdefinitions/Rmult.con" -> + rat_of_binop rmult next + |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" -> + rat_of_binop rdiv next + |"cic:/Coq/Reals/Rdefinitions/Rplus.con" -> + rat_of_binop rplus next + |"cic:/Coq/Reals/Rdefinitions/Rminus.con" -> + rat_of_binop rminus next + | _ -> failwith "not a rational") + | _ -> failwith "not a rational") + | Cic.Const (u,boh) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1 + |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0 + | _ -> failwith "not a rational") + | _ -> failwith "not a rational" +;; + +(* coq wrapper +let rational_of_const = rational_of_term;; +*) +let fails f a = + try + let tmp = (f a) in + false + with + _-> true + ;; + +let rec flin_of_term t = + let fl_of_binop f l = + let a = List.hd l and + b = List.hd(List.tl l) in + f (flin_of_term a) (flin_of_term b) + in + try( + match t with + | Cic.Cast (t1,t2) -> (flin_of_term t1) + | Cic.Appl (t1::next) -> + begin + match t1 with + Cic.Const (u,boh) -> + begin + match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> + flin_emult (rop r1) (flin_of_term (List.hd next)) + |"cic:/Coq/Reals/Rdefinitions/Rplus.con"-> + fl_of_binop flin_plus next + |"cic:/Coq/Reals/Rdefinitions/Rminus.con"-> + fl_of_binop flin_minus next + |"cic:/Coq/Reals/Rdefinitions/Rmult.con"-> + begin + let arg1 = (List.hd next) and + arg2 = (List.hd(List.tl next)) + in + if fails rational_of_term arg1 + then + if fails rational_of_term arg2 + then + ( (* prodotto tra 2 incognite ????? impossibile*) + failwith "Sistemi lineari!!!!\n" + ) + else + ( + match arg1 with + Cic.Rel(n) -> (*trasformo al volo*) + (flin_add (flin_zero()) arg1 (rational_of_term arg2)) + |_-> (* test this *) + let tmp = flin_of_term arg1 in + flin_emult (rational_of_term arg2) (tmp) + ) + else + if fails rational_of_term arg2 + then + ( + match arg2 with + Cic.Rel(n) -> (*trasformo al volo*) + (flin_add (flin_zero()) arg2 (rational_of_term arg1)) + |_-> (* test this *) + let tmp = flin_of_term arg2 in + flin_emult (rational_of_term arg1) (tmp) + + ) + else + ( (*prodotto tra razionali*) + (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2))) + ) + (*try + begin + (*let a = rational_of_term arg1 in + debug("ho fatto rational of term di "^CicPp.ppterm arg1^ + " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*) + let a = flin_of_term arg1 + try + begin + let b = (rational_of_term arg2) in + debug("ho fatto rational of term di "^CicPp.ppterm arg2^ + " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n"); + (flin_add_cste (flin_zero()) (rmult a b)) + end + with + _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n"); + (flin_add (flin_zero()) arg2 a) + end + with + _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n"); + (flin_add(flin_zero()) arg1 (rational_of_term arg2)) + *) + end + |"cic:/Coq/Reals/Rdefinitions/Rinv.con"-> + let a=(rational_of_term (List.hd next)) in + flin_add_cste (flin_zero()) (rinv a) + |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"-> + begin + let b=(rational_of_term (List.hd(List.tl next))) in + try + begin + let a = (rational_of_term (List.hd next)) in + (flin_add_cste (flin_zero()) (rdiv a b)) + end + with + _-> (flin_add (flin_zero()) (List.hd next) (rinv b)) + end + |_->assert false + end + |_ -> assert false + end + | Cic.Const (u,boh) -> + begin + match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one () + |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero () + |_-> assert false + end + |_-> assert false) + with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1 +;; + +(* coq wrapper +let flin_of_constr = flin_of_term;; +*) + +(** + Translates a flin to (c,x) list + @param f a flin + @return something like (c1,x1)::(c2,x2)::...::(cn,xn) +*) +let flin_to_alist f = + let res=ref [] in + Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f; + !res +;; + +(* Représentation des hypothèses qui sont des inéquations ou des équations. +*) + +(** + The structure for ineq +*) +type hineq={hname:Cic.term; (* le nom de l'hypothèse *) + htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) + hleft:Cic.term; + hright:Cic.term; + hflin:flin; + hstrict:bool} +;; + +(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 +*) + +let ineq1_of_term (h,t) = + match t with (* match t *) + Cic.Appl (t1::next) -> + let arg1= List.hd next in + let arg2= List.hd(List.tl next) in + (match t1 with (* match t1 *) + Cic.Const (u,boh) -> + (match UriManager.string_of_uri u with (* match u *) + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> + [{hname=h; + htype="Rlt"; + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); + hstrict=true}] + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> + [{hname=h; + htype="Rgt"; + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); + hstrict=true}] + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> + [{hname=h; + htype="Rle"; + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); + hstrict=false}] + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> + [{hname=h; + htype="Rge"; + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); + hstrict=false}] + |_->assert false)(* match u *) + | Cic.MutInd (u,i,o) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Init/Logic_Type/eqT.ind" -> + let t0= arg1 in + let arg1= arg2 in + let arg2= List.hd(List.tl (List.tl next)) in + (match t0 with + Cic.Const (u,boh) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/R.con"-> + [{hname=h; + htype="eqTLR"; + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); + hstrict=false}; + {hname=h; + htype="eqTRL"; + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); + hstrict=false}] + |_-> assert false) + |_-> assert false) + |_-> assert false) + |_-> assert false)(* match t1 *) + |_-> assert false (* match t *) +;; +(* coq wrapper +let ineq1_of_constr = ineq1_of_term;; +*) + +(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) +*) + +let rec print_rl l = + match l with + []-> () + | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next +;; + +let rec print_sys l = + match l with + [] -> () + | (a,b)::next -> (print_rl a; + print_string (if b=true then "strict\n"else"\n"); + print_sys next) + ;; + +(*let print_hash h = + Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h +;;*) + +let fourier_lineq lineq1 = + let nvar=ref (-1) in + let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *) + List.iter (fun f -> + Hashtbl.iter (fun x c -> + try (Hashtbl.find hvar x;()) + with _-> nvar:=(!nvar)+1; + Hashtbl.add hvar x (!nvar); + debug("aggiungo una var "^ + string_of_int !nvar^" per "^ + CicPp.ppterm x^"\n")) + f.hflin.fhom) + lineq1; + (*print_hash hvar;*) + debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n"); + let sys= List.map (fun h-> + let v=Array.create ((!nvar)+1) r0 in + Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c) + h.hflin.fhom; + ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) + lineq1 in + debug ("chiamo unsolvable sul sistema di "^ + string_of_int (List.length sys) ^"\n"); + print_sys sys; + unsolvable sys +;; + +(***************************************************************************** +Construction de la preuve en cas de succès de la méthode de Fourier, +i.e. on obtient une contradiction. +*) + + +let _eqT = Cic.MutInd((UriManager.uri_of_string + "cic:/Coq/Init/Logic_Type/eqT.ind"), 0, []) ;; +let _False = Cic.MutInd ((UriManager.uri_of_string + "cic:/Coq/Init/Logic/False.ind"), 0, []) ;; +let _not = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Init/Logic/not.con"), []);; +let _R0 = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R0.con"), []) ;; +let _R1 = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R1.con"), []) ;; +let _R = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R.con"), []) ;; +let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;; +let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;; +let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;; +let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;; +let _Rfourier_le=Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;; +let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;; +let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;; +let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;; +let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;; +let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;; +let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;; +let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;; +let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;; +let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;; +let _Rinv = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rinv.con"), []) ;; +let _Rinv_R1 = Cic.Const((UriManager.uri_of_string + "cic:/Coq/Reals/Rbase/Rinv_R1.con" ), []) ;; +let _Rle = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rle.con"), []) ;; +let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;; +let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;; +let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;; +let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;; +(*let _Rle_zero_zero = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con"), []) ;;*) +let _Rlt = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rlt.con"), []) ;; +let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;; +let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;; +let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;; +let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;; +let _Rminus = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rminus.con"), []) ;; +let _Rmult = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rmult.con"), []) ;; +let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;; +let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;; +let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;; +let _Ropp = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Ropp.con"), []) ;; +let _Rplus = Cic.Const ((UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rplus.con"), []) ;; + +(******************************************************************************) + +let is_int x = (x.den)=1 +;; + +(* fraction = couple (num,den) *) +let rec rational_to_fraction x= (x.num,x.den) +;; + +(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) +*) + +let rec int_to_real_aux n = + match n with + 0 -> _R0 (* o forse R0 + R0 ????? *) + | 1 -> _R1 + | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ] +;; + + +let int_to_real n = + let x = int_to_real_aux (abs n) in + if n < 0 then + Cic.Appl [ _Ropp ; x ] + else + x +;; + + +(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) +*) + +let rational_to_real x = + let (n,d)=rational_to_fraction x in + Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ] +;; + +(* preuve que 0 m=goal) metasenv in + debug ("th = "^ CicPp.ppterm t ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + in + let tacn=ref + (fun ~status -> pall "n0" ~status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + let tacd=ref + (fun ~status -> pall "d0" ~status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + + + for i=1 to n-1 do + tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) + ~status _Rlt_zero_pos_plus1; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) + ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" + ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); + done; + + + +debug("TAC ZERO INF POS\n"); + +(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) + ~continuations:[ + !tacn ; + !tacd ] + ~status) +;; + + + +(* preuve que 0<=n*1/d +*) + +let tac_zero_infeq_pos gl (n,d) ~status = + (*let cste = pf_parse_constr gl in*) + debug("inizio tac_zero_infeq_pos\n"); + let tacn = ref + (*(if n=0 then + (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) + else*) + (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) + (* ) *) + in + let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in + for i=1 to n-1 do + tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); + done; + let r = + (Tacticals.thens ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in + debug("fine tac_zero_infeq_pos\n"); + r +;; + + + +(* preuve que 0<(-n)*(1/d) => False +*) + +let tac_zero_inf_false gl (n,d) ~status= + debug("inizio tac_zero_inf_false\n"); + if n=0 then + (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in + debug("fine\n"); + r) + else + (debug "2\n";let r = (Tacticals.then_ ~start:( + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " + ^ CicPp.ppterm ty ^"\n"); + let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in + debug("!!!!!!!!!2\n"); + r + ) + ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in + debug("fine\n"); + r + ) +;; + +(* preuve que 0<=n*(1/d) => False ; n est negatif +*) + +let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= +debug("stat tac_zero_infeq_false\n"); +let r = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + + debug("faccio fold di " ^ CicPp.ppterm + (Cic.Appl + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] + ] + ) ^ "\n") ; + debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); + (*CSC: Patch to undo the over-simplification of RewriteSimpl *) + Tacticals.then_ + ~start: + (ReductionTactics.fold_tac ~reduction:CicReduction.whd + ~also_in_hypotheses:false + ~term: + (Cic.Appl + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] + ] + ) + ) + ~continuation: + (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) + ~continuation:(tac_zero_inf_pos (-n,d))) ~status in + debug("end tac_zero_infeq_false\n"); + r +(*PORTING + Tacticals.id_tac ~status +*) +;; + + +(* *********** ********** ******** ??????????????? *********** **************) + +let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,t)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + PrimitiveTactics.apply_tac + (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*) + ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *) + ~status:(proof',goal) + in + proof'',fresh_meta::goals +;; + + + + + +let my_cut ~term:c ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + +debug("my_cut di "^CicPp.ppterm c^"\n"); + + + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,c)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, + CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] + ~status:(proof',goal) + in + (* We permute the generated goals to be consistent with Coq *) + match goals with + [] -> assert false + | he::tl -> proof'',he::fresh_meta::tl +;; + + +let exact = PrimitiveTactics.exact_tac;; + +let tac_use h ~status:(proof,goal as status) = +debug("Inizio TC_USE\n"); +let curi,metasenv,pbo,pty = proof in +let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); +debug ("ty = "^ CicPp.ppterm ty^"\n"); + +let res = +match h.htype with + "Rlt" -> exact ~term:h.hname ~status + |"Rle" -> exact ~term:h.hname ~status + |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_gt_to_lt) + ~continuation:(exact ~term:h.hname)) ~status + |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_ge_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_eqLR_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_eqRL_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |_->assert false +in +debug("Fine TAC_USE\n"); +res +;; + + + +let is_ineq (h,t) = + match t with + Cic.Appl ( Cic.Const(u,boh)::next) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true + |"cic:/Coq/Init/Logic_Type/eqT.con" -> + (match (List.hd next) with + Cic.Const (uri,_) when + UriManager.string_of_uri uri = + "cic:/Coq/Reals/Rdefinitions/R.con" -> true + | _ -> false) + |_->false) + |_->false +;; + +let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; + +let mkAppL a = + Cic.Appl(Array.to_list a) +;; + +(* Résolution d'inéquations linéaires dans R *) +let rec strip_outer_cast c = match c with + | Cic.Cast (c,_) -> strip_outer_cast c + | _ -> c +;; + +(*let find_in_context id context = + let rec find_in_context_aux c n = + match c with + [] -> failwith (id^" not found in context") + | a::next -> (match a with + Some (Cic.Name(name),_) when name = id -> n + (*? magari al posto di _ qualcosaltro?*) + | _ -> find_in_context_aux next (n+1)) + in + find_in_context_aux context 1 +;; + +(* mi sembra quadratico *) +let rec filter_real_hyp context cont = + match context with + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> ( + let n = find_in_context h cont in + debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n"); + [(Cic.Rel(n),t)] @ filter_real_hyp next cont) + | a::next -> debug(" no\n"); filter_real_hyp next cont +;;*) +let filter_real_hyp context _ = + let rec filter_aux context num = + match context with + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> + ( + (*let n = find_in_context h cont in*) + debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); + [(Cic.Rel(num),t)] @ filter_aux next (num+1) + ) + | a::next -> filter_aux next (num+1) + in + filter_aux context 1 +;; + + +(* lifts everithing at the conclusion level *) +let rec superlift c n= + match c with + [] -> [] + | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl( + CicSubstitution.lift n a))] @ superlift next (n+1) + | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def( + CicSubstitution.lift n a))] @ superlift next (n+1) + | _::next -> superlift next (n+1) (*?? ??*) + +;; + +let equality_replace a b ~status = +debug("inizio EQ\n"); + let module C = Cic in + let proof,goal = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in +debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); + let (proof,goals) = + EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) + ~status:((curi,metasenv',pbo,pty),goal) + in + let new_goals = fresh_meta::goals in +debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " + ^string_of_int( List.length goals)^"+ meta\n"); + (proof,new_goals) +;; + +let tcl_fail a ~status:(proof,goal) = + match a with + 1 -> raise (ProofEngineTypes.Fail "fail-tactical") + |_-> (proof,[goal]) +;; + +(* Galla: moved in variousTactics.ml +let assumption_tac ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let num = ref 0 in + let tac_list = List.map + ( fun x -> num := !num + 1; + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) + ) + context + in + Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) +;; +*) +(* Galla: moved in negationTactics.ml +(* !!!!! fix !!!!!!!!!! *) +let contradiction_tac ~status:(proof,goal)= + Tacticals.then_ + (*inutile sia questo che quello prima della chiamata*) + ~start:PrimitiveTactics.intros_tac + ~continuation:(Tacticals.then_ + ~start:(VariousTactics.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) +;; +*) + +(* ********************* TATTICA ******************************** *) + +let rec fourier ~status:(s_proof,s_goal)= + let s_curi,s_metasenv,s_pbo,s_pty = s_proof in + let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) + s_metasenv in + + debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); + debug_pcontext s_context; + + let fhyp = String.copy "new_hyp_for_fourier" in + +(* here we need to negate the thesis, but to do this we need to apply the right +theoreme,so let's parse our thesis *) + + let th_to_appl = ref _Rfourier_not_le_gt in + (match s_ty with + Cic.Appl ( Cic.Const(u,boh)::args) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := + _Rfourier_not_ge_lt + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := + _Rfourier_not_gt_le + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := + _Rfourier_not_le_gt + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := + _Rfourier_not_lt_ge + |_-> failwith "fourier can't be applyed") + |_-> failwith "fourier can't be applyed"); + (* fix maybe strip_outer_cast goes here?? *) + + (* now let's change our thesis applying the th and put it with hp *) + + let proof,gl = + Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) + ~continuation:PrimitiveTactics.intros_tac + ~status:(s_proof,s_goal) in + let goal = if List.length gl = 1 then List.hd gl + else failwith "a new goal" in + + debug ("port la tesi sopra e la nego. contesto :\n"); + debug_pcontext s_context; + + (* now we have all the right environment *) + + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + + + (* now we want to convert hp to inequations, but first we must lift + everyting to thesis level, so that a variable has the save Rel(n) + in each hp ( needed by ineq1_of_term ) *) + + (* ? fix if None ?????*) + (* fix change superlift with a real name *) + + let l_context = superlift context 1 in + let hyps = filter_real_hyp l_context l_context in + + debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n"); + + let lineq =ref [] in + + (* transform hyps into inequations *) + + List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) + with _-> ()) + hyps; + + + debug ("applico fourier a "^ string_of_int (List.length !lineq)^ + " disequazioni\n"); + + let res=fourier_lineq (!lineq) in + let tac=ref Tacticals.id_tac in + if res=[] then + (print_string "Tactic Fourier fails.\n";flush stdout; + failwith "fourier_tac fails") + else + ( + match res with (*match res*) + [(cres,sres,lc)]-> + + (* in lc we have the coefficient to "reduce" the system *) + + print_string "Fourier's method can prove the goal...\n";flush stdout; + + debug "I coeff di moltiplicazione rit sono: "; + + let lutil=ref [] in + List.iter + (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil); + (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *)) + ) + (List.combine (!lineq) lc); + + print_string (" quindi lutil e' lunga "^ + string_of_int (List.length (!lutil))^"\n"); + + (* on construit la combinaison linéaire des inéquation *) + + (match (!lutil) with (*match (!lutil) *) + (h1,c1)::lutil -> + debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n"; + + let s=ref (h1.hstrict) in + + + let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in + let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in + + List.iter (fun (h,c) -> + s:=(!s)||(h.hstrict); + t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl + [_Rmult;rational_to_real c;h.hleft ] ]); + t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl + [_Rmult;rational_to_real c;h.hright] ])) + lutil; + + let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in + let tc=rational_to_real cres in + + +(* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *) + + debug "inizio a costruire tac1\n"; + Fourier.print_rational(c1); + + let tac1=ref ( fun ~status -> + if h1.hstrict then + (Tacticals.thens + ~start:( + fun ~status -> + debug ("inizio t1 strict\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find + (function (m,_,_) -> m=goal) metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) + ~continuations:[tac_use h1;tac_zero_inf_pos + (rational_to_fraction c1)] + ~status + ) + else + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) + ~continuations:[tac_use h1;tac_zero_inf_pos + (rational_to_fraction c1)] ~status + ) + ) + + in + s:=h1.hstrict; + List.iter (fun (h,c) -> + (if (!s) then + (if h.hstrict then + (debug("tac1 1\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_lt_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (debug("tac1 2\n"); + Fourier.print_rational(c1); + tac1:=(Tacticals.thens + ~start:( + fun ~status -> + debug("INIZIO TAC 1 2\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) + metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + ) + else + (if h.hstrict then + (debug("tac1 3\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (debug("tac1 4\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + ) + ); + s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) + + let tac2 = + if sres then + tac_zero_inf_false goal (rational_to_fraction cres) + else + tac_zero_infeq_false goal (rational_to_fraction cres) + in + tac:=(Tacticals.thens + ~start:(my_cut ~term:ineq) + ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ + ~start:(fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) + metasenv in + PrimitiveTactics.change_tac ~what:ty + ~with_what:(Cic.Appl [ _not; ineq]) ~status) + ~continuation:(Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term: + (if sres then _Rnot_lt_lt else _Rnot_le_le)) + ~continuation:(Tacticals.thens + ~start:( + fun ~status -> + debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); + let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc + ~status + in + (match r with (p,gl) -> + debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations:[(Tacticals.thens + ~start:( + fun ~status -> + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in + (match r with (p,gl) -> + debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations: + [PrimitiveTactics.apply_tac ~term:_Rinv_R1 + ;Tacticals.try_tactics + ~tactics:[ "ring", (fun ~status -> + debug("begin RING\n"); + let r = Ring.ring_tac ~status in + debug ("end RING\n"); + r) + ; "id", Tacticals.id_tac] + ]) + ;(*Tacticals.id_tac*) + Tacticals.then_ + ~start: + ( + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m= + goal) metasenv in + (* check if ty is of type *) + let w1 = + debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); + (match ty with + Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) + |_ -> assert false) + in + let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in + debug("fine MY_CHNGE\n"); + r + + ) + ~continuation:(*PORTINGTacticals.id_tac*)tac2])) + ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) + + |_-> assert false)(*match (!lutil) *) + |_-> assert false); (*match res*) + debug ("finalmente applico tac\n"); + ( + let r = !tac ~status:(proof,goal) in + debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r + + ) +;; + +let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; + + diff --git a/helm/ocaml/tactics/fourierR.mli b/helm/ocaml/tactics/fourierR.mli new file mode 100644 index 000000000..e5790ec0f --- /dev/null +++ b/helm/ocaml/tactics/fourierR.mli @@ -0,0 +1,5 @@ +(* +val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +*) +val fourier_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml new file mode 100644 index 000000000..bc28c4170 --- /dev/null +++ b/helm/ocaml/tactics/introductionTactics.ml @@ -0,0 +1,59 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let constructor_tac ~n ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.MutInd (uri, typeno, exp_named_subst)) + | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) -> + PrimitiveTactics.apply_tac ~status:(proof, goal) + ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) + | _ -> raise (ProofEngineTypes.Fail "Constructor: failed") +;; + + +let exists_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let split_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let left_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let right_tac ~status = + constructor_tac ~n:2 ~status +;; + diff --git a/helm/ocaml/tactics/introductionTactics.mli b/helm/ocaml/tactics/introductionTactics.mli new file mode 100644 index 000000000..c3a12720b --- /dev/null +++ b/helm/ocaml/tactics/introductionTactics.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val constructor_tac: n:int -> ProofEngineTypes.tactic + +val exists_tac: ProofEngineTypes.tactic +val split_tac: ProofEngineTypes.tactic +val left_tac: ProofEngineTypes.tactic +val right_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml new file mode 100644 index 000000000..28e5ceeb5 --- /dev/null +++ b/helm/ocaml/tactics/negationTactics.ml @@ -0,0 +1,73 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let absurd_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let _,metasenv,_,_ = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *) + then P.apply_tac + ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status + else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") +;; + + +let contradiction_tac ~status = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + try + T.then_ + ~start: P.intros_tac + ~continuation:( + T.then_ + ~start: + (EliminationTactics.elim_type_tac + ~term: + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"), 0, []))) + ~continuation: VariousTactics.assumption_tac) + ~status + with + (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption") + (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *) +;; + +(* Questa era in fourierR.ml +(* !!!!! fix !!!!!!!!!! *) +let contradiction_tac ~status:(proof,goal)= + Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) + ~continuation:(Tacticals.then_ + ~start:(VariousTactics.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) +;; +*) + + diff --git a/helm/ocaml/tactics/negationTactics.mli b/helm/ocaml/tactics/negationTactics.mli new file mode 100644 index 000000000..bfa3e8d5d --- /dev/null +++ b/helm/ocaml/tactics/negationTactics.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val absurd_tac: term:Cic.term -> ProofEngineTypes.tactic +val contradiction_tac: ProofEngineTypes.tactic + diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml new file mode 100644 index 000000000..ccd8ccfe0 --- /dev/null +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -0,0 +1,548 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open ProofEngineHelpers +open ProofEngineTypes + +exception NotAnInductiveTypeToEliminate +exception NotTheRightEliminatorShape +exception NoHypothesesFound +exception WrongUriToVariable of string + +(* lambda_abstract newmeta ty *) +(* returns a triple [bo],[context],[ty'] where *) +(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) +(* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *) +(* So, lambda_abstract is the core of the implementation of *) +(* the Intros tactic. *) +let lambda_abstract context newmeta ty mknames = + let module C = Cic in + let rec collect_context context = + function + C.Cast (te,_) -> collect_context context te + | C.Prod (n,s,t) -> + let n' = C.Name (mknames n) in + let (context',ty,bo) = + collect_context ((Some (n',(C.Decl s)))::context) t + in + (context',ty,C.Lambda(n',s,bo)) + | C.LetIn (n,s,t) -> + let (context',ty,bo) = + collect_context ((Some (n,(C.Def s)))::context) t + in + (context',ty,C.LetIn(n,s,bo)) + | _ as t -> + let irl = identity_relocation_list_for_metavariable context in + context, t, (C.Meta (newmeta,irl)) + in + collect_context context ty + +let eta_expand metasenv context t arg = + let module T = CicTypeChecker in + let module S = CicSubstitution in + let module C = Cic in + let rec aux n = + function + t' when t' = S.lift n arg -> C.Rel (1 + n) + | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.Var (uri,exp_named_subst') + | C.Meta _ + | C.Sort _ + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) + | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) + | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) + | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) + | C.Appl l -> C.Appl (List.map (aux n) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = aux_exp_named_subst n exp_named_subst in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,aux n outt, aux n t, + List.map (aux n) pl) + | C.Fix (i,fl) -> + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) + fl + in + C.CoFix (i, substitutedfl) + and aux_exp_named_subst n = + List.map (function uri,t -> uri,aux n t) + in + let argty = + T.type_of_aux' metasenv context arg + in + (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) + +(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) +let classify_metas newmeta in_subst_domain subst_in metasenv = + List.fold_right + (fun (i,canonical_context,ty) (old_uninst,new_uninst) -> + if in_subst_domain i then + old_uninst,new_uninst + else + let ty' = subst_in canonical_context ty in + let canonical_context' = + List.fold_right + (fun entry canonical_context' -> + let entry' = + match entry with + Some (n,Cic.Decl s) -> + Some (n,Cic.Decl (subst_in canonical_context' s)) + | Some (n,Cic.Def s) -> + Some (n,Cic.Def (subst_in canonical_context' s)) + | None -> None + in + entry'::canonical_context' + ) canonical_context [] + in + if i < newmeta then + ((i,canonical_context',ty')::old_uninst),new_uninst + else + old_uninst,((i,canonical_context',ty')::new_uninst) + ) metasenv ([],[]) + +(* Auxiliary function for apply: given a type (a backbone), it returns its *) +(* head, a META environment in which there is new a META for each hypothesis,*) +(* a list of arguments for the new applications and the indexes of the first *) +(* and last new METAs introduced. The nth argument in the list of arguments *) +(* is just the nth new META. *) +let new_metasenv_for_apply newmeta proof context ty = + let module C = Cic in + let module S = CicSubstitution in + let rec aux newmeta = + function + C.Cast (he,_) -> aux newmeta he + | C.Prod (name,s,t) -> + let irl = identity_relocation_list_for_metavariable context in + let newargument = C.Meta (newmeta,irl) in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 1) (S.subst newargument t) + in + res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta + | t -> t,[],[],newmeta + in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in + res,newmetasenv,arguments,lastmeta + +(* Useful only inside apply_tac *) +let + generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst += + let module C = Cic in + let params = + match CicEnvironment.get_obj uri with + C.Constant (_,_,_,params) + | C.CurrentProof (_,_,_,_,params) + | C.Variable (_,_,_,params) + | C.InductiveDefinition (_,params,_) -> params + in + let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'= + let next_fresh_meta = ref newmeta in + let newmetasenvfragment = ref [] in + let exp_named_subst_diff = ref [] in + let rec aux = + function + [],[] -> [] + | uri::tl,[] -> + let ty = + match CicEnvironment.get_obj uri with + C.Variable (_,_,ty,_) -> + CicSubstitution.subst_vars !exp_named_subst_diff ty + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + in + let irl = identity_relocation_list_for_metavariable context in + let subst_item = uri,C.Meta (!next_fresh_meta,irl) in + newmetasenvfragment := + (!next_fresh_meta,context,ty)::!newmetasenvfragment ; + exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ; + incr next_fresh_meta ; + subst_item::(aux (tl,[])) + | uri::tl1,((uri',_) as s)::tl2 -> + assert (UriManager.eq uri uri') ; + s::(aux (tl1,tl2)) + | [],_ -> assert false + in + let exp_named_subst' = aux (params,exp_named_subst) in + !exp_named_subst_diff,!next_fresh_meta, + List.rev !newmetasenvfragment, exp_named_subst' + in +prerr_endline ("@@@ " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst)) ^ " |--> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst'))) ; + new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff +;; + +let apply_tac ~term ~status:(proof, goal) = + (* Assumption: The term "term" must be closed in the current context *) + let module T = CicTypeChecker in + let module R = CicReduction in + let module C = Cic in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let newmeta = new_meta ~proof in + let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = + match term with + C.Var (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Var (uri,exp_named_subst') + | C.Const (uri,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = + generalize_exp_named_subst_with_fresh_metas context newmeta uri + exp_named_subst + in + exp_named_subst_diff,newmeta',newmetasenvfragment, + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | _ -> [],newmeta,[],term + in + let metasenv' = metasenv@newmetasenvfragment in +prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ; + let termty = + CicSubstitution.subst_vars exp_named_subst_diff + (CicTypeChecker.type_of_aux' metasenv' context term) + in +prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ; + (* newmeta is the lowest index of the new metas introduced *) + let (consthead,newmetas,arguments,_) = + new_metasenv_for_apply newmeta' proof context termty + in + let newmetasenv = metasenv'@newmetas in + let subst,newmetasenv' = + CicUnification.fo_unif newmetasenv context consthead ty + in + let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in + let apply_subst = CicUnification.apply_subst subst in + let old_uninstantiatedmetas,new_uninstantiatedmetas = + (* subst_in doesn't need the context. Hence the underscore. *) + let subst_in _ = CicUnification.apply_subst subst in + classify_metas newmeta in_subst_domain subst_in newmetasenv' + in + let bo' = + apply_subst + (if List.length newmetas = 0 then + term' + else + Cic.Appl (term'::arguments) + ) + in +prerr_endline ("XXXX " ^ CicPp.ppterm (if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments)) ^ " |>>> " ^ CicPp.ppterm bo') ; + let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in + let (newproof, newmetasenv''') = + let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in + subst_meta_and_metasenv_in_proof + proof metano subst_in newmetasenv'' + in + (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas) + + (* TODO per implementare i tatticali e' necessario che tutte le tattiche + sollevino _solamente_ Fail *) +let apply_tac ~term ~status = + try + apply_tac ~term ~status + (* TODO cacciare anche altre eccezioni? *) + with CicUnification.UnificationFailed as e -> + raise (Fail (Printexc.to_string e)) + +let intros_tac ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let newmeta = new_meta ~proof in + let (context',ty',bo') = + lambda_abstract context newmeta ty (ProofEngineHelpers.fresh_name) + in + let (newproof, _) = + subst_meta_in_proof proof metano bo' [newmeta,context',ty'] + in + (newproof, [newmeta]) + +let cut_tac ~term ~status:(proof, goal) = + let module C = Cic in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let newmeta1 = new_meta ~proof in + let newmeta2 = newmeta1 + 1 in + let context_for_newmeta1 = + (Some (C.Name "dummy_for_cut",C.Decl term))::context in + let irl1 = + identity_relocation_list_for_metavariable context_for_newmeta1 in + let irl2 = identity_relocation_list_for_metavariable context in + let newmeta1ty = CicSubstitution.lift 1 ty in + let bo' = + C.Appl + [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ; + C.Meta (newmeta2,irl2)] + in + let (newproof, _) = + subst_meta_in_proof proof metano bo' + [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; + in + (newproof, [newmeta1 ; newmeta2]) + +let letin_tac ~term ~status:(proof, goal) = + let module C = Cic in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let _ = CicTypeChecker.type_of_aux' metasenv context term in + let newmeta = new_meta ~proof in + let context_for_newmeta = + (Some (C.Name "dummy_for_letin",C.Def term))::context in + let irl = + identity_relocation_list_for_metavariable context_for_newmeta in + let newmetaty = CicSubstitution.lift 1 ty in + let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in + let (newproof, _) = + subst_meta_in_proof + proof metano bo'[newmeta,context_for_newmeta,newmetaty] + in + (newproof, [newmeta]) + + (** functional part of the "exact" tactic *) +let exact_tac ~term ~status:(proof, goal) = + (* Assumption: the term bo must be closed in the current context *) + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let module T = CicTypeChecker in + let module R = CicReduction in + if R.are_convertible context (T.type_of_aux' metasenv context term) ty then + begin + let (newproof, metasenv') = + subst_meta_in_proof proof metano term [] in + (newproof, []) + end + else + raise (Fail "The type of the provided term is not the one expected.") + + +(* not really "primitive" tactics .... *) + +let elim_tac ~term ~status:(proof, goal) = + let module T = CicTypeChecker in + let module U = UriManager in + let module R = CicReduction in + let module C = Cic in + let (curi,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let termty = T.type_of_aux' metasenv context term in + let uri,exp_named_subst,typeno,args = + match termty with + C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) + | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> + (uri,exp_named_subst,typeno,args) + | _ -> raise NotAnInductiveTypeToEliminate + in + let eliminator_uri = + let buri = U.buri_of_uri uri in + let name = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tys,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + | _ -> assert false + in + let ext = + match T.type_of_aux' metasenv context ty with + C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.Type -> "_rect" + | _ -> assert false + in + U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") + in + let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in + let ety = T.type_of_aux' metasenv context eliminator_ref in + let newmeta = new_meta ~proof in + let (econclusion,newmetas,arguments,lastmeta) = + new_metasenv_for_apply newmeta proof context ety + in + (* Here we assume that we have only one inductive hypothesis to *) + (* eliminate and that it is the last hypothesis of the theorem. *) + (* A better approach would be fingering the hypotheses in some *) + (* way. *) + let meta_of_corpse = + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas + in + let irl = + identity_relocation_list_for_metavariable canonical_context + in + Cic.Meta (lastmeta - 1, irl) + in + let newmetasenv = newmetas @ metasenv in + let subst1,newmetasenv' = + CicUnification.fo_unif newmetasenv context term meta_of_corpse + in + let ueconclusion = CicUnification.apply_subst subst1 econclusion in + (* The conclusion of our elimination principle is *) + (* (?i farg1 ... fargn) *) + (* The conclusion of our goal is ty. So, we can *) + (* eta-expand ty w.r.t. farg1 .... fargn to get *) + (* a new ty equal to (P farg1 ... fargn). Now *) + (* ?i can be instantiated with P and we are ready *) + (* to refine the term. *) + let emeta, fargs = + match ueconclusion with + C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs + | C.Meta (emeta,_) -> emeta,[] + | _ -> raise NotTheRightEliminatorShape + in + let ty' = CicUnification.apply_subst subst1 ty in + let eta_expanded_ty = +(*CSC: newmetasenv' era metasenv ??????????? *) + List.fold_left (eta_expand newmetasenv' context) ty' fargs + in + let subst2,newmetasenv'' = +(*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite +da subst1!!!! Dovrei rimuoverle o sono innocue?*) + CicUnification.fo_unif + newmetasenv' context ueconclusion eta_expanded_ty + in + let in_subst_domain i = + let eq_to_i = function (j,_) -> i=j in + List.exists eq_to_i subst1 || + List.exists eq_to_i subst2 + in + (* When unwinding the META that corresponds to the elimination *) + (* predicate (which is emeta), we must also perform one-step *) + (* beta-reduction. apply_subst doesn't need the context. Hence *) + (* the underscore. *) + let apply_subst _ t = + let t' = CicUnification.apply_subst subst1 t in + CicUnification.apply_subst_reducing + subst2 (Some (emeta,List.length fargs)) t' + in + let old_uninstantiatedmetas,new_uninstantiatedmetas = + classify_metas newmeta in_subst_domain apply_subst + newmetasenv'' + in + let arguments' = List.map (apply_subst context) arguments in + let bo' = Cic.Appl (eliminator_ref::arguments') in + let newmetasenv''' = + new_uninstantiatedmetas@old_uninstantiatedmetas + in + let (newproof, newmetasenv'''') = + (* When unwinding the META that corresponds to the *) + (* elimination predicate (which is emeta), we must *) + (* also perform one-step beta-reduction. *) + (* The only difference w.r.t. apply_subst is that *) + (* we also substitute metano with bo'. *) + (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) + (*CSC: no? *) + let apply_subst' t = + let t' = CicUnification.apply_subst subst1 t in + CicUnification.apply_subst_reducing + ((metano,bo')::subst2) + (Some (emeta,List.length fargs)) t' + in + subst_meta_and_metasenv_in_proof + proof metano apply_subst' newmetasenv''' + in + (newproof, + List.map (function (i,_,_) -> i) new_uninstantiatedmetas) +;; + +(* The simplification is performed only on the conclusion *) +let elim_intros_simpl_tac ~term = + Tacticals.then_ ~start:(elim_tac ~term) + ~continuation: + (Tacticals.thens + ~start:intros_tac + ~continuations: + [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None]) +;; + +exception NotConvertible + +(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal, *) +(*CSC: while [what] can have a richer context (because of binders) *) +(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *) +(*CSC: Is that evident? Is that right? Or should it be changed? *) +let change_tac ~what ~with_what ~status:(proof, goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + (* are_convertible works only on well-typed terms *) + ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ; + if CicReduction.are_convertible context what with_what then + begin + let replace = + ProofEngineReduction.replace ~equality:(==) ~what ~with_what + in + let ty' = replace ty in + let context' = + List.map + (function + Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t)) + | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) + | None -> None + ) context + in + let metasenv' = + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [metano] + end + else + raise (ProofEngineTypes.Fail "Not convertible") diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli new file mode 100644 index 000000000..dad385339 --- /dev/null +++ b/helm/ocaml/tactics/primitiveTactics.mli @@ -0,0 +1,41 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val apply_tac: + term: Cic.term -> ProofEngineTypes.tactic +val exact_tac: + term: Cic.term -> ProofEngineTypes.tactic +val intros_tac: + ProofEngineTypes.tactic +val cut_tac: + term: Cic.term -> ProofEngineTypes.tactic +val letin_tac: + term: Cic.term -> ProofEngineTypes.tactic + +val elim_intros_simpl_tac: + term: Cic.term -> ProofEngineTypes.tactic + +val change_tac: + what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml new file mode 100644 index 000000000..74b6fcdac --- /dev/null +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -0,0 +1,122 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*CSC: generatore di nomi? Chiedere il nome? *) +let fresh_name = + let next_fresh_index = ref 0 in + function + Cic.Anonymous -> + incr next_fresh_index ; + "fresh_name" ^ string_of_int !next_fresh_index + | Cic.Name name -> + incr next_fresh_index ; + name ^ string_of_int !next_fresh_index + +(* identity_relocation_list_for_metavariable i canonical_context *) +(* returns the identity relocation list, which is the list [1 ; ... ; n] *) +(* where n = List.length [canonical_context] *) +(*CSC: ma mi basta la lunghezza del contesto canonico!!!*) +let identity_relocation_list_for_metavariable canonical_context = + let canonical_context_length = List.length canonical_context in + let rec aux = + function + (_,[]) -> [] + | (n,None::tl) -> None::(aux ((n+1),tl)) + | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) + in + aux (1,canonical_context) + +(* Returns the first meta whose number is above the *) +(* number of the higher meta. *) +let new_meta ~proof = + let (_,metasenv,_,_) = proof in + let rec aux = + function + None,[] -> 1 + | Some n,[] -> n + | None,(n,_,_)::tl -> aux (Some n,tl) + | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) + in + 1 + aux (None,metasenv) + +let subst_meta_in_proof proof meta term newmetasenv = + let uri,metasenv,bo,ty = proof in + let subst_in = CicUnification.apply_subst [meta,term] in + let metasenv' = + newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) + in + let metasenv'' = + List.map + (function i,canonical_context,ty -> + let canonical_context' = + List.map + (function + Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) + | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s)) + | None -> None + ) canonical_context + in + i,canonical_context',(subst_in ty) + ) metasenv' + in + let bo' = subst_in bo in + let newproof = uri,metasenv'',bo',ty in + (newproof, metasenv'') + +(*CSC: commento vecchio *) +(* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *) +(* This (heavy) function must be called when a tactic can instantiate old *) +(* metavariables (i.e. existential variables). It substitues the metasenv *) +(* of the proof with the result of removing [meta] from the domain of *) +(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *) +(* in the current proof. Finally it applies [apply_subst_replacing] to *) +(* current proof. *) +(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *) +(*CSC: ci ripasso sopra apply_subst!!! *) +(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *) +(*CSC: [newmetasenv]. *) +let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = + let (uri,_,bo,ty) = proof in + let bo' = subst_in bo in + let metasenv' = + List.fold_right + (fun metasenv_entry i -> + match metasenv_entry with + (m,canonical_context,ty) when m <> meta -> + let canonical_context' = + List.map + (function + None -> None + | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) + | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t)) + ) canonical_context + in + (m,canonical_context',subst_in ty)::i + | _ -> i + ) newmetasenv [] + in + let newproof = uri,metasenv',bo',ty in + (newproof, metasenv') + diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli new file mode 100644 index 000000000..de0b37596 --- /dev/null +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -0,0 +1,45 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val fresh_name : Cic.name -> string + +(* identity_relocation_list_for_metavariable i canonical_context *) +(* returns the identity relocation list, which is the list [1 ; ... ; n] *) +(* where n = List.length [canonical_context] *) +val identity_relocation_list_for_metavariable : + 'a option list -> Cic.term option list + +(* Returns the first meta whose number is above the *) +(* number of the higher meta. *) +val new_meta : proof:ProofEngineTypes.proof -> int + +val subst_meta_in_proof : + ProofEngineTypes.proof -> + int -> Cic.term -> Cic.metasenv -> + ProofEngineTypes.proof * Cic.metasenv +val subst_meta_and_metasenv_in_proof : + ProofEngineTypes.proof -> + int -> (Cic.term -> Cic.term) -> Cic.metasenv -> + ProofEngineTypes.proof * Cic.metasenv diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml new file mode 100644 index 000000000..710a48164 --- /dev/null +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -0,0 +1,826 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 12/04/2002 *) +(* *) +(* *) +(******************************************************************************) + + +(* The code of this module is derived from the code of CicReduction *) + +exception Impossible of int;; +exception ReferenceToConstant;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; +exception WrongUriToInductiveDefinition;; +exception WrongUriToConstant;; +exception RelToHiddenHypothesis;; + +let alpha_equivalence = + let module C = Cic in + let rec aux t t' = + if t = t' then true + else + match t,t' with + C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) -> + UriManager.eq uri1 uri2 && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.Cast (te,ty), C.Cast (te',ty') -> + aux te te' && aux ty ty' + | C.Prod (_,s,t), C.Prod (_,s',t') -> + aux s s' && aux t t' + | C.Lambda (_,s,t), C.Lambda (_,s',t') -> + aux s s' && aux t t' + | C.LetIn (_,s,t), C.LetIn(_,s',t') -> + aux s s' && aux t t' + | C.Appl l, C.Appl l' -> + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true l l' + with + Invalid_argument _ -> false) + | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) -> + UriManager.eq uri uri' && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) -> + UriManager.eq uri uri' && i = i' && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.MutConstruct (uri,i,j,exp_named_subst1), + C.MutConstruct (uri',i',j',exp_named_subst2) -> + UriManager.eq uri uri' && i = i' && j = j' && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> + UriManager.eq sp sp' && i = i' && + aux outt outt' && aux t t' && + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true pl pl' + with + Invalid_argument _ -> false) + | C.Fix (i,fl), C.Fix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (_,i,ty,bo) (_,i',ty',bo') -> + b && i = i' && aux ty ty' && aux bo bo' + ) true fl fl' + with + Invalid_argument _ -> false) + | C.CoFix (i,fl), C.CoFix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (_,ty,bo) (_,ty',bo') -> + b && aux ty ty' && aux bo bo' + ) true fl fl' + with + Invalid_argument _ -> false) + | _,_ -> false (* we already know that t != t' *) + and aux_exp_named_subst exp_named_subst1 exp_named_subst2 = + try + List.fold_left2 + (fun b (uri1,t1) (uri2,t2) -> + b && UriManager.eq uri1 uri2 && aux t1 t2 + ) true exp_named_subst1 exp_named_subst2 + with + Invalid_argument _ -> false + in + aux +;; + +(* "textual" replacement of a subterm with another one *) +let replace ~equality ~what ~with_what ~where = + let module C = Cic in + let rec aux = + function + t when (equality t what) -> with_what + | C.Rel _ as t -> t + | C.Var (uri,exp_named_subst) -> + C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux te, aux ty) + | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) + | C.Appl l -> + (* Invariant enforced: no application of an application *) + (match List.map aux l with + (C.Appl l')::tl -> C.Appl (l'@tl) + | l' -> C.Appl l') + | C.Const (uri,exp_named_subst) -> + C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.MutInd (uri,i,exp_named_subst) -> + C.MutInd + (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.MutConstruct (uri,i,j,exp_named_subst) -> + C.MutConstruct + (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,aux outt, aux t,List.map aux pl) + | C.Fix (i,fl) -> + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux ty, aux bo)) + fl + in + C.CoFix (i, substitutedfl) + in + aux where +;; + +(* replaces in a term a term with another one. *) +(* Lifting are performed as usual. *) +let replace_lifting ~equality ~what ~with_what ~where = + let rec substaux k what = + let module C = Cic in + let module S = CicSubstitution in + function + t when (equality t what) -> S.lift (k-1) with_what + | C.Rel n as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k what t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty) + | C.Prod (n,s,t) -> + C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.Lambda (n,s,t) -> + C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.LetIn (n,s,t) -> + C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k what) tl in + begin + match substaux k what he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst + in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,substaux k what outt, substaux k what t, + List.map (substaux k what) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> + (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> + (name, substaux k what ty, substaux (k+len) (S.lift len what) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + substaux 1 what where +;; + +(* replaces in a term a term with another one. *) +(* Lifting are performed as usual. *) +let replace_lifting_csc nnn ~equality ~what ~with_what ~where = + let rec substaux k = + let module C = Cic in + let module S = CicSubstitution in + function + t when (equality t what) -> S.lift (k-1) with_what + | C.Rel n as t -> + if n < k then C.Rel n else C.Rel (n + nnn) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) + | C.Prod (n,s,t) -> + C.Prod (n, substaux k s, substaux (k + 1) t) + | C.Lambda (n,s,t) -> + C.Lambda (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,t) -> + C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k) tl in + begin + match substaux k he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,substaux k outt, substaux k t, + List.map (substaux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> + (name, i, substaux k ty, substaux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> + (name, substaux k ty, substaux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in +let res = + substaux 1 where +in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res +;; + +(* Takes a well-typed term and fully reduces it. *) +(*CSC: It does not perform reduction in a Case *) +let reduce context = + let rec reduceaux context l = + let module C = Cic in + let module S = CicSubstitution in + function + C.Rel n as t -> + (match List.nth context (n-1) with + Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) + | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) + | None -> raise RelToHiddenHypothesis + ) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + (match CicEnvironment.get_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | C.Variable (_,None,_,_) -> + let t' = C.Var (uri,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.Variable (_,Some body,_,_) -> + (reduceaux context l + (CicSubstitution.subst_vars exp_named_subst' body)) + ) + | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) + | C.Sort _ as t -> t (* l should be empty *) + | C.Implicit as t -> t + | C.Cast (te,ty) -> + C.Cast (reduceaux context l te, reduceaux context l ty) + | C.Prod (name,s,t) -> + assert (l = []) ; + C.Prod (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | C.Lambda (name,s,t) -> + (match l with + [] -> + C.Lambda (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | he::tl -> reduceaux context tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.LetIn (n,s,t) -> + reduceaux context l (S.subst (reduceaux context [] s) t) + | C.Appl (he::tl) -> + let tl' = List.map (reduceaux context []) tl in + reduceaux context (tl'@l) he + | C.Appl [] -> raise (Impossible 1) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + (match CicEnvironment.get_obj uri with + C.Constant (_,Some body,_,_) -> + (reduceaux context l + (CicSubstitution.subst_vars exp_named_subst' body)) + | C.Constant (_,None,_,_) -> + let t' = C.Const (uri,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_,_) -> + (reduceaux context l + (CicSubstitution.subst_vars exp_named_subst' body)) + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + let t' = C.MutInd (uri,i,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.MutConstruct (uri,i,j,exp_named_subst) as t -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + let t' = C.MutConstruct (uri,i,j,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.MutCase (mutind,i,outtype,term,pl) -> + let decofix = + function + C.CoFix (i,fl) as t -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + reduceaux context [] body' + | C.Appl (C.CoFix (i,fl) :: tl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + let tl' = List.map (reduceaux context []) tl in + reduceaux context tl' body' + | t -> t + in + (match decofix (reduceaux context [] term) with + C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) + | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> + let (arity, r) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,_,r) -> + let (_,_,arity,_) = List.nth tl i in + (arity,r) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (r,tl) + in + reduceaux context (ts@l) (List.nth pl (j-1)) + | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> + let outtype' = reduceaux context [] outtype in + let term' = reduceaux context [] term in + let pl' = List.map (reduceaux context []) pl in + let res = + C.MutCase (mutind,i,outtype',term',pl') + in + if l = [] then res else C.Appl (res::l) + ) + | C.Fix (i,fl) -> + let tys = + List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.Fix (i, fl') + in + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth l recindex) + with + _ -> None + in + (match recparam with + Some recparam -> + (match reduceaux context [] recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + (* Possible optimization: substituting whd recparam in l*) + reduceaux context l body' + | _ -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | None -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | C.CoFix (i,fl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' = + let fl' = + List.map + (function (n,ty,bo) -> + (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.CoFix (i, fl') + in + if l = [] then t' else C.Appl (t'::l) + and reduceaux_exp_named_subst context l = + List.map (function uri,t -> uri,reduceaux context [] t) + in + reduceaux context [] +;; + +exception WrongShape;; +exception AlreadySimplified;; + +(* Takes a well-typed term and *) +(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *) +(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *) +(* w.r.t. zero or more variables and if the Fix can be reduced, than it *) +(* is reduced, the delta-reduction is succesfull and the whole algorithm *) +(* is applied again to the new redex; Step 3) is applied to the result *) +(* of the recursive simplification. Otherwise, if the Fix can not be *) +(* reduced, than the delta-reductions fails and the delta-redex is *) +(* not reduced. Otherwise, if the delta-residual is not the *) +(* lambda-abstraction of a Fix, then it is reduced and the result is *) +(* directly returned, without performing step 3). *) +(* 3) Folds the application of the constant to the arguments that did not *) +(* change in every iteration, i.e. to the actual arguments for the *) +(* lambda-abstractions that precede the Fix. *) +(*CSC: It does not perform simplification in a Case *) +let simpl context = + (* reduceaux is equal to the reduceaux locally defined inside *) + (* reduce, but for the const case. *) + (**** Step 1 ****) + let rec reduceaux context l = + let module C = Cic in + let module S = CicSubstitution in + function + C.Rel n as t -> + (match List.nth context (n-1) with + Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) + | Some (_,C.Def bo) -> + try_delta_expansion l t (S.lift n bo) + | None -> raise RelToHiddenHypothesis + ) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + (match CicEnvironment.get_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | C.Variable (_,None,_,_) -> + let t' = C.Var (uri,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.Variable (_,Some body,_,_) -> + reduceaux context l + (CicSubstitution.subst_vars exp_named_subst' body) + ) + | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) + | C.Sort _ as t -> t (* l should be empty *) + | C.Implicit as t -> t + | C.Cast (te,ty) -> + C.Cast (reduceaux context l te, reduceaux context l ty) + | C.Prod (name,s,t) -> + assert (l = []) ; + C.Prod (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | C.Lambda (name,s,t) -> + (match l with + [] -> + C.Lambda (name, + reduceaux context [] s, + reduceaux ((Some (name,C.Decl s))::context) [] t) + | he::tl -> reduceaux context tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.LetIn (n,s,t) -> + reduceaux context l (S.subst (reduceaux context [] s) t) + | C.Appl (he::tl) -> + let tl' = List.map (reduceaux context []) tl in + reduceaux context (tl'@l) he + | C.Appl [] -> raise (Impossible 1) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + (match CicEnvironment.get_obj uri with + C.Constant (_,Some body,_,_) -> + try_delta_expansion l + (C.Const (uri,exp_named_subst')) + (CicSubstitution.subst_vars exp_named_subst' body) + | C.Constant (_,None,_,_) -> + let t' = C.Const (uri,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + let t' = C.MutInd (uri,i,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = + reduceaux_exp_named_subst context l exp_named_subst + in + let t' = C.MutConstruct(uri,i,j,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) + | C.MutCase (mutind,i,outtype,term,pl) -> + let decofix = + function + C.CoFix (i,fl) as t -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + reduceaux context [] body' + | C.Appl (C.CoFix (i,fl) :: tl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + let tl' = List.map (reduceaux context []) tl in + reduceaux context tl body' + | t -> t + in + (match decofix (reduceaux context [] term) with + C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) + | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> + let (arity, r) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,ingredients,r) -> + let (_,_,arity,_) = List.nth tl i in + (arity,r) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (r,tl) + in + reduceaux context (ts@l) (List.nth pl (j-1)) + | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> + let outtype' = reduceaux context [] outtype in + let term' = reduceaux context [] term in + let pl' = List.map (reduceaux context []) pl in + let res = + C.MutCase (mutind,i,outtype',term',pl') + in + if l = [] then res else C.Appl (res::l) + ) + | C.Fix (i,fl) -> + let tys = + List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' () = + let fl' = + List.map + (function (n,recindex,ty,bo) -> + (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.Fix (i, fl') + in + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth l recindex) + with + _ -> None + in + (match recparam with + Some recparam -> + (match reduceaux context [] recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + (* Possible optimization: substituting whd recparam in l*) + reduceaux context l body' + | _ -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | None -> if l = [] then t' () else C.Appl ((t' ())::l) + ) + | C.CoFix (i,fl) -> + let tys = + List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + in + let t' = + let fl' = + List.map + (function (n,ty,bo) -> + (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) + ) fl + in + C.CoFix (i, fl') + in + if l = [] then t' else C.Appl (t'::l) + and reduceaux_exp_named_subst context l = + List.map (function uri,t -> uri,reduceaux context [] t) + (**** Step 2 ****) + and try_delta_expansion l term body = + let module C = Cic in + let module S = CicSubstitution in + try + let res,constant_args = + let rec aux rev_constant_args l = + function + C.Lambda (name,s,t) as t' -> + begin + match l with + [] -> raise WrongShape + | he::tl -> + (* when name is Anonimous the substitution should *) + (* be superfluous *) + aux (he::rev_constant_args) tl (S.subst he t) + end + | C.LetIn (_,s,t) -> + aux rev_constant_args l (S.subst s t) + | C.Fix (i,fl) as t -> + let tys = + List.map (function (name,_,ty,_) -> + Some (C.Name name, C.Decl ty)) fl + in + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + List.nth l recindex + with + _ -> raise AlreadySimplified + in + (match CicReduction.whd context recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (function _ -> + decr counter ; S.subst (C.Fix (!counter,fl)) + ) fl body + in + (* Possible optimization: substituting whd *) + (* recparam in l *) + reduceaux context l body', + List.rev rev_constant_args + | _ -> raise AlreadySimplified + ) + | _ -> raise WrongShape + in + aux [] l body + in + (**** Step 3 ****) + let term_to_fold, delta_expanded_term_to_fold = + match constant_args with + [] -> term,body + | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args) + in + let simplified_term_to_fold = + reduceaux context [] delta_expanded_term_to_fold + in + replace (=) simplified_term_to_fold term_to_fold res + with + WrongShape -> + (* The constant does not unfold to a Fix lambda-abstracted *) + (* w.r.t. zero or more variables. We just perform reduction.*) + reduceaux context l body + | AlreadySimplified -> + (* If we performed delta-reduction, we would find a Fix *) + (* not applied to a constructor. So, we refuse to perform *) + (* delta-reduction. *) + if l = [] then term else C.Appl (term::l) + in + reduceaux context [] +;; diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli new file mode 100644 index 000000000..91bce1a39 --- /dev/null +++ b/helm/ocaml/tactics/proofEngineReduction.mli @@ -0,0 +1,47 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception Impossible of int +exception ReferenceToConstant +exception ReferenceToVariable +exception ReferenceToCurrentProof +exception ReferenceToInductiveDefinition +exception WrongUriToInductiveDefinition +exception RelToHiddenHypothesis +exception WrongShape +exception AlreadySimplified + +val alpha_equivalence: Cic.term -> Cic.term -> bool +val replace : + equality:(Cic.term -> 'a -> bool) -> + what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term +val replace_lifting : + equality:(Cic.term -> Cic.term -> bool) -> + what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term +val replace_lifting_csc : + int -> equality:(Cic.term -> Cic.term -> bool) -> + what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term +val reduce : Cic.context -> Cic.term -> Cic.term +val simpl : Cic.context -> Cic.term -> Cic.term diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml new file mode 100644 index 000000000..d89420f58 --- /dev/null +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -0,0 +1,149 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open ProofEngineTypes + +let clearbody ~hyp ~status:(proof, goal) = + let module C = Cic in + match hyp with + None -> assert false + | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") + | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body -> + let curi,metasenv,pbo,pty = proof in + let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + t when t == hyp_to_clear_body -> + let cleared_entry = + let ty = + CicTypeChecker.type_of_aux' metasenv context term + in + Some (n_to_clear_body, Cic.Decl ty) + in + cleared_entry::context + | None -> None::context + | Some (n,C.Decl t) + | Some (n,C.Def t) -> + let _ = + try + CicTypeChecker.type_of_aux' metasenv context t + with + _ -> + raise + (Fail + ("The correctness of hypothesis " ^ + string_of_name n ^ + " relies on the body of " ^ + string_of_name n_to_clear_body) + ) + in + entry::context + ) canonical_context [] + in + let _ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + with + _ -> + raise + (Fail + ("The correctness of the goal relies on the body of " ^ + string_of_name n_to_clear_body)) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] + +let clear ~hyp:hyp_to_clear ~status:(proof, goal) = + let module C = Cic in + match hyp_to_clear with + None -> assert false + | Some (n_to_clear, _) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = + List.find (function (m,_,_) -> m=goal) metasenv + in + let string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + t when t == hyp_to_clear -> None::context + | None -> None::context + | Some (n,C.Decl t) + | Some (n,C.Def t) -> + let _ = + try + CicTypeChecker.type_of_aux' metasenv context t + with + _ -> + raise + (Fail + ("Hypothesis " ^ + string_of_name n ^ + " uses hypothesis " ^ + string_of_name n_to_clear) + ) + in + entry::context + ) canonical_context [] + in + let _ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + with + _ -> + raise + (Fail + ("Hypothesis " ^ string_of_name n_to_clear ^ + " occurs in the goal")) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] + diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.mli b/helm/ocaml/tactics/proofEngineStructuralRules.mli new file mode 100644 index 000000000..32ba812ac --- /dev/null +++ b/helm/ocaml/tactics/proofEngineStructuralRules.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val clearbody: hyp: Cic.hypothesis -> ProofEngineTypes.tactic +val clear: hyp: Cic.hypothesis -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml new file mode 100644 index 000000000..f5e75fc47 --- /dev/null +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -0,0 +1,41 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + (** + current proof (proof uri * metas * (in)complete proof * term to be prooved) + *) +type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term + (** current goal, integer index *) +type goal = int + (** + a tactic: make a transition from one status to another one or, usually, + raise a "Fail" (@see Fail) exception in case of failure + *) + (** an unfinished proof with the optional current goal *) +type tactic = status:(proof * goal) -> proof * goal list + + (** tactic failure *) +exception Fail of string + diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml new file mode 100644 index 000000000..54b439b25 --- /dev/null +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -0,0 +1,127 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* +let reduction_tac ~reduction ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let new_ty = reduction context ty in + let new_metasenv = + List.map + (function + (n,_,_) when n = metano -> (metano,context,new_ty) + | _ as t -> t + ) metasenv + in + (curi,new_metasenv,pbo,pty), [metano] +;; +*) + +(* The default of term is the thesis of the goal to be prooved *) +let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let term = + match term with None -> ty | Some t -> t + in + (* We don't know if [term] is a subterm of [ty] or a subterm of *) + (* the type of one metavariable. So we replace it everywhere. *) + (*CSC: Il vero problema e' che non sapendo dove sia il term non *) + (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) + (*CSC: e' meglio prima cercare il termine e scoprirne il *) + (*CSC: contesto, poi ridurre e infine rimpiazzare. *) + let replace context where= +(*CSC: Per il momento se la riduzione fallisce significa solamente che *) +(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) +(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) + try + let term' = reduction context term in + ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' + ~where:where + with + _ -> where + in + let ty' = replace context ty in + let context' = + if also_in_hypotheses then + List.fold_right + (fun entry context -> + match entry with + Some (name,Cic.Def t) -> + (Some (name,Cic.Def (replace context t)))::context + | Some (name,Cic.Decl t) -> + (Some (name,Cic.Decl (replace context t)))::context + | None -> None::context + ) context [] + else + context + in + let metasenv' = + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [metano] +;; + +let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;; +let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;; +let whd_tac = reduction_tac ~reduction:CicReduction.whd ;; + +let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let term' = reduction context term in + (* We don't know if [term] is a subterm of [ty] or a subterm of *) + (* the type of one metavariable. So we replace it everywhere. *) + (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) + (*CSC: che si guadagni nulla in fatto di efficienza. *) + let replace = + ProofEngineReduction.replace ~equality:(=) ~what:term' ~with_what:term + in + let ty' = replace ty in + let metasenv' = + let context' = + if also_in_hypotheses then + List.map + (function + Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) + | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t)) + | None -> None + ) context + else + context + in + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + + in + (curi,metasenv',pbo,pty), [metano] +;; diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli new file mode 100644 index 000000000..8df6c2468 --- /dev/null +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* The default of term is the thesis of the goal to be prooved *) +val simpl_tac: + also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic +val reduce_tac: + also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic +val whd_tac: + also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic + +val fold_tac: + reduction:(Cic.context -> Cic.term -> Cic.term) -> + also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml new file mode 100644 index 000000000..c7015a755 --- /dev/null +++ b/helm/ocaml/tactics/ring.ml @@ -0,0 +1,594 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open CicReduction +open PrimitiveTactics +open ProofEngineTypes +open UriManager + +(** DEBUGGING *) + + (** perform debugging output? *) +let debug = false + + (** debugging print *) +let warn s = + if debug then + prerr_endline ("RING WARNING: " ^ s) + +(** CIC URIS *) + +(** + Note: For constructors URIs aren't really URIs but rather triples of + the form (uri, typeno, consno). This discrepancy is to preserver an + uniformity of invocation of "mkXXX" functions. +*) + +let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind" +let refl_eqt_uri = (eqt_uri, 0, 1) +let equality_is_a_congruence_A = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var" +let equality_is_a_congruence_x = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var" +let equality_is_a_congruence_y = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var" +let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con" +let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind" +let true_uri = (bool_uri, 0, 1) +let false_uri = (bool_uri, 0, 2) + +let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con" +let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" +let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con" +let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con" +let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" +let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" +let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con" + +let apolynomial_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind" +let apvar_uri = (apolynomial_uri, 0, 1) +let ap0_uri = (apolynomial_uri, 0, 2) +let ap1_uri = (apolynomial_uri, 0, 3) +let applus_uri = (apolynomial_uri, 0, 4) +let apmult_uri = (apolynomial_uri, 0, 5) +let apopp_uri = (apolynomial_uri, 0, 6) + +let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var" +let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind" +let empty_vm_uri = (varmap_uri, 0, 1) +let node_vm_uri = (varmap_uri, 0, 2) +let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con" +let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind" +let left_idx_uri = (index_uri, 0, 1) +let right_idx_uri = (index_uri, 0, 2) +let end_idx_uri = (index_uri, 0, 3) + +let abstract_rings_A_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var" +let abstract_rings_Aplus_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var" +let abstract_rings_Amult_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var" +let abstract_rings_Aone_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var" +let abstract_rings_Azero_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var" +let abstract_rings_Aopp_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var" +let abstract_rings_Aeq_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var" +let abstract_rings_vm_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var" +let abstract_rings_T_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var" +let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con" +let interp_sacs_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con" +let apolynomial_normalize_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con" +let apolynomial_normalize_ok_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con" + +(** CIC PREDICATES *) + + (** + check whether a term is a constant or not, if argument "uri" is given and is + not "None" also check if the constant correspond to the given one or not + *) +let cic_is_const ?(uri: uri option = None) term = + match uri with + | None -> + (match term with + | Cic.Const _ -> true + | _ -> false) + | Some realuri -> + (match term with + | Cic.Const (u, _) when (eq u realuri) -> true + | _ -> false) + +(** PROOF AND GOAL ACCESSORS *) + + (** + @param proof a proof + @return the uri of a given proof + *) +let uri_of_proof ~proof:(uri, _, _, _) = uri + + (** + @param metano meta list index + @param metasenv meta list (environment) + @raise Failure if metano is not found in metasenv + @return conjecture corresponding to metano in metasenv + *) +let conj_of_metano metano = + try + List.find (function (m, _, _) -> m = metano) + with Not_found -> + failwith ( + "Ring.conj_of_metano: " ^ + (string_of_int metano) ^ " no such meta") + + (** + @param status current proof engine status + @raise Failure if proof is None + @return current goal's metasenv + *) +let metasenv_of_status ~status:((_,m,_,_), _) = m + + (** + @param status a proof engine status + @raise Failure when proof or goal are None + @return context corresponding to current goal + *) +let context_of_status ~status:(proof, goal as status) = + let metasenv = metasenv_of_status ~status:status in + let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in + context + +(** CIC TERM CONSTRUCTORS *) + + (** + Create a Cic term consisting of a constant + @param uri URI of the constant + @proof current proof + @exp_named_subst explicit named substitution + *) +let mkConst ~uri ~exp_named_subst = + Cic.Const (uri, exp_named_subst) + + (** + Create a Cic term consisting of a constructor + @param uri triple where uri is the uri of an inductive + type, typeno is the type number in a mutind structure (0 based), consno is + the constructor number (1 based) + @exp_named_subst explicit named substitution + *) +let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst = + Cic.MutConstruct (uri, typeno, consno, exp_named_subst) + + (** + Create a Cic term consisting of a type member of a mutual induction + @param uri pair where uri is the uri of a mutual inductive + type and typeno is the type number (0 based) in the mutual induction + @exp_named_subst explicit named substitution + *) +let mkMutInd ~uri:(uri, typeno) ~exp_named_subst = + Cic.MutInd (uri, typeno, exp_named_subst) + +(** EXCEPTIONS *) + + (** + raised when the current goal is not ringable; a goal is ringable when is an + equality on reals (@see r_uri) + *) +exception GoalUnringable + +(** RING's FUNCTIONS LIBRARY *) + + (** + Check whether the ring tactic can be applied on a given term (i.e. that is + an equality on reals) + @param term to be tested + @return true if the term is ringable, false otherwise + *) +let ringable = + let is_equality = function + | Cic.MutInd (uri, 0, []) when (eq uri eqt_uri) -> true + | _ -> false + in + let is_real = function + | Cic.Const (uri, _) when (eq uri r_uri) -> true + | _ -> false + in + function + | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) -> + warn "Goal Ringable!"; + true + | _ -> + warn "Goal Not Ringable :-(("; + false + + (** + split an equality goal of the form "t1 = t2" in its two subterms t1 and t2 + after checking that the goal is ringable + @param goal the current goal + @return a pair (t1,t2) that are two sides of the equality goal + @raise GoalUnringable if the goal isn't ringable + *) +let split_eq = function + | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term -> + warn ("" ^ (CicPp.ppterm t1) ^ ""); + warn ("" ^ (CicPp.ppterm t2) ^ ""); + (t1, t2) + | _ -> raise GoalUnringable + + (** + @param i an integer index representing a 1 based number of node in a binary + search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left + child of the root (if any), 3 is the right child of the root (if any), 4 is + the left child of the left child of the root (if any), ....) + @param proof the current proof + @return an index representing the same node in a varmap (@see varmap_uri), + the returned index is as defined in index (@see index_uri) + *) +let path_of_int n = + let rec digits_of_int n = + if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + in + List.fold_right + (fun digit path -> + Cic.Appl [ + mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) []; + path]) + (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *) + (mkCtor end_idx_uri []) + + (** + Build a variable map (@see varmap_uri) from a variables array. + A variable map is almost a binary tree so this function receiving a var list + like [v;w;x;y;z] will build a varmap of shape: v + / \ + w x + / \ + y z + @param vars variables array + @return a cic term representing the variable map containing vars variables + *) +let btree_of_array ~vars = + let r = mkConst r_uri [] in (* cic objects *) + let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in + let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in + let size = Array.length vars in + let halfsize = size lsr 1 in + let rec aux n = (* build the btree starting from position n *) + (* + n is the position in the vars array _1_based_ in order to access + left and right child using (n*2, n*2+1) trick + *) + if n > size then + empty_vm_r + else if n > halfsize then (* no more children *) + Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r] + else (* still children *) + Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)] + in + aux 1 + + (** + abstraction function: + concrete polynoms -----> (abstract polynoms, varmap) + @param terms list of conrete polynoms + @return a pair where aterms is a list of abstract polynoms + and varmap is the variable map needed to interpret them + *) +let abstract_poly ~terms = + let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *) + let varlist = ref [] in (* vars list in reverse order *) + let counter = ref 1 in (* index of next new variable *) + let rec aux = function (* TODO not tail recursive *) + (* "bop" -> binary operator | "uop" -> unary operator *) + | Cic.Appl (bop::t1::t2::[]) + when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *) + Cic.Appl [mkCtor applus_uri []; aux t1; aux t2] + | Cic.Appl (bop::t1::t2::[]) + when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *) + Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2] + | Cic.Appl (uop::t::[]) + when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *) + Cic.Appl [mkCtor apopp_uri []; aux t] + | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *) + mkCtor ap0_uri [] + | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *) + mkCtor ap1_uri [] + | t -> (* variable *) + try + Hashtbl.find varhash t (* use an old var *) + with Not_found -> begin (* create a new var *) + let newvar = + Cic.Appl [mkCtor apvar_uri []; path_of_int !counter] + in + incr counter; + varlist := t :: !varlist; + Hashtbl.add varhash t newvar; + newvar + end + in + let aterms = List.map aux terms in (* abstract vars *) + let varmap = (* build varmap *) + btree_of_array ~vars:(Array.of_list (List.rev !varlist)) + in + (aterms, varmap) + + (** + given a list of abstract terms (i.e. apolynomials) build the ring "segments" + that is triples like (t', t'', t''') where + t' = interp_ap(varmap, at) + t'' = interp_sacs(varmap, (apolynomial_normalize at)) + t''' = apolynomial_normalize_ok(varmap, at) + at is the abstract term built from t, t is a single member of aterms + *) +let build_segments ~terms = + let r = mkConst r_uri [] in (* cic objects *) + let rplus = mkConst rplus_uri [] in + let rmult = mkConst rmult_uri [] in + let ropp = mkConst ropp_uri [] in + let r1 = mkConst r1_uri [] in + let r0 = mkConst r0_uri [] in + let theory_args_subst varmap = + [abstract_rings_A_uri, r ; + abstract_rings_Aplus_uri, rplus ; + abstract_rings_Amult_uri, rmult ; + abstract_rings_Aone_uri, r1 ; + abstract_rings_Azero_uri, r0 ; + abstract_rings_Aopp_uri, ropp ; + abstract_rings_vm_uri, varmap] in + let theory_args_subst' eq varmap t = + [abstract_rings_A_uri, r ; + abstract_rings_Aplus_uri, rplus ; + abstract_rings_Amult_uri, rmult ; + abstract_rings_Aone_uri, r1 ; + abstract_rings_Azero_uri, r0 ; + abstract_rings_Aopp_uri, ropp ; + abstract_rings_Aeq_uri, eq ; + abstract_rings_vm_uri, varmap ; + abstract_rings_T_uri, t] in + let interp_ap varmap = + mkConst interp_ap_uri (theory_args_subst varmap) in + let interp_sacs varmap = + mkConst interp_sacs_uri (theory_args_subst varmap) in + let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in + let apolynomial_normalize_ok eq varmap t = + mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in + let rtheory = mkConst rtheory_uri [] in + let lxy_false = (** Cic funcion "fun (x,y):R -> false" *) + Cic.Lambda (Cic.Anonymous, r, + Cic.Lambda (Cic.Anonymous, r, + mkCtor false_uri [])) + in + let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *) + List.map (* build ring segments *) + (fun t -> + Cic.Appl [interp_ap varmap ; t], + Cic.Appl ( + [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]), + Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t] + ) aterms + + +let status_of_single_goal_tactic_result = + function + proof,[goal] -> proof,goal + | _ -> + raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal") + +(* Galla: spostata in variousTactics.ml + (** + auxiliary tactic "elim_type" + @param status current proof engine status + @param term term to cut + *) +let elim_type_tac ~term ~status = + warn "in Ring.elim_type_tac"; + Tacticals.thens ~start:(cut_tac ~term) + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status +*) + + (** + auxiliary tactic, use elim_type and try to close 2nd subgoal using proof + @param status current proof engine status + @param term term to cut + @param proof term used to prove second subgoal generated by elim_type + *) +let elim_type2_tac ~term ~proof ~status = + let module E = EliminationTactics in + warn "in Ring.elim_type2"; + Tacticals.thens ~start:(E.elim_type_tac ~term) + ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status + +(* Galla: spostata in variousTactics.ml + (** + Reflexivity tactic, try to solve current goal using "refl_eqT" + Warning: this isn't equale to the coq's Reflexivity because this one tries + only refl_eqT, coq's one also try "refl_equal" + @param status current proof engine status + *) +let reflexivity_tac ~status:(proof, goal) = + warn "in Ring.reflexivity_tac"; + let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in + try + apply_tac ~status:(proof, goal) ~term:refl_eqt + with (Fail _) as e -> + let e_str = Printexc.to_string e in + raise (Fail ("Reflexivity failed with exception: " ^ e_str)) +*) + + (** lift an 8-uple of debrujins indexes of n *) +let lift ~n (a,b,c,d,e,f,g,h) = + match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with + | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h) + | _ -> assert false + + (** + remove hypothesis from a given status starting from the last one + @param count number of hypotheses to remove + @param status current proof engine status + *) +let purge_hyps_tac ~count ~status:(proof, goal as status) = + let module S = ProofEngineStructuralRules in + let rec aux n context status = + assert(n>=0); + match (n, context) with + | (0, _) -> status + | (n, hd::tl) -> + aux (n-1) tl + (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status)) + | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" + in + let (_, metasenv, _, _) = proof in + let (_, context, _) = conj_of_metano goal metasenv in + let proof',goal' = aux count context status in + assert (goal = goal') ; + proof',[goal'] + +(** THE TACTIC! *) + + (** + Ring tactic, does associative and commutative rewritings in Reals ring + @param status current proof engine status + *) +let ring_tac ~status:((proof, goal) as status) = + warn "in Ring tactic"; + let eqt = mkMutInd (eqt_uri, 0) [] in + let r = mkConst r_uri [] in + let metasenv = metasenv_of_status ~status in + let (metano, context, ty) = conj_of_metano goal metasenv in + let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) + match (build_segments ~terms:[t1; t2]) with + | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin + List.iter (* debugging, feel free to remove *) + (fun (descr, term) -> + warn (descr ^ " " ^ (CicPp.ppterm term))) + (List.combine + ["t1"; "t1'"; "t1''"; "t1'_eq_t1''"; + "t2"; "t2'"; "t2''"; "t2'_eq_t2''"] + [t1; t1'; t1''; t1'_eq_t1''; + t2; t2'; t2''; t2'_eq_t2'']); + try + let new_hyps = ref 0 in (* number of new hypotheses created *) + Tacticals.try_tactics + ~status + ~tactics:[ + "reflexivity", EqualityTactics.reflexivity_tac ; + "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; + "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ; + "exact sym_eqt su t1 ...", exact_tac + ~term:( + Cic.Appl + [mkConst sym_eqt_uri + [equality_is_a_congruence_A, mkConst r_uri [] ; + equality_is_a_congruence_x, t1'' ; + equality_is_a_congruence_y, t1 + ] ; + t1'_eq_t1'' + ]) ; + "elim_type eqt su t1 ...", (fun ~status -> + let status' = (* status after 1st elim_type use *) + let context = context_of_status ~status in + if not (are_convertible context t1'' t1) then begin + warn "t1'' and t1 are NOT CONVERTIBLE"; + let newstatus = + elim_type2_tac (* 1st elim_type use *) + ~status ~proof:t1'_eq_t1'' + ~term:(Cic.Appl [eqt; r; t1''; t1]) + in + incr new_hyps; (* elim_type add an hyp *) + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false + end else begin + warn "t1'' and t1 are CONVERTIBLE"; + status + end + in + let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') = + lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') + in + let status'' = + Tacticals.try_tactics (* try to solve 1st subgoal *) + ~status:status' + ~tactics:[ + "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; + "exact sym_eqt su t2 ...", + exact_tac + ~term:( + Cic.Appl + [mkConst sym_eqt_uri + [equality_is_a_congruence_A, mkConst r_uri [] ; + equality_is_a_congruence_x, t2'' ; + equality_is_a_congruence_y, t2 + ] ; + t2'_eq_t2'' + ]) ; + "elim_type eqt su t2 ...", (fun ~status -> + let status' = + let context = context_of_status ~status in + if not (are_convertible context t2'' t2) then begin + warn "t2'' and t2 are NOT CONVERTIBLE"; + let newstatus = + elim_type2_tac (* 2nd elim_type use *) + ~status ~proof:t2'_eq_t2'' + ~term:(Cic.Appl [eqt; r; t2''; t2]) + in + incr new_hyps; (* elim_type add an hyp *) + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false + end else begin + warn "t2'' and t2 are CONVERTIBLE"; + status + end + in + try (* try to solve main goal *) + warn "trying reflexivity ...."; + EqualityTactics.reflexivity_tac ~status:status' + with (Fail _) -> (* leave conclusion to the user *) + warn "reflexivity failed, solution's left as an ex :-)"; + purge_hyps_tac ~count:!new_hyps ~status:status')] + in + status'')] + with (Fail s) -> + raise (Fail ("Ring failure: " ^ s)) + end + | _ -> (* impossible: we are applying ring exacty to 2 terms *) + assert false + + (* wrap ring_tac catching GoalUnringable and raising Fail *) +let ring_tac ~status = + try + ring_tac ~status + with GoalUnringable -> + raise (Fail "goal unringable") + diff --git a/helm/ocaml/tactics/ring.mli b/helm/ocaml/tactics/ring.mli new file mode 100644 index 000000000..b6eb34b69 --- /dev/null +++ b/helm/ocaml/tactics/ring.mli @@ -0,0 +1,12 @@ + + (* ring tactics *) +val ring_tac: ProofEngineTypes.tactic + +(*Galla: spostata in variuosTactics.ml + (* auxiliary tactics *) +val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic +*) + +(* spostata in variousTactics.ml +val reflexivity_tac: ProofEngineTypes.tactic +*) diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml new file mode 100644 index 000000000..1319c13ca --- /dev/null +++ b/helm/ocaml/tactics/tacticals.ml @@ -0,0 +1,249 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open CicReduction +open ProofEngineTypes +open UriManager + +(** DEBUGGING *) + + (** perform debugging output? *) +let debug = false + + (** debugging print *) +let warn s = + if debug then + prerr_endline ("TACTICALS WARNING: " ^ s) + + +(** TACTIC{,AL}S *) + + (* not a tactical, but it's used only here (?) *) + +let id_tac ~status:(proof,goal) = + (proof,[goal]) + + + (** + naive implementation of ORELSE tactical, try a sequence of tactics in turn: + if one fails pass to the next one and so on, eventually raises (failure "no + tactics left") + TODO warning: not tail recursive due to "try .. with" boxing + + Galla: is this exactly Coq's "First"? + + *) +let rec try_tactics ~(tactics: (string * tactic) list) ~status = + warn "in Tacticals.try_tactics"; + match tactics with + | (descr, tac)::tactics -> + warn ("Tacticals.try_tactics IS TRYING " ^ descr); + (try + let res = tac ~status in + warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!"); + res + with + e -> + match e with + (Fail _) + | (CicTypeChecker.NotWellTyped _) + | (CicUnification.UnificationFailed) -> + warn ( + "Tacticals.try_tactics failed with exn: " ^ + Printexc.to_string e); + try_tactics ~tactics ~status + | _ -> raise e (* [e] must not be caught ; let's re-raise it *) + ) + | [] -> raise (Fail "try_tactics: no tactics left") + + + +let thens ~start ~continuations ~status = + let (proof,new_goals) = start ~status in + try + List.fold_left2 + (fun (proof,goals) goal tactic -> + let (proof',new_goals') = tactic ~status:(proof,goal) in + (proof',goals@new_goals') + ) (proof,[]) new_goals continuations + with + Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") + + + +let then_ ~start ~continuation ~status = + let (proof,new_goals) = start ~status in + List.fold_left + (fun (proof,goals) goal -> + let (proof',new_goals') = continuation ~status:(proof,goal) in + (proof',goals@new_goals') + ) (proof,[]) new_goals + + +(* Galla *) +(* si suppone che tutte le tattiche sollevino solamente Fail? *) + + +(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *) + +(* This keep on appling tactic until it fails *) +(* When generates more than one goal, you have a tree of + application on the tactic, repeat_tactic works in depth on this tree *) + +let rec repeat_tactic ~tactic ~status = + warn "in repeat_tactic"; + try let (proof, goallist) = tactic ~status in + let rec step proof goallist = + match goallist with + [] -> (proof, []) + | head::tail -> + let (proof', goallist') = repeat_tactic ~tactic ~status:(proof, head) in + let (proof'', goallist'') = step proof' tail in + proof'', goallist'@goallist'' + in + step proof goallist + with + (Fail _) as e -> + warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; + id_tac ~status +;; + + + +(* This tries to apply tactic n times *) + +let rec do_tactic ~n ~tactic ~status = + warn "in do_tactic"; + try + let (proof, goallist) = + if (n>0) then tactic ~status + else id_tac ~status in +(* else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *) + let rec step proof goallist = + match goallist with + [] -> (proof, []) + | head::tail -> + let (proof', goallist') = do_tactic ~n:(n-1) ~tactic ~status:(proof, head) in + let (proof'', goallist'') = step proof' tail in + proof'', goallist'@goallist'' + in + step proof goallist + with + (Fail _) as e -> + warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; + id_tac ~status +;; + + + +(* This applies tactic and catches its possible failure *) + +let rec try_tactic ~tactic ~status = + warn "in Tacticals.try_tactic"; + try + tactic ~status + with + (Fail _) as e -> + warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e); + id_tac ~status +;; + + +(* This tries tactics until one of them doesn't _solve_ the goal *) +(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) + +let rec solve_tactics ~(tactics: (string * tactic) list) ~status = + warn "in Tacticals.solve_tactics"; + match tactics with + | (descr, currenttactic)::moretactics -> + warn ("Tacticals.solve_tactics is trying " ^ descr); + (try + let (proof, goallist) = currenttactic ~status in + match goallist with + [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!"); +(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *) +(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) + (proof, goallist) + | _ -> warn ("Tacticals.solve_tactics: try the next tactic"); + solve_tactics ~tactics:(moretactics) ~status + with + (Fail _) as e -> + warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e); + solve_tactics ~tactics ~status + ) + | [] -> raise (Fail "solve_tactics cannot solve the goal"); + id_tac ~status +;; + + + + + + + + + + + (** tattica di prova per debuggare i tatticali *) +(* +let thens' ~start ~continuations ~status = + let (proof,new_goals) = start ~status in + try + List.fold_left2 + (fun (proof,goals) goal tactic -> + let (proof',new_goals') = tactic ~status:(proof,goal) in + (proof',goals@new_goals') + ) (proof,[]) new_goals continuations + with + Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") + +let prova_tac = + let apply_T_tac ~status:((proof,goal) as status) = + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let rel = + let rec find n = + function + [] -> assert false + | (Some (Cic.Name name,_))::_ when name = "T" -> n + | _::tl -> find (n+1) tl + in + prerr_endline ("eseguo find"); + find 1 context + in + prerr_endline ("eseguo apply"); + apply_tac ~term:(Cic.Rel rel) ~status + in +(* do_tactic ~n:2 *) + repeat_tactic + ~tactic: + (then_ + ~start:(intros_tac ~name:"pippo") + ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)])) +(* id_tac *) +;; +*) + + diff --git a/helm/ocaml/tactics/tacticals.mli b/helm/ocaml/tactics/tacticals.mli new file mode 100644 index 000000000..b1861b5fa --- /dev/null +++ b/helm/ocaml/tactics/tacticals.mli @@ -0,0 +1,61 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +val id_tac : ProofEngineTypes.tactic + + + + (* pseudo tacticals *) +val try_tactics: + tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic + +val thens: + start: ProofEngineTypes.tactic -> + continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic + +val then_: + start: ProofEngineTypes.tactic -> + continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + + +val repeat_tactic: + tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + +val do_tactic: + n: int -> + tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + +val try_tactic: + tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + +val solve_tactics: + tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic + + + +(* +val prova_tac : ProofEngineTypes.tactic +*) diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml new file mode 100644 index 000000000..1df9128c1 --- /dev/null +++ b/helm/ocaml/tactics/variousTactics.ml @@ -0,0 +1,206 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio +chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una +funzione di callback che restituisce la (sola) hyp da applicare *) + +let assumption_tac ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let _,metasenv,_,_ = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let rec find n = function + hd::tl -> + (match hd with + (Some (_, C.Decl t)) when + (R.are_convertible context (S.lift n t) ty) -> n + | (Some (_, C.Def t)) when + (R.are_convertible context + (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n + | _ -> find (n+1) tl + ) + | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption") + in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context)) +;; + +(* Questa invece era in fourierR.ml +let assumption_tac ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let num = ref 0 in + let tac_list = List.map + ( fun x -> num := !num + 1; + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) + ) + context + in + Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) +;; +*) + + +(* ANCORA DA DEBUGGARE *) + +(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda +e li aggiunga nel context, poi si conta la lunghezza di questo nuovo +contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *) + +let generalize_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +(* + let found = false in + let rec new_context context ty = + if ty == term then let found = true in context + else match ty with + C.Rel _ + | C.Var _ + | C.Meta _ (* ???? *) + | C.Sort s + | C.Implicit -> context + | C.Cast (val,typ) -> + let tmp_context = new_context context val in + tmp_context @ (new_context tmp_context typ) + | C.Prod (binder, source, target) -> + | C.Lambda (binder, source, target) -> + let tmp_context = new_context context source in + tmp_context @ (new_context tmp_context binder) + | C.LetIn (binder, term, target) -> + | C.Appl applist -> + let rec aux context = + match applist with + [] -> context + | hd::tl -> + let tmp_context = (new_context context hd) + in aux tmp_context tl + in aux context applist + | C.Const (uri, exp_named_subst) + | C.MutInd (uri, typeno, exp_named_subst) + | C.MutConstruct (uri, typeno, consno, exp_named_subst) -> + match exp_named_subst with + [] -> context + | (uri,t)::_ -> new_context context (type_of_aux' context t) + | _ -> assert false + | C.MutCase (uri, typeno, outtype, iterm, patterns) + | C.Fix (funno, funlist) + | C.CoFix (funno, funlist) -> + match funlist with + [] -> context (* caso possibile? *) + | (name, index, type, body)::_ -> + let tmp_context = ~ + in +*) + T.thens + ~start:(P.cut_tac + ~term:( + C.Prod( + (C.Name "dummy_for_gen"), + (CicTypeChecker.type_of_aux' metasenv context term), + (ProofEngineReduction.replace_lifting_csc 1 + ~equality:(==) + ~what:term + ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) + ~where:ty) + ))) + ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] + ~status +;; + + +(* IN FASE DI IMPLEMENTAZIONE *) + +let decide_equality_tac = +(* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza +e' vera o no e lo risolve *) + Tacticals.id_tac +;; + + +let compare_tac ~term ~status:((proof, goal) as status) = +(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *) +(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *) + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let termty = (CicTypeChecker.type_of_aux' metasenv context term) in + match termty with + (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + + let term' = (* (t1=t2)\/~(t1=t2) *) + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; + term ; + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ; + t1 ; + C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] + ] + ] + in + T.thens + ~start:(P.cut_tac ~term:term') + ~continuations:[ + T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; + decide_equality_tac] + | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + let term' = (* (t1=t2) \/ ~(t1=t2) *) + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; + term ; + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ; + t1 ; + C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] + ] + ] + in + T.thens + ~start:(P.cut_tac ~term:term') + ~continuations:[ + T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; + decide_equality_tac] + | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") +;; + + +let discriminate_tac ~term ~status:((proof, goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + T.id_tac +;; + diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli new file mode 100644 index 000000000..27b59682f --- /dev/null +++ b/helm/ocaml/tactics/variousTactics.mli @@ -0,0 +1,34 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val assumption_tac: ProofEngineTypes.tactic + +val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic + +(* +val decide_equality_tac: ProofEngineTypes.tactic +val compare_tac: term1:Cic.term -> term2:Cic.term -> ProofEngineTypes.tactic +*) +