--- /dev/null
+*.cmi
+*.cma
+*.cmo
+*.cmx
+*.cmxa
+*.o
+*.a
--- /dev/null
+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
--- /dev/null
+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
+
--- /dev/null
+(* 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
+;;
+
+
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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")
+;;
+
+
--- /dev/null
+(* 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
+
--- /dev/null
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* Méthode d'élimination de Fourier *)
+(* Référence:
+Auteur(s) : Fourier, Jean-Baptiste-Joseph
+
+Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,...
+
+Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890
+
+Pages: 326-327
+
+http://gallica.bnf.fr/
+*)
+
+(** @author The Coq Development Team *)
+
+
+(* Un peu de calcul sur les rationnels...
+Les opérations rendent des rationnels normalisés,
+i.e. le numérateur et le dénominateur sont premiers entre eux.
+*)
+
+
+(** Type for coefficents *)
+type rational = {
+num:int; (** Numerator *)
+den:int; (** Denumerator *)
+};;
+
+(** Debug function.
+ @param x the rational to print*)
+let print_rational x =
+ print_int x.num;
+ print_string "/";
+ print_int x.den
+;;
+
+let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);;
+
+(** The constant 0*)
+let r0 = {num=0;den=1};;
+(** The constant 1*)
+let r1 = {num=1;den=1};;
+
+let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
+ if x.num=0 then r0
+ else (let d=pgcd x.num x.den in
+ let d= (if d<0 then -d else d) in
+ {num=(x.num)/d;den=(x.den)/d});;
+
+(** Calculates the opposite of a rational.
+ @param x The rational
+ @return -x*)
+let rop x = rnorm {num=(-x.num);den=x.den};;
+
+(** Sums two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x+y*)
+let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};;
+(** Substracts two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x-y*)
+let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};;
+(** Multiplyes two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x*y*)
+let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};;
+(** Inverts arational.
+ @param x A rational
+ @return x{^ -1} *)
+let rinv x = rnorm {num=x.den;den=x.num};;
+(** Divides two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x/y*)
+let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};;
+
+let rinf x y = x.num*y.den < y.num*x.den;;
+let rinfeq x y = x.num*y.den <= y.num*x.den;;
+
+
+(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation
+c1x1+...+cnxn < d si strict=true, <= sinon,
+hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ.
+*)
+
+type ineq = {coef:rational list;
+ hist:rational list;
+ strict:bool};;
+
+let pop x l = l:=x::(!l);;
+
+(* sépare la liste d'inéquations s selon que leur premier coefficient est
+négatif, nul ou positif. *)
+let partitionne s =
+ let lpos=ref [] in
+ let lneg=ref [] in
+ let lnul=ref [] in
+ List.iter (fun ie -> 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;;
+
+*)
--- /dev/null
+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
--- /dev/null
+(* 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<n*1/d
+*)
+
+let tac_zero_inf_pos (n,d) ~status =
+ (*let cste = pf_parse_constr gl in*)
+ let pall str ~status:(proof,goal) t =
+ debug ("tac "^str^" :\n" );
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> 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);;
+
+
--- /dev/null
+(*
+val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic
+val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
+*)
+val fourier_tac: ProofEngineTypes.tactic
--- /dev/null
+(* 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
+;;
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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)
+;;
+*)
+
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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")
--- /dev/null
+(* 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
--- /dev/null
+(* 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')
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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 []
+;;
--- /dev/null
+(* 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
--- /dev/null
+(* 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]
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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]
+;;
--- /dev/null
+(* 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
--- /dev/null
+(* 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 <uri, typeno, consno> 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 <uri, typeno> 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 ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
+ warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
+ (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 <aterms, varmap> 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")
+
--- /dev/null
+
+ (* 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
+*)
--- /dev/null
+(* 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 <tactic> 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 *)
+;;
+*)
+
+
--- /dev/null
+(* 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
+*)
--- /dev/null
+(* 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
+;;
+
--- /dev/null
+(* 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
+*)
+
projects / helm.git / commitdiff