From 50d48fe8a3c70e70bf2f06b60dfa3a6b8c121b6b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Oct 2002 19:40:37 +0000 Subject: [PATCH] Debug printing update, now the unification bug seems to be in tac_zero_inf_pos. We get '0 < 1 + 0' instead of '0 < 1'. --- helm/gTopLevel/fourierR.ml | 171 ++++++++++++++++++++++--------------- 1 file changed, 103 insertions(+), 68 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 446b2ef4b..5fa371030 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -428,62 +428,48 @@ Construction de la preuve en cas de succ i.e. on obtient une contradiction. *) -let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 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 _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.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 _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 _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.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_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_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_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;; -let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.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 _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;; -let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;; -let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;; - let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;; - -let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;; -let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;; - -let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;; - -let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;; - - -let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;; -let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;; - - - - - - +(*****************************************************************************************************) let is_int x = (x.den)=1 ;; @@ -521,6 +507,8 @@ let rational_to_real x = (* preuve que 0 m=goal) metasenv in + debug ("th = "^ CicPp.ppterm t ^"\n"); + 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 + let tacd=ref + (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; + + + +debug("\nTAC ZERO INF POS\n"); + +(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) + ~continuations:[ + !tacn ; + !tacd ] + ~status) +;; + (* preuve que 0<=n*1/d @@ -570,7 +587,7 @@ let tac_zero_inf_false gl (n,d) = let tac_zero_infeq_false gl (n,d) = (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos gl (-n,d))) + ~continuation:(tac_zero_inf_pos (-n,d))) ;; @@ -615,18 +632,24 @@ let my_cut ~term:c ~status:(proof,goal)= let exact = PrimitiveTactics.exact_tac;; -let tac_use h = match h.htype with - "Rlt" -> exact ~term:h.hname - |"Rle" -> exact ~term:h.hname - |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) - |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) - ~continuation:(exact ~term:h.hname)) - |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) - ~continuation:(exact ~term:h.hname)) - |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) - ~continuation:(exact ~term:h.hname)) - |_->assert false +let tac_use h ~status = +debug("Inizio TC_USE\n"); +let res = +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 + |_->assert false +in +debug("Fine TAC_USE"); +res ;; @@ -863,43 +886,55 @@ let rec fourier ~status:(s_proof,s_goal)= debug "inizio a costruire tac1\n"; - let tac1=ref ( if h1.hstrict then + let tac1=ref ( fun ~status -> + debug "Sotto tattica t1\n"; + if h1.hstrict then (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt) - ~continuations:[tac_use h1;tac_zero_inf_pos goal - (rational_to_fraction c1)]) + ~continuations:[tac_use h1;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 goal - (rational_to_fraction c1)])) + ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status)) + in s:=h1.hstrict; List.iter (fun (h,c) -> (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 goal - (rational_to_fraction c)]) + tac_zero_inf_pos + (rational_to_fraction c)])) else + ( + debug("tac1 2\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le) ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos goal - (rational_to_fraction c)]) + tac_zero_inf_pos + (rational_to_fraction c)])) ) else (if h.hstrict then + ( + + debug("tac1 3\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos goal - (rational_to_fraction c)]) + tac_zero_inf_pos + (rational_to_fraction c)])) else - tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) + ( + debug("tac1 4\n"); + tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) ~continuations:[!tac1;tac_use h; - tac_zero_inf_pos goal - (rational_to_fraction c)]))); + tac_zero_inf_pos + (rational_to_fraction c)])) + + ) + ); s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) @@ -953,7 +988,7 @@ let rec fourier ~status:(s_proof,s_goal)= |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) - debug ("finalmente applico t1\n"); + debug ("finalmente applico tac\n"); (!tac ~status:(proof,goal)) ;; -- 2.39.2