+
+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 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 ?????*)
+ (* 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;
+
+
+ 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_tac fails")
+ 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";
+