From 251e2f428031db12bae815fb56862e3b6384f0f8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Nov 2002 11:59:11 +0000 Subject: [PATCH] - porting to the new theory with explicit named substitutions completed - bug fixed: fold used to undo an over-simplification of RewriteSimpl --- helm/gTopLevel/fourierR.ml | 310 +++++++++++++++++-------------------- 1 file changed, 141 insertions(+), 169 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 247a47248..bdba62319 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,9 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); (proof',[fresh_meta]) ;; -let rewrite_simpl_tac ~term = - Tacticals.then_ ~start:(rewrite_tac ~term) - ~continuation:ReductionTactics.simpl_tac + +let rewrite_simpl_tac ~term ~status = + Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:ReductionTactics.simpl_tac ~status ;; (******************** THE FOURIER TACTIC ***********************) @@ -198,23 +198,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 @@ -491,143 +474,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") [] ;; (******************************************************************************) @@ -768,16 +694,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 + ~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 +*) ;; @@ -1214,6 +1167,7 @@ theoreme,so let's parse our thesis *) 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? + CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac ~continuations:[Tacticals.then_ ~start:( fun ~status:(proof,goal as status) -> @@ -1236,9 +1190,27 @@ theoreme,so let's parse our thesis *) r) ; "id", Tacticals.id_tac] ]) -(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *) - ;tac2])) - ;!tac1]);(*end 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 + (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*) + 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:=*) tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False) ~continuations:[Tacticals.then_ -- 2.39.2