+++ /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 **********************)
-
-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
-
- prerr_endline("rewrite chiamata con "^CicPp.ppterm gty^"\n");
- 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/Equality/eq.ind") ->
- let eq_ind_r =
- C.Const
- (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
- 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",0)
- 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.syntactic_equality ~alpha_equivalence:true)
- ~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])
-;;
-
-(* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*)
-
-
-
-let simpl_tac ~status:(proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
-prerr_endline("simpl_tac su "^CicPp.ppterm ty);
-
- let new_ty = ProofEngineReduction.simpl context ty in
-
-prerr_endline("ritorna "^CicPp.ppterm new_ty);
-
- 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]
-
-;;
-
-let rewrite_simpl_tac ~term ~status =
-
- Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~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 =
- 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 f times a
-*)
-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
- @return proiection on string of t
-*)
-let rec string_of_term t =
- match t with
- Cic.Cast (t1,t2) -> string_of_term t1
- |Cic.Const (u,boh) -> UriManager.string_of_uri u
- |Cic.Var (u) -> UriManager.string_of_uri u
- | _ -> "not_of_constant"
-;;
-
-(* coq wrapper
-let string_of_constr = string_of_term
-;;
-*)
-
-(**
- @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 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
- try
- begin
- let a = rational_of_term arg1 in
- try
- begin
- let b = (rational_of_term arg2) in
- (flin_add_cste (flin_zero()) (rmult a b))
- end
- with
- _ -> (flin_add (flin_zero()) arg2 a)
- end
- with
- _-> (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 _ -> 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) =
- debug("Trasformo in ineq "^CicPp.ppterm t^"\n");
- 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" ->
- debug("Ho trovato una ==\n");
- 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}]
- |_-> debug("eqT deve essere applicato a const R\n");assert false)
- |_-> debug("eqT deve essere appl a const\n");assert false)
- |_-> debug("Il trmine e' un appl mutind ma non eqT\n");assert false)
- |_-> debug("Il termine non e' una app di const o app di mutind\n");assert false)(* match t1 *)
- |_-> debug("Il termine non e' una applicazione\n");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))
- 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 0 ;;
-let _False = Cic.MutInd (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
-let _not = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/not.con") 0;;
-let _R0 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
-let _R1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
-let _R = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
-let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
-let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
-let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
-let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
-let _Rfourier_le=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
-let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
-let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
-let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
-let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
-let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
-let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
-let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
-let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
-let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
-let _Rinv = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
-let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
- "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
-let _Rle = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
-let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
-let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
-let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
-let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
-let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
-let _Rlt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
-let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
-let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
-let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
-let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
-let _Rminus = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
-let _Rmult = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
-let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
-let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
-let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
-let _Ropp = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
-let _Rplus = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
-let _sym_eqT = Cic.Const(UriManager.uri_of_string
- "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
-
-(******************************************************************************)
-
-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 ^" fails\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
-*)
-
-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("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
- 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*)
- Ring.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)) ~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
-
- 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
- [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
- | a::next -> debug(" no\n"); filter_real_hyp next cont
-;;
-
-(* 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))^" e ty "^CicPp.ppterm ty ^"\n");
- let (proof,goals) =
- 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])
-;;
-
-
-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)
-;;
-
-(* !!!!! fix !!!!!!!!!! *)
-let contradiction_tac ~status:(proof,goal)=
- Tacticals.then_
- ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
- ~continuation:(Tacticals.then_
- ~start:(Ring.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 ~name:fhyp)
- ~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 _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");)
- hyps;
-
-
- debug ("applico fourier a "^ string_of_int (List.length !lineq)^
- " disequazioni\n");
-
- let res=fourier_lineq (!lineq) in
- let tac=ref Ring.id_tac in
- if res=[] then
- (print_string "Tactic Fourier fails.\n";flush stdout;
- failwith "fourier can't proove it")
- 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.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("Change_tac "^CicPp.ppterm ty^" with "^CicPp.ppterm (Cic.Appl [ _not; ineq]) ^"\n");
-
- 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 ->
- 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:(proof,goals as 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
-(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
- di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
- parametri della equality_replace vengono passati al contrario? Oppure la
- tattica usa i parametri al contrario?
- ~continuations:[Tacticals.then_
- ~start:(
- fun ~status:(proof,goal as status) ->
- debug("ECCOCI\n");
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=
- goal) metasenv in
- debug("ty = "^CicPp.ppterm ty^"\n");
- let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
- ~status in
- debug("fine ECCOCI\n");
- r)
- ~continuation:(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", Ring.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
- (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
- Cic.Prod (Cic.Anonimous,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:Ring.id_tac(*tac2*)]))
- ;Ring.id_tac(*!tac1*)]);(*end tac:=*)
- tac:=(Tacticals.thens
- ~start:(PrimitiveTactics.cut_tac ~term:_False)
- ~continuations:[Tacticals.then_
- ~start:(PrimitiveTactics.intros_tac ~name:"??")
- ~continuation:contradiction_tac
- ;!tac])
-
-
- |_-> assert false)(*match (!lutil) *)
- |_-> assert false); (*match res*)
- debug ("finalmente applico tac\n");
- (!tac ~status:(proof,goal))
-;;
-
-let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
-
-
projects / helm.git / commitdiff