+++ /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
-(* 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