From: Enrico Tassi Date: Mon, 7 Oct 2002 20:40:43 +0000 (+0000) Subject: fourier_tac without useless recursion X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~56 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=73fc7a48b8abb4f68708a079630d3232f6abb584;p=helm.git fourier_tac without useless recursion --- diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index e664bc999..585513e59 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -694,7 +694,7 @@ let tcl_fail a ~status:(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 (-1) in + let num = ref 0 in let tac_list = List.map ( fun x -> num := !num + 1; match x with @@ -718,99 +718,107 @@ let contradiction_tac ~status:(proof,goal)= (* ********************* TATTICA ******************************** *) -let rec fourier ~status:(proof,goal)= - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +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(goal)^" e contesto :\n"); - debug_pcontext context; + debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); + debug_pcontext s_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 - (* 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 - "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" -> - (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" -> - (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" -> - (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 - in tac (proof,goal) ) - with _ -> - - (* les hypothèses *) + + (* here we need to negate the thesis, but to do this we nned 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 ?????*) - let new_context = superlift context 1 in - let hyps = filter_real_hyp new_context new_context in + (* fix change superlift with a real name *) + + let l_context = superlift context 1 in + let hyps = filter_real_hyp l_context l_context in + debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n"); + let lineq =ref [] in + + (* transform hyps into inequations *) + List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) with _-> ()) hyps; - (* lineq = les inéquations découlant des hypothèses *) - 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) - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) - else ( - + if res=[] then + (print_string "Tactic Fourier fails.\n";flush stdout;failwith "fourier_tac fails") + 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 " ") + (* 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 *) - - + + (* 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"; + + 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 (Cic.Appl [_Rmult;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) -> @@ -823,8 +831,10 @@ let rec fourier ~status:(proof,goal)= let tc=rational_to_real cres in - (* puis sa preuve *) + (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *) + 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