open Fourier
-let debug x = print_string x ; flush stdout;;
+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.
*)
let ineq1_of_term (h,t) =
- match t with
+ 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 with (* match t1 *)
Cic.Const (u,boh) ->
- (match UriManager.string_of_uri u with
- "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
+ (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;
+ |"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;
+ |"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;
+ |"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)
+ |_->assert false)(* match u *)
| Cic.MutInd (u,i,o) ->
(match UriManager.string_of_uri u with
"cic:/Coq/Init/Logic_Type/eqT.con" ->
|_-> assert false)
|_-> assert 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 *)
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)
((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
;;
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 _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
+let _Rminus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
+
let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.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 _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.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_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_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_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
+let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.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 _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
+let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
+let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;;
+
+let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
+
+let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
+let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
+
+let _False = Cic.MutConstruct(UriManager.uri_of_string "cic:/Coq/Init/Datatypes/bool.ind") 0 1 0 ;;
+
+let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
+
+
+let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
+let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
+
+
+
+
let is_int x = (x.den)=1
(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
;;
+
+
+
(* preuve que 0<=n*1/d
*)
;;
-(* *********** ********** ******** ??????????????? *********** **************
+(* *********** ********** ******** ??????????????? *********** **************)
-let mkMeta proof = Cic.Meta (ProofEngineHelpers.new_meta proof) (ProofEngineHelpers.identity_relocation_list_for_metavariable []);;
+let mkMeta (proof,goal) =
+let curi,metasenv,pbo,pty = proof in
+let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+Cic.Meta (ProofEngineHelpers.new_meta proof)
+ (ProofEngineHelpers.identity_relocation_list_for_metavariable context)
+;;
-let apply_type_tac t al (proof,goals) =
- let new_m = mkMeta proof in
- PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast new_m t)::al))
+let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
+ let new_m = mkMeta (proof,goal) in
+ PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (new_m,t))::al)) ~status:(proof,goal)
;;
-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 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
+ apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,ty)) ~applist:[mkMeta(proof,goal)] ~status:(proof,goal)
;;
-*********** * ********************************* ***************************** *)
let exact = PrimitiveTactics.exact_tac;;
match c with
[] -> failwith (id^" not found in context")
| a::next -> (match a with
- Some (Cic.Name(name),Cic.Decl(t)) when name = id -> n
+ 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 (*?? bisogna invertire il contesto? ??*)
+ in
+ find_in_context_aux context 1
;;
(* mi sembra quadratico *)
-let rec filter_real_hyp context =
+let rec filter_real_hyp context cont =
match context with
[] -> []
- | Some(Cic.Name(h),Cic.Def(t))::next -> [(Cic.Rel(find_in_context h next),t)] @
- filter_real_hyp next
- | a::next -> filter_real_hyp next
+ | 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) (*?? ??*)
+
+;;
+
+(* this may not work *)
+let equality_replace a b =
+ let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in
+ PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;a;b])
+;;
+
+(* unused *)
+let tcl_fail a ~status:(proof,goal) =
+ match a with
+ 1 -> raise (ProofEngineTypes.Fail "???????")
+ |_-> (proof,[goal])
+;;
+
+
+(* !!!!! fix !!!!!!!!!! *)
+let contradiction_tac ~status:(proof,goal)=
+ proof,[goal]
+;;
+
+(* ********************* TATTICA ******************************** *)
-(* se pf_concl estrae la concl*)
let rec fourier ~status:(proof,goal)=
- debug ("invoco fourier_tac sul goal"^string_of_int(goal)^"\n");
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- (* il goal di prima dovrebbe essere ty
- let goal = strip_outer_cast (pf_concl gl) in*)
+ debug ("invoco fourier_tac sul goal "^string_of_int(goal)^" e contesto :\n");
+ debug_pcontext context;
+
+ (* il goal di prima dovrebbe essere ty
+
+ let goal = strip_outer_cast (pf_concl gl) in *)
- let fhyp = String.copy "new_hyp_for_fourier" in
+ let fhyp = String.copy "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 ty with
- Cic.Appl ( Cic.Const(u,boh)::args) ->
- (match UriManager.string_of_uri u with
+ try (let tac =
+ match ty with
+ Cic.Appl ( Cic.Const(u,boh)::args) ->
+ (match UriManager.string_of_uri u with
"cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
(Tacticals.then_
~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt)
~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
(Tacticals.then_
~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le)
~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
(Tacticals.then_
~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt)
~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
(Tacticals.then_
~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge)
~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
~continuation:fourier)
- |_->assert false)
- |_->assert false
+ |_->assert false)
+ |_->assert false
in tac (proof,goal) )
- with _ ->
+ with _ ->
(* les hypothèses *)
-
(* ? fix if None ?????*)
- debug ("estraggo hp da context "^ string_of_int(List.length context)^"\n");
- let hyps = filter_real_hyp context in
- debug ("trasformo in eq "^ string_of_int (List.length hyps)^"\n");
- let lineq =ref [] in
- List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
+ let new_context = superlift context 1 in
+ let hyps = filter_real_hyp new_context new_context in
+ debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
+ let lineq =ref [] in
+ List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
with _-> ())
hyps;
(* lineq = les inéquations découlant des hypothèses *)
- debug ("applico fourier a "^ string_of_int (List.length !lineq)^"\n");
+ debug ("applico fourier a "^ string_of_int (List.length !lineq)^" disequazioni\n");
- let res=fourier_lineq (!lineq) in
- (*let tac=ref tclIDTAC in*)
- if res=[]
- then (print_string "Tactic Fourier fails.\n";
- flush stdout)
-;debug "fine\n";
-;(proof,[goal])
-;;
+ let res=fourier_lineq (!lineq) in
+ let tac=ref Ring.id_tac in
+ if res=[] then (print_string "Tactic Fourier fails.\n";flush stdout)
(* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
-
-(*
- 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);
-
-*)
+ else (
+
+ match res with (*match res*)
+ [(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...\n";flush stdout;
+
+
+ let lutil=ref [] in
+ debug "I coeff di moltiplicazione rit sono: ";
+ List.iter
+ (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
+ Fourier.print_rational(c);print_string " ")
+ )
+ (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
- (h1,c1)::lutil ->
+
+ (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 (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
+ (* 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*)
+ 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
-*)
+
+ let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
+ let tc=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)
+ debug "inizio a costruire tac1\n";
+ let tac1=ref ( if h1.hstrict then
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt)
+ ~continuations:[tac_use h1;tac_zero_inf_pos goal
+ (rational_to_fraction c1)])
+ else
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
+ ~continuations:[tac_use h1;tac_zero_inf_pos goal
+ (rational_to_fraction c1)]))
+ in
+ s:=h1.hstrict;
+
+ List.iter (fun (h,c) ->
+ (if (!s) then
+ (if h.hstrict then
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_lt_lt)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (rational_to_fraction c)])
+ else
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_lt_le)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (rational_to_fraction c)])
+ )
+ else
+ (if h.hstrict then
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (rational_to_fraction c)])
+ else
+ tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos goal
+ (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:=(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"))
-*)
+ tac:=(Tacticals.thens ~start:(my_cut ~term:ineq)
+ ~continuations:[Tacticals.then_ (* ?????????????????????????????? *)
+ ~start:(PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq] ))
+ ~continuation:(Tacticals.then_
+ ~start:(PrimitiveTactics.apply_tac
+ ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
+ ~continuation:(Tacticals.thens
+ ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
+ ~continuations:[tac2;(Tacticals.thens
+ ~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
+ ~continuations:
(* 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")))]
+ [Tacticals.try_tactics
+ (* ???????????????????????????? *)
+ ~tactics:[ "ring", Ring.ring_tac ; "id", Ring.id_tac]
+ ;
+ Tacticals.then_
+ ~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
+ ~continuation:(PrimitiveTactics.apply_tac ~term:_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)
+ ] (* end continuations before comment *)
+ )
+ );
+ !tac1]
+ );(*end tac:=*)
+ tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False)
+ ~continuations:[Tacticals.then_
+ (* ???????????????????????????????
+ in coq era intro *)
+ ~start:(PrimitiveTactics.intros_tac ~name:(String.copy "??"))
+ (* ????????????????????????????? *)
+
+ ~continuation:contradiction_tac;!tac])
-;;
-let fourier_tac x gl =
- fourier gl
-;;
+ |_-> assert false)(*match (!lutil) *)
+ |_-> assert false); (*match res*)
-let v_fourier = add_tactic "Fourier" fourier_tac
-*)
+ debug ("finalmente applico t1\n");
+ (!tac ~status:(proof,goal))
+
+;;
-(*open CicReduction*)
-(*open PrimitiveTactics*)
-(*open ProofEngineTypes*)
-let fourier_tac ~status:(proof,goal) = ignore(fourier (proof,goal)) ; (proof,[goal]) ;;
+let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
projects / helm.git / commitdiff