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
(* ********************* 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<cres ou 0<=cres selon sres *)
-
+
+ (* 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
- 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 " ")
+ (* 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) ->
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
projects / helm.git / commitdiff