*)
+(******************** 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 Term
-open Tactics
-open Clenv
-open Names
-open Tacmach*)
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.
*)
-(*type flin = {fhom:(constr , rational)Hashtbl.t;
- fcste:rational};;
-let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};;
-let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;;
+(**
+ 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}
+;;
-let flin_add f x c =
+(**
+ @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
;;
-let flin_add_cste f c =
+(**
+ 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;
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);
-;;*)
-
+;;
+
+
(*****************************************************************************)
-(*let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
-let pf_parse_constr gl s =
- Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
-
-let rec string_of_constr c =
- match kind_of_term c with
- Cast (c,t) -> string_of_constr c
- |Const c -> string_of_path c
- |Var(c) -> string_of_id c
+
+
+(**
+ @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"
;;
-let rec rational_of_constr c =
- match kind_of_term c with
- | Cast (c,t) -> (rational_of_constr c)
- | App (c,args) ->
- (match kind_of_term c with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.Ropp" ->
- rop (rational_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rinv" ->
- rinv (rational_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rmult" ->
- rmult (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rdiv" ->
- rdiv (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rplus" ->
- rplus (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rminus" ->
- rminus (rational_of_constr args.(0))
- (rational_of_constr args.(1))
+(* 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")
- | Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.R1" -> r1
- |"Coq.Reals.Rdefinitions.R0" -> r0
+ | 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"
;;
-let rec flin_of_constr c =
+(* 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 kind_of_term c with
- | Cast (c,t) -> (flin_of_constr c)
- | App (c,args) ->
- (match kind_of_term c with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.Ropp" ->
- flin_emult (rop r1) (flin_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rplus"->
- flin_plus (flin_of_constr args.(0))
- (flin_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rminus"->
- flin_minus (flin_of_constr args.(0))
- (flin_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rmult"->
- (try (let a=(rational_of_constr args.(0)) in
- try (let b = (rational_of_constr args.(1)) in
- (flin_add_cste (flin_zero()) (rmult a b)))
- with _-> (flin_add (flin_zero())
- args.(1)
- a))
- with _-> (flin_add (flin_zero())
- args.(0)
- (rational_of_constr args.(1))))
- |"Coq.Reals.Rdefinitions.Rinv"->
- let a=(rational_of_constr args.(0)) in
+ 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)
- |"Coq.Reals.Rdefinitions.Rdiv"->
- (let b=(rational_of_constr args.(1)) in
- try (let a = (rational_of_constr args.(0)) in
- (flin_add_cste (flin_zero()) (rdiv a b)))
- with _-> (flin_add (flin_zero())
- args.(0)
- (rinv b)))
- |_->assert false)
- |_ -> assert false)
- | Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.R1" -> flin_one ()
- |"Coq.Reals.Rdefinitions.R0" -> flin_zero ()
- |_-> assert false)
+ |"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())
- c
- r1
+ 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.
*)
-(*type hineq={hname:constr; (* le nom de l'hypothèse *)
+
+(**
+ 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:constr;
- hright:constr;
+ 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_constr (h,t) =
- match (kind_of_term t) with
- App (f,args) ->
- let t1= args.(0) in
- let t2= args.(1) in
- (match kind_of_term f with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
+
+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=t1;
- hright=t2;
- hflin= flin_minus (flin_of_constr t1)
- (flin_of_constr t2);
+ hleft=arg1;
+ hright=arg2;
+ hflin= flin_minus (flin_of_term arg1)
+ (flin_of_term arg2);
hstrict=true}]
- |"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h;
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
+ [{hname=h;
htype="Rgt";
- hleft=t2;
- hright=t1;
- hflin= flin_minus (flin_of_constr t2)
- (flin_of_constr t1);
+ hleft=arg2;
+ hright=arg1;
+ hflin= flin_minus (flin_of_term arg2)
+ (flin_of_term arg1);
hstrict=true}]
- |"Coq.Reals.Rdefinitions.Rle" -> [{hname=h;
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
+ [{hname=h;
htype="Rle";
- hleft=t1;
- hright=t2;
- hflin= flin_minus (flin_of_constr t1)
- (flin_of_constr t2);
+ hleft=arg1;
+ hright=arg2;
+ hflin= flin_minus (flin_of_term arg1)
+ (flin_of_term arg2);
hstrict=false}]
- |"Coq.Reals.Rdefinitions.Rge" -> [{hname=h;
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
+ [{hname=h;
htype="Rge";
- hleft=t2;
- hright=t1;
- hflin= flin_minus (flin_of_constr t2)
- (flin_of_constr t1);
+ hleft=arg2;
+ hright=arg1;
+ hflin= flin_minus (flin_of_term arg2)
+ (flin_of_term arg1);
hstrict=false}]
- |_->assert false)
- | Ind (sp,i) ->
- (match (string_of_path sp) with
- "Coq.Init.Logic_Type.eqT" -> let t0= args.(0) in
- let t1= args.(1) in
- let t2= args.(2) in
- (match (kind_of_term t0) with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.R"->
+ |_->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=t1;
- hright=t2;
- hflin= flin_minus (flin_of_constr t1)
- (flin_of_constr t2);
+ hleft=arg1;
+ hright=arg2;
+ hflin= flin_minus (flin_of_term arg1)
+ (flin_of_term arg2);
hstrict=false};
{hname=h;
htype="eqTRL";
- hleft=t2;
- hright=t1;
- hflin= flin_minus (flin_of_constr t2)
- (flin_of_constr t1);
+ 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)
- |_-> assert 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 fourier_lineq lineq1 =
+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.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 is_int x = (x.den)=1
-;;*)
+
+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)
-;;*)
+let rec rational_to_fraction x= (x.num,x.den)
+;;
(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
*)
-(*let int_to_real n =
- let nn=abs n in
- let s=ref "" in
- if nn=0
- then s:="R0"
- else (s:="R1";
- for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
- if n<0 then s:="(Ropp "^(!s)^")";
- !s
-;;*)
+
+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
- ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))")
-;;*)
+
+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 gl (n,d) =
- let cste = pf_parse_constr gl in
- let tacn=ref (apply (cste "Rlt_zero_1")) in
- let tacd=ref (apply (cste "Rlt_zero_1")) in
- for i=1 to n-1 do
- tacn:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacn); done;
- for i=1 to d-1 do
- tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
- (tclTHENS (apply (cste "Rlt_mult_inv_pos")) [!tacn;!tacd])
-;;*)
+
+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)=
- let cste = pf_parse_constr gl in
- let tacn=ref (if n=0
- then (apply (cste "Rle_zero_zero"))
- else (apply (cste "Rle_zero_1"))) in
- let tacd=ref (apply (cste "Rlt_zero_1")) in
- for i=1 to n-1 do
- tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
- for i=1 to d-1 do
- tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
- (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
-;;*)
-
+
+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) =
- let cste = pf_parse_constr gl in
- if n=0 then (apply (cste "Rnot_lt0"))
+
+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
- (tclTHEN (apply (cste "Rle_not_lt"))
- (tac_zero_infeq_pos gl (-n,d)))
-;;*)
+ (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) =
- let cste = pf_parse_constr gl in
- (tclTHEN (apply (cste "Rlt_not_le"))
- (tac_zero_inf_pos gl (-n,d)))
+
+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 create_meta () = mkMeta(new_meta());;
+
+
+
-let my_cut c gl=
- let concl = pf_concl gl in
- apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
-;;
-let exact = exact_check;;
-
-let tac_use h = match h.htype with
- "Rlt" -> exact h.hname
- |"Rle" -> exact h.hname
- |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
- (exact h.hname))
- |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
- (exact h.hname))
- |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
- (exact h.hname))
- |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
- (exact h.hname))
- |_->assert false
+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 (kind_of_term t) with
- App (f,args) ->
- (match (string_of_constr f) with
- "Coq.Reals.Rdefinitions.Rlt" -> true
- |"Coq.Reals.Rdefinitions.Rgt" -> true
- |"Coq.Reals.Rdefinitions.Rle" -> true
- |"Coq.Reals.Rdefinitions.Rge" -> true
- |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
- "Coq.Reals.Rdefinitions.R"->true
- |_->false)
+ 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 =
- let l = Array.to_list a in
- mkApp(List.hd l, Array.of_list (List.tl l))
-;;*)
+ 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 rec fourier gl=
- let parse = pf_parse_constr gl in
- let goal = strip_outer_cast (pf_concl gl) in
- let fhyp=id_of_string "new_hyp_for_fourier" in
- (* si le but est une inéquation, on introduit son contraire,
- et le but à prouver devient False *)
- try (let tac =
- match (kind_of_term goal) with
- App (f,args) ->
- (match (string_of_constr f) with
- "Coq.Reals.Rdefinitions.Rlt" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rle" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_gt_le"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rgt" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_le_gt"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rge" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
- (intro_using fhyp))
- fourier)
- |_->assert false)
- |_->assert false
- in tac gl)
- with _ ->
-*)
- (* les hypothèses *)
-
-(*
- let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
- (list_of_sign (pf_hyps gl)) in
- let lineq =ref [] in
- List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
- with _-> ())
- hyps;
-*)
-
- (* lineq = les inéquations découlant des hypothèses *)
+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
+;;
-(*
- let res=fourier_lineq (!lineq) in
- let tac=ref tclIDTAC in
- if res=[]
- then (print_string "Tactic Fourier fails.\n";
- flush stdout)
+(* 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) (*?? ??*)
+
+;;
-*)
- (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
+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)
+;;
-(*
- else (match res with
- [(cres,sres,lc)]->
-*)
- (* lc=coefficients multiplicateurs des inéquations
- qui donnent 0<cres ou 0<=cres selon sres *)
- (*print_string "Fourier's method can prove the goal...";flush stdout;*)
-
-
-(*
- let lutil=ref [] in
- List.iter
- (fun (h,c) ->
- if c<>r0
- then (lutil:=(h,c)::(!lutil)(*;
- print_rational(c);print_string " "*)))
- (List.combine (!lineq) lc);
-
-*)
- (* on construit la combinaison linéaire des inéquation *)
-
-(*
- (match (!lutil) with
- (h1,c1)::lutil ->
- let s=ref (h1.hstrict) in
- let t1=ref (mkAppL [|parse "Rmult";
- parse (rational_to_real c1);
- h1.hleft|]) in
- let t2=ref (mkAppL [|parse "Rmult";
- parse (rational_to_real c1);
- h1.hright|]) in
- List.iter (fun (h,c) ->
+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:=(mkAppL [|parse "Rplus";
- !t1;
- mkAppL [|parse "Rmult";
- parse (rational_to_real c);
- h.hleft|] |]);
- t2:=(mkAppL [|parse "Rplus";
- !t2;
- mkAppL [|parse "Rmult";
- parse (rational_to_real c);
- h.hright|] |]))
+ 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=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
- !t1;
- !t2 |] in
- let tc=parse (rational_to_real cres) in
-*)
- (* puis sa preuve *)
-(*
- let tac1=ref (if h1.hstrict
- then (tclTHENS (apply (parse "Rfourier_lt"))
- [tac_use h1;
- tac_zero_inf_pos gl
- (rational_to_fraction c1)])
- else (tclTHENS (apply (parse "Rfourier_le"))
- [tac_use h1;
- tac_zero_inf_pos gl
- (rational_to_fraction c1)])) in
- s:=h1.hstrict;
- List.iter (fun (h,c)->
- (if (!s)
- then (if h.hstrict
- then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)]))
- else (if h.hstrict
- then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])));
- s:=(!s)||(h.hstrict))
- lutil;
- let tac2= if sres
- then tac_zero_inf_false gl (rational_to_fraction cres)
- else tac_zero_infeq_false gl (rational_to_fraction cres)
- in
- tac:=(tclTHENS (my_cut ineq)
- [tclTHEN (change_in_concl
- (mkAppL [| parse "not"; ineq|]
- ))
- (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
- else parse "Rnot_le_le"))
- (tclTHENS (Equality.replace
- (mkAppL [|parse "Rminus";!t2;!t1|]
- )
- tc)
- [tac2;
- (tclTHENS (Equality.replace (parse "(Rinv R1)")
- (parse "R1"))
-*)
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
-(*
- [tclORELSE
- (Ring.polynom [])
- tclIDTAC;
- (tclTHEN (apply (parse "sym_eqT"))
- (apply (parse "Rinv_R1")))]
-
- )
- ]));
- !tac1]);
- tac:=(tclTHENS (cut (parse "False"))
- [tclTHEN intro contradiction;
- !tac])
- |_-> assert false) |_-> assert false
- );
- ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
- (!tac gl)
- ((tclABSTRACT None !tac) gl)
-
-;;
-
-let fourier_tac x gl =
- fourier gl
-;;
-
-let v_fourier = add_tactic "Fourier" fourier_tac
+
+ 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);;
-(*open CicReduction*)
-(*open PrimitiveTactics*)
-(*open ProofEngineTypes*)
-let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
projects / helm.git / blobdiff