let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
let eq_ind_r,ty,t1,t2 =
match CicTypeChecker.type_of_aux' metasenv context equality with
- C.Appl [C.MutInd (uri,0,_) ; ty ; t1 ; t2]
+ C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
let eq_ind_r =
C.Const
(U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
in
eq_ind_r,ty,t1,t2
- | C.Appl [C.MutInd (uri,0,_) ; ty ; t1 ; t2]
+ | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
let eqT_ind_r =
C.Const
;;
-
-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
-
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+ ~continuation:
+ (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+ ~status
;;
(******************** THE FOURIER TACTIC ***********************)
@param c a rational
@return the new flin
*)
-let flin_add f x c =
- let cx = flin_coef f x in
- Hashtbl.remove f.fhom x;
- Hashtbl.add f.fhom x (rplus cx c);
- f
+let flin_add f x c =
+ match x with
+ Cic.Rel(n) ->(
+ let cx = flin_coef f x in
+ Hashtbl.remove f.fhom x;
+ Hashtbl.add f.fhom x (rplus cx c);
+ f)
+ |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
+ let cx = flin_coef f x in
+ Hashtbl.remove f.fhom x;
+ Hashtbl.add f.fhom x (rplus cx c);
+ f
;;
(**
Adds c to f.fcste
;;
(**
- @return f times a
+ @return a times f
*)
let flin_emult a f =
let f2 = flin_zero() in
(*****************************************************************************)
-(**
- @param t a term
- @return proiection on string of t
-*)
-let rec string_of_term t =
- match t with
- Cic.Cast (t,_) -> string_of_term t
- |Cic.Const (u,_) -> UriManager.string_of_uri u
- |Cic.Var (u,_) -> UriManager.string_of_uri u
- | _ -> "not_of_constant"
-;;
-
-(* coq wrapper
-let string_of_constr = string_of_term
-;;
-*)
-
(**
@param t a term
@raise Failure if conversion is impossible
(* coq wrapper
let rational_of_const = rational_of_term;;
*)
-
+let fails f a =
+ try
+ let tmp = (f a) in
+ false
+ with
+ _-> true
+ ;;
let rec flin_of_term t =
let fl_of_binop f l =
let arg1 = (List.hd next) and
arg2 = (List.hd(List.tl next))
in
- try
+ if fails rational_of_term arg1
+ then
+ if fails rational_of_term arg2
+ then
+ ( (* prodotto tra 2 incognite ????? impossibile*)
+ failwith "Sistemi lineari!!!!\n"
+ )
+ else
+ (
+ match arg1 with
+ Cic.Rel(n) -> (*trasformo al volo*)
+ (flin_add (flin_zero()) arg1 (rational_of_term arg2))
+ |_-> (* test this *)
+ let tmp = flin_of_term arg1 in
+ flin_emult (rational_of_term arg2) (tmp)
+ )
+ else
+ if fails rational_of_term arg2
+ then
+ (
+ match arg2 with
+ Cic.Rel(n) -> (*trasformo al volo*)
+ (flin_add (flin_zero()) arg2 (rational_of_term arg1))
+ |_-> (* test this *)
+ let tmp = flin_of_term arg2 in
+ flin_emult (rational_of_term arg1) (tmp)
+
+ )
+ else
+ ( (*prodotto tra razionali*)
+ (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
+ )
+ (*try
begin
- let a = rational_of_term arg1 in
+ (*let a = rational_of_term arg1 in
+ debug("ho fatto rational of term di "^CicPp.ppterm arg1^
+ " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
+ let a = flin_of_term arg1
try
begin
let b = (rational_of_term arg2) in
+ debug("ho fatto rational of term di "^CicPp.ppterm arg2^
+ " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
(flin_add_cste (flin_zero()) (rmult a b))
end
with
- _ -> (flin_add (flin_zero()) arg2 a)
+ _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
+ (flin_add (flin_zero()) arg2 a)
end
with
- _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
+ _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
+ (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
|_-> assert false
end
|_-> assert false)
- with _ -> flin_add (flin_zero()) t r1
+ with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
;;
(* coq wrapper
|_->assert false)(* match u *)
| Cic.MutInd (u,i,o) ->
(match UriManager.string_of_uri u with
- "cic:/Coq/Init/Logic_Type/eqT.con" ->
+ "cic:/Coq/Init/Logic_Type/eqT.ind" ->
let t0= arg1 in
let arg1= arg2 in
let arg2= List.hd(List.tl (List.tl next)) in
Hashtbl.iter (fun x c ->
try (Hashtbl.find hvar x;())
with _-> nvar:=(!nvar)+1;
- Hashtbl.add hvar x (!nvar))
+ Hashtbl.add hvar x (!nvar);
+ debug("aggiungo una var "^
+ string_of_int !nvar^" per "^
+ CicPp.ppterm x^"\n"))
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)
+ Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
h.hflin.fhom;
((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
lineq1 in
*)
-let _eqT =
- Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [];;
-let _False =
- Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [];;
-let _not =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") [];;
-let _R0 =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") [];;
-let _R1 =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") [];;
-let _R =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") [];;
-let _Rfourier_eqLR_to_le=
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [];;
-let _Rfourier_eqRL_to_le =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [];;
-let _Rfourier_ge_to_le =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [];;
-let _Rfourier_gt_to_lt =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [];;
-let _Rfourier_le =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con")[];;
-let _Rfourier_le_le =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con")
- [];;
-let _Rfourier_le_lt =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con")
- [] ;;
-let _Rfourier_lt =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") []
-;;
-let _Rfourier_lt_le =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con")
- []
-;;
-let _Rfourier_lt_lt =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con")
- []
-;;
-let _Rfourier_not_ge_lt =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [];;
-let _Rfourier_not_gt_le =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [];;
-let _Rfourier_not_le_gt =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [];;
-let _Rfourier_not_lt_ge =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [];;
-let _Rinv =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con")[];;
-let _Rinv_R1 =
- Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [];;
-let _Rle =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") [];;
-let _Rle_mult_inv_pos =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [];;
-let _Rle_not_lt =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [];;
-let _Rle_zero_1 =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [];;
-let _Rle_zero_pos_plus1 =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [];;
-let _Rle_zero_zero =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con")
- []
-;;
-let _Rlt =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") [];;
-let _Rlt_mult_inv_pos =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [];;
-let _Rlt_not_le =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [];;
-let _Rlt_zero_1 =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [];;
-let _Rlt_zero_pos_plus1 =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [];;
-let _Rminus =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con")
- []
-;;
-let _Rmult =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con")
- []
-;;
-let _Rnot_le_le =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [];;
-let _Rnot_lt0 =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [];;
-let _Rnot_lt_lt =
- Cic.Const
- (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [];;
-let _Ropp =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") []
-;;
-let _Rplus =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") []
-;;
-let _sym_eqT =
- Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") [];;
+let _eqT = Cic.MutInd(UriManager.uri_of_string
+ "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [] ;;
+let _False = Cic.MutInd (UriManager.uri_of_string
+ "cic:/Coq/Init/Logic/False.ind") 0 [] ;;
+let _not = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Init/Logic/not.con") [];;
+let _R0 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/R0.con") [] ;;
+let _R1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/R1.con") [] ;;
+let _R = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/R.con") [] ;;
+let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [] ;;
+let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [] ;;
+let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [] ;;
+let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [] ;;
+let _Rfourier_le=Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") [] ;;
+let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") [] ;;
+let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") [] ;;
+let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") [] ;;
+let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") [] ;;
+let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") [] ;;
+let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [] ;;
+let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [] ;;
+let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [] ;;
+let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [] ;;
+let _Rinv = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rinv.con") [] ;;
+let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
+ "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [] ;;
+let _Rle = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rle.con") [] ;;
+let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [] ;;
+let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [] ;;
+let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;;
+let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;;
+(*let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;*)
+let _Rlt = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;;
+let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [] ;;
+let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [] ;;
+let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [] ;;
+let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [] ;;
+let _Rminus = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rminus.con") [] ;;
+let _Rmult = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rmult.con") [] ;;
+let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [] ;;
+let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [] ;;
+let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [] ;;
+let _Ropp = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Ropp.con") [] ;;
+let _Rplus = Cic.Const (UriManager.uri_of_string
+ "cic:/Coq/Reals/Rdefinitions/Rplus.con") [] ;;
(******************************************************************************)
(*let cste = pf_parse_constr gl in*)
debug("inizio tac_zero_infeq_pos\n");
let tacn = ref
- (if n=0 then
+ (*(if n=0 then
(PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
- else
+ 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
)
;;
-(* preuve que 0<=(-n)*(1/d) => False
+(* preuve que 0<=n*(1/d) => False ; n est negatif
*)
-let tac_zero_infeq_false gl (n,d) ~status=
-debug("stat tac_zero_infeq_false");
+let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
+debug("stat tac_zero_infeq_false\n");
let r =
- (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
- ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
- debug("stat tac_zero_infeq_false");
- r
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+
+ debug("faccio fold di " ^ CicPp.ppterm
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+ ]
+ ) ^ "\n") ;
+ debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
+ (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
+ Tacticals.then_
+ ~start:
+ (ReductionTactics.fold_tac ~also_in_hypotheses:false
+ ~term:
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+ ]
+ )
+ )
+ ~continuation:
+ (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+ ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
+ debug("end tac_zero_infeq_false\n");
+ r
+(*PORTING
+ Tacticals.id_tac ~status
+*)
;;
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)) (* ??? *)*)
+ ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
+ ~status:(proof',goal)
in
proof'',fresh_meta::goals
;;
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+debug("my_cut di "^CicPp.ppterm c^"\n");
+
+
let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
| _ -> c
;;
-let find_in_context id context =
+(*let find_in_context id context =
let rec find_in_context_aux c n =
match c with
[] -> failwith (id^" not found in context")
[] -> []
| Some(Cic.Name(h),Cic.Decl(t))::next -> (
let n = find_in_context h cont in
+ debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
[(Cic.Rel(n),t)] @ filter_real_hyp next cont)
| a::next -> debug(" no\n"); filter_real_hyp next cont
+;;*)
+let filter_real_hyp context _ =
+ let rec filter_aux context num =
+ match context with
+ [] -> []
+ | Some(Cic.Name(h),Cic.Decl(t))::next ->
+ (
+ (*let n = find_in_context h cont in*)
+ debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
+ [(Cic.Rel(num),t)] @ filter_aux next (num+1)
+ )
+ | a::next -> filter_aux next (num+1)
+ in
+ filter_aux context 1
;;
+
(* lifts everithing at the conclusion level *)
let rec superlift c n=
match c with
(* !!!!! fix !!!!!!!!!! *)
let contradiction_tac ~status:(proof,goal)=
Tacticals.then_
- ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
+ ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
~continuation:(Tacticals.then_
~start:(Ring.elim_type_tac ~term:_False)
~continuation:(assumption_tac))
" disequazioni\n");
let res=fourier_lineq (!lineq) in
- let tac=ref Ring.id_tac in
+ let tac=ref Tacticals.id_tac in
if res=[] then
(print_string "Tactic Fourier fails.\n";flush stdout;
failwith "fourier_tac fails")
in
tac:=(Tacticals.thens
~start:(my_cut ~term:ineq)
- ~continuations:[Tacticals.then_
+ ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)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)
~continuation:(Tacticals.thens
~start:(
fun ~status ->
+ debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
~status
in
r)
~continuations:
[PrimitiveTactics.apply_tac ~term:_Rinv_R1
-(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
- di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
- parametri della equality_replace vengono passati al contrario? Oppure la
- tattica usa i parametri al contrario?
- ~continuations:[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]
+ ; "id", Tacticals.id_tac]
])
-(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
- ;tac2]))
- ;!tac1]);(*end tac:=*)
- tac:=(Tacticals.thens
- ~start:(PrimitiveTactics.cut_tac ~term:_False)
- ~continuations:[Tacticals.then_
- ~start:(PrimitiveTactics.intros_tac ~name:"??")
- ~continuation:contradiction_tac
- ;!tac])
-
+ ;(*Tacticals.id_tac*)
+ 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
+ (* check if ty is of type *)
+ let w1 =
+ debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
+ (match ty with
+ Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
+ |_ -> assert false)
+ in
+ let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
+ debug("fine MY_CHNGE\n");
+ r
+
+ )
+ ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
+ ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
|_-> assert false)(*match (!lutil) *)
|_-> assert false); (*match res*)
debug ("finalmente applico tac\n");
- (!tac ~status:(proof,goal))
+ (
+ let r = !tac ~status:(proof,goal) in
+ debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
+
+ )
;;
let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
projects / helm.git / blobdiff