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")
+ let str = ref "" in
+ List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
+ a ^ " " | _ ->()) x ;
+ debug ("contesto : "^ (!str) ^ "\n")
;;
(******************************************************************************
_ -> (flin_add (flin_zero()) arg2 a)
end
with
- _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
+ _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
end
|"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
let a=(rational_of_term (List.hd next)) in
h.hflin.fhom;
((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");
+ debug ("chiamo unsolvable sul sistema di "^
+ string_of_int (List.length sys) ^"\n");
print_sys sys;
unsolvable sys
;;
-(******************************************************************************
+(*****************************************************************************
Construction de la preuve en cas de succès de la méthode de Fourier,
i.e. on obtient une contradiction.
*)
-let _eqT = Cic.MutInd(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
-let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
-let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;;
-let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
-let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
-let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.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 _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.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_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
-let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_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_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_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_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
-let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
-let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
-let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
-let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
-let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
-let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
-let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
-let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
-let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
-let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
-let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
-let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
-let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
-let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
-let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
-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 _Rminus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
-let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
-let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
-let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
-let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.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 _sym_eqT = Cic.Const(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
-(*****************************************************************************************************)
+let _eqT = Cic.MutInd(UriManager.uri_of_string
+ "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
+let _False = Cic.MutInd (UriManager.uri_of_string
+ "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
+let _not = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Init/Logic/not.con") 0;;
+let _R0 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
+let _R1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
+let _R = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/R.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 _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.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_le=Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
+let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le_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_lt=Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_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_lt_lt =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
+let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
+let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
+let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
+let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
+let _Rinv = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
+let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
+ "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
+let _Rle = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
+let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
+let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
+let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
+let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
+let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
+let _Rlt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
+let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
+let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
+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 _Rminus = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
+let _Rmult = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
+let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
+let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
+let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.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 _sym_eqT = Cic.Const(UriManager.uri_of_string
+ "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
+
+(******************************************************************************)
+
let is_int x = (x.den)=1
;;
(* preuve que 0<n*1/d
*)
-
-(*
-let tac_zero_inf_pos gl (n,d) =
- (*let cste = pf_parse_constr gl in*)
- let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
- let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
- for i=1 to n-1 do
- tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
- for i=1 to d-1 do
- tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
- (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
-;;*)
let tac_zero_inf_pos (n,d) ~status =
(*let cste = pf_parse_constr gl in*)
let pall str ~status:(proof,goal) t =
debug ("ty = "^ CicPp.ppterm ty^"\n");
in
let tacn=ref
- (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
+ (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
+ PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
let tacd=ref
- (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
+ (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
+ PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
for i=1 to n-1 do
- tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) ~status _Rlt_zero_pos_plus1;PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacn); done;
- for i=1 to d-1 do
- tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); done;
+ tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
+ ~status _Rlt_zero_pos_plus1;
+ PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
+ ~continuation:!tacn);
+ done;
+ for i=1 to d-1 do
+ tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
+ ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
+ ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
+ done;
(* preuve que 0<=n*1/d
*)
-let tac_zero_infeq_pos gl (n,d) =
- (*let cste = pf_parse_constr gl in*)
- let tacn = ref (if n=0 then
- (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
- else
- (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
- in
- let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
- for i=1 to n-1 do
- tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
- for i=1 to d-1 do
- tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
- (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
+let tac_zero_infeq_pos gl (n,d) ~status =
+ (*let cste = pf_parse_constr gl in*)
+ debug("inizio tac_zero_infeq_pos\n");
+ let tacn = ref
+ (if n=0 then
+ (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
+ else
+ (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
+ )
+ in
+ let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
+ for i=1 to n-1 do
+ tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
+ done;
+ for i=1 to d-1 do
+ tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
+ done;
+ let r =
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
+ debug("fine tac_zero_infeq_pos\n");
+ r
;;
(* preuve que 0<(-n)*(1/d) => False
*)
-let tac_zero_inf_false gl (n,d) =
- if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
+let tac_zero_inf_false gl (n,d) ~status=
+debug("inizio tac_zero_inf_false\n");
+ if n=0 then
+ (debug "1\n";let r = (PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
+ debug("fine\n");
+ r)
else
- (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
- ~continuation:(tac_zero_infeq_pos gl (-n,d)))
+ (debug "2\n";let r = (Tacticals.then_ ~start:(
+ fun ~status:(proof,goal as status) ->
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+
+ debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
+ ^ CicPp.ppterm ty ^"\n");
+
+ let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
+
+ debug("!!!!!!!!!2\n");
+ r
+
+ )
+
+ ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
+ debug("fine\n");
+ r
+ )
;;
(* preuve que 0<=(-n)*(1/d) => False
*)
-let tac_zero_infeq_false gl (n,d) =
+let tac_zero_infeq_false gl (n,d) ~status=
+debug("stat tac_zero_infeq_false");
+let r =
(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
- ~continuation:(tac_zero_inf_pos (-n,d)))
+ ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
+ debug("stat tac_zero_infeq_false");
+ r
;;
let metasenv' = (fresh_meta,context,t)::metasenv in
let proof' = curi,metasenv',pbo,pty in
let proof'',goals =
- PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) ~status:(proof',goal)
+ PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta
+ (fresh_meta,irl),t))::al)) ~status:(proof',goal)
in
proof'',fresh_meta::goals
;;
let metasenv' = (fresh_meta,context,c)::metasenv in
let proof' = curi,metasenv',pbo,pty in
let proof'',goals =
- apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] ~status:(proof',goal)
+ apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
+ CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
+ ~status:(proof',goal)
in
(* We permute the generated goals to be consistent with Coq *)
match goals with
match h.htype with
"Rlt" -> exact ~term:h.hname ~status
|"Rle" -> exact ~term:h.hname ~status
- |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
- ~continuation:(exact ~term:h.hname)) ~status
- |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
- ~continuation:(exact ~term:h.hname)) ~status
- |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
- ~continuation:(exact ~term:h.hname)) ~status
- |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
- ~continuation:(exact ~term:h.hname)) ~status
+ |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_gt_to_lt)
+ ~continuation:(exact ~term:h.hname)) ~status
+ |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_ge_to_le)
+ ~continuation:(exact ~term:h.hname)) ~status
+ |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_eqLR_to_le)
+ ~continuation:(exact ~term:h.hname)) ~status
+ |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_eqRL_to_le)
+ ~continuation:(exact ~term:h.hname)) ~status
|_->assert false
in
debug("Fine TAC_USE\n");
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)
+ | 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) (*?? ??*)
;;
let equality_replace a b ~status =
+debug("inizio EQ\n");
let module C = Cic in
let proof,goal = status in
let curi,metasenv,pbo,pty = proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
+debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) =
rewrite_tac ~term:(C.Meta (fresh_meta,irl))
~status:((curi,metasenv',pbo,pty),goal)
in
- (proof,fresh_meta::goals)
+ let new_goals = fresh_meta::goals in
+debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "^string_of_int( List.length goals)^"+ meta\n");
+ (proof,new_goals)
;;
let tcl_fail a ~status:(proof,goal) =
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
+ 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 *)
+(* here we need to negate the thesis, but to do this we need 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?? *)
+ 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 *)
~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
+ 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;
hyps;
- debug ("applico fourier a "^ string_of_int (List.length !lineq)^" disequazioni\n");
+ 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")
+ (print_string "Tactic Fourier fails.\n";flush stdout;
+ failwith "fourier_tac fails")
else
(
match res with (*match res*)
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 *))
+ (* 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");
+ print_string (" quindi lutil e' lunga "^
+ string_of_int (List.length (!lutil))^"\n");
(* on construit la combinaison linéaire des inéquation *)
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 (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
List.iter (fun (h,c) ->
s:=(!s)||(h.hstrict);
- 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] ]))
+ 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=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
let tc=rational_to_real cres in
- (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
+(* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
debug "inizio a costruire tac1\n";
Fourier.print_rational(c1);
let tac1=ref ( fun ~status ->
- debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n");
+ debug ("Sotto tattica t1 "^(if h1.hstrict
+ then "strict" else "lasc")^"\n");
if h1.hstrict then
(Tacticals.thens ~start:(
fun ~status ->
debug ("inizio t1 strict\n");
let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = List.find
+ (function (m,_,_) -> m=goal) metasenv in
debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
- PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
+ PrimitiveTactics.apply_tac ~term:_Rfourier_lt
+ ~status)
~continuations:[tac_use h1;
- tac_zero_inf_pos (rational_to_fraction c1)] ~status
+ tac_zero_inf_pos
+ (rational_to_fraction c1)] ~status
)
else
- (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
- ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status))
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_le)
+ ~continuations:
+ [tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status))
in
s:=h1.hstrict;
(if (!s) then
(if h.hstrict then
(debug("tac1 1\n");
- tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
- ~term:_Rfourier_lt_lt)
- ~continuations:[!tac1;tac_use h;
- tac_zero_inf_pos
- (rational_to_fraction c)]))
+ tac1:=(Tacticals.thens
+ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_lt_lt)
+ ~continuations:[!tac1;tac_use h;
+ tac_zero_inf_pos
+ (rational_to_fraction c)]))
else
(
debug("tac1 2\n");
~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)
+ ~start:(
+
+ fun ~status ->
+ let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc ~status
+ in
+ (match r with (p,gl) ->
+ debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
+
+ r
+
+ )
~continuations:[(*tac2;*)(Tacticals.thens
- ~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
+ ~start:(
+ fun ~status ->
+ let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
+ (match r with (p,gl) ->
+ debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));r
+
+ )
~continuations:
- [
- (*
- 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)
- ;
- Tacticals.try_tactics
- (* ???????????????????????????? *)
- ~tactics:[ "ring", Ring.ring_tac ; "id", Ring.id_tac]
-
- ]
+ (* ******* *)
+ [
+ Tacticals.then_
+ ~start:(
+ fun ~status:(proof,goal as status) ->
+ debug("ECCOCI\n");
+
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+
+ debug("ty = "^CicPp.ppterm ty^"\n");
+
+ let r = PrimitiveTactics.apply_tac ~term:_sym_eqT ~status in
+ debug("fine ECCOCI\n");
+ r
+ )
+ ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
+
+
+ ;
+ Tacticals.try_tactics
+ (* ???????????????????????????? *)
+ ~tactics:[ "ring",
+
+ (fun ~status ->
+ debug("begin RING\n");
+ let r = Ring.ring_tac ~status in
+ debug ("end RING\n");
+ r)
+
+
+ ; "id", Ring.id_tac]
+
+ ]
- )
- ;tac2 ] (* end continuations before comment *)
+ );tac2(* < order *)
+ ] (* end continuations before comment *)
)
);
!tac1]
~continuations:[Tacticals.then_
(* ???????????????????????????????
in coq era intro *)
- ~start:(PrimitiveTactics.intros_tac ~name:(String.copy "??"))
+ ~start:(PrimitiveTactics.intros_tac ~name:"??")
(* ????????????????????????????? *)
~continuation:contradiction_tac;!tac])
;;
let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
+
+
+let simpl_tac ~status:(proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+
+prerr_endline("simpl_tac su "^CicPp.ppterm ty);
+
+ let new_ty = ProofEngineReduction.simpl context ty in
+
+prerr_endline("ritorna "^CicPp.ppterm new_ty);
+
+ let new_metasenv =
+ List.map
+ (function
+ (n,_,_) when n = metano -> (metano,context,new_ty)
+ | _ as t -> t
+ ) metasenv
+ in
+ (curi,new_metasenv,pbo,pty), [metano]
+
+;;
+
+let rewrite_simpl_tac ~term ~status =
+
+ Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status
+
+;;
projects / helm.git / commitdiff