X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=f6f44e950fe961ce3c7b4f6bb8dd771447b1c1a9;hb=1e2b0bee559e543455ff839d969c5778d5c353bd;hp=c8c856459d4ebd65d7cdca91af4ae019d0484bd5;hpb=3066e4dcb7270a5eb20020a91d45da9eb87e2f2e;p=helm.git diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index c8c856459..f6f44e950 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -33,14 +33,14 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = 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 @@ -78,9 +78,12 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); (proof',[fresh_meta]) ;; -let rewrite_simpl_tac ~term = + +let rewrite_simpl_tac ~term ~status = Tacticals.then_ ~start:(rewrite_tac ~term) - ~continuation:ReductionTactics.simpl_tac + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status ;; (******************** THE FOURIER TACTIC ***********************) @@ -143,11 +146,18 @@ let flin_coef f x = @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 @@ -186,7 +196,7 @@ let flin_minus f1 f2 = ;; (** - @return f times a + @return a times f *) let flin_emult a f = let f2 = flin_zero() in @@ -198,23 +208,6 @@ let flin_emult a f = (*****************************************************************************) -(** - @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 @@ -262,7 +255,13 @@ let rec rational_of_term t = (* 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 = @@ -290,19 +289,59 @@ let rec flin_of_term t = 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 @@ -330,7 +369,7 @@ let rec flin_of_term t = |_-> 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 @@ -408,7 +447,7 @@ let ineq1_of_term (h,t) = |_->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 @@ -468,14 +507,17 @@ let fourier_lineq lineq1 = 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 @@ -491,143 +533,86 @@ i.e. on obtient une contradiction. *) -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") [] ;; (******************************************************************************) @@ -718,11 +703,11 @@ 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 + (*(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 @@ -768,16 +753,43 @@ let tac_zero_inf_false gl (n,d) ~status= ) ;; -(* 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 +*) ;; @@ -792,8 +804,10 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = 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 ;; @@ -806,6 +820,9 @@ let my_cut ~term:c ~status:(proof,goal)= 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 @@ -886,7 +903,7 @@ let rec strip_outer_cast c = match c with | _ -> 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") @@ -904,10 +921,26 @@ let rec filter_real_hyp context cont = [] -> [] | 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 @@ -967,7 +1000,7 @@ let assumption_tac ~status:(proof,goal)= (* !!!!! 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)) @@ -1048,7 +1081,7 @@ theoreme,so let's parse our thesis *) " 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") @@ -1182,7 +1215,7 @@ theoreme,so let's parse our thesis *) 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) @@ -1195,6 +1228,7 @@ theoreme,so let's parse our thesis *) ~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 @@ -1210,47 +1244,45 @@ theoreme,so let's parse our thesis *) 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);;