From: Enrico Tassi Date: Wed, 2 Oct 2002 17:08:50 +0000 (+0000) Subject: tactic update X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~62 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1febf21f7c0f7ce0556839580e0914161b965543;p=helm.git tactic update --- diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml index bb8b4ea13..c1a40e6e1 100644 --- a/helm/gTopLevel/fourier.ml +++ b/helm/gTopLevel/fourier.ml @@ -21,10 +21,16 @@ Pages: 326-327 http://gallica.bnf.fr/ *) + + + (* Un peu de calcul sur les rationnels... Les opérations rendent des rationnels normalisés, i.e. le numérateur et le dénominateur sont premiers entre eux. *) + + + type rational = {num:int; den:int} ;; @@ -202,4 +208,4 @@ let test2=[ deduce test2;; unsolvable test2;; -*) \ No newline at end of file +*) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 7e66efa49..21f1d5b33 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -32,7 +32,13 @@ des in 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. @@ -299,42 +305,46 @@ type hineq={hname:Cic.term; (* le nom de l'hypoth *) 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" -> @@ -362,8 +372,8 @@ let ineq1_of_term (h,t) = |_-> 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;; @@ -372,6 +382,24 @@ 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 *) @@ -382,6 +410,8 @@ let fourier_lineq lineq1 = 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) @@ -389,6 +419,7 @@ let fourier_lineq lineq1 = ((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 ;; @@ -410,6 +441,8 @@ let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier 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 ;; @@ -420,10 +453,34 @@ let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/ 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 @@ -474,6 +531,9 @@ let tac_zero_inf_pos gl (n,d) = (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd]) ;; + + + (* preuve que 0<=n*1/d *) @@ -513,26 +573,30 @@ let tac_zero_infeq_false gl (n,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;; @@ -587,223 +651,250 @@ let find_in_context id context = 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 - 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 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);;