From fe07fcacb7060dddc6542b04bc1168f444ceaebf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Oct 2002 15:16:44 +0000 Subject: [PATCH] - rewritesimpl_tac added in fourierR.ml (wrong location) - simpl_tac added in fourierR.ml (wrong location) - "RewriteSimpl ->" button added - "Rewrite ->" button removed --- helm/gTopLevel/fourierR.ml | 470 ++++++++++++++++++++++----------- helm/gTopLevel/fourierR.mli | 2 +- helm/gTopLevel/gTopLevel.ml | 18 +- helm/gTopLevel/proofEngine.ml | 2 +- helm/gTopLevel/proofEngine.mli | 2 +- 5 files changed, 332 insertions(+), 162 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 566003e89..744a86e67 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -91,9 +91,10 @@ open Fourier 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") ;; (****************************************************************************** @@ -297,7 +298,7 @@ let rec flin_of_term t = _ -> (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 @@ -474,59 +475,103 @@ let fourier_lineq lineq1 = 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 ;; @@ -565,18 +610,6 @@ let rational_to_real x = (* preuve que 0 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; @@ -613,19 +655,30 @@ debug("TAC ZERO INF POS\n"); (* 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 ;; @@ -633,19 +686,44 @@ let tac_zero_infeq_pos gl (n,d) = (* 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 ;; @@ -660,7 +738,8 @@ 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)) ~status:(proof',goal) in proof'',fresh_meta::goals ;; @@ -679,7 +758,9 @@ let my_cut ~term:c ~status:(proof,goal)= 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 @@ -701,14 +782,18 @@ 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 + |"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"); @@ -773,13 +858,16 @@ let rec filter_real_hyp context cont = 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 @@ -789,11 +877,14 @@ let equality_replace a b ~status = 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) = @@ -832,26 +923,32 @@ let contradiction_tac ~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 *) @@ -859,7 +956,8 @@ let rec fourier ~status:(s_proof,s_goal)= ~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; @@ -891,12 +989,14 @@ let rec fourier ~status:(s_proof,s_goal)= 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*) @@ -911,11 +1011,12 @@ let rec fourier ~status:(s_proof,s_goal)= 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 *) @@ -926,48 +1027,53 @@ let rec fourier ~status:(s_proof,s_goal)= 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; @@ -976,11 +1082,12 @@ let rec fourier ~status:(s_proof,s_goal)= (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"); @@ -1040,28 +1147,63 @@ let rec fourier ~status:(s_proof,s_goal)= ~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] @@ -1070,7 +1212,7 @@ let rec fourier ~status:(s_proof,s_goal)= ~continuations:[Tacticals.then_ (* ??????????????????????????????? in coq era intro *) - ~start:(PrimitiveTactics.intros_tac ~name:(String.copy "??")) + ~start:(PrimitiveTactics.intros_tac ~name:"??") (* ????????????????????????????? *) ~continuation:contradiction_tac;!tac]) @@ -1085,3 +1227,31 @@ let rec fourier ~status:(s_proof,s_goal)= ;; 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 + +;; diff --git a/helm/gTopLevel/fourierR.mli b/helm/gTopLevel/fourierR.mli index 87d034909..fbd55e685 100644 --- a/helm/gTopLevel/fourierR.mli +++ b/helm/gTopLevel/fourierR.mli @@ -1,2 +1,2 @@ -val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic val fourier_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index cbfe18e73..c980f723b 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -47,9 +47,9 @@ let htmlfooter = "" ;; -let prooffile = "/public/sacerdot/currentproof";; +let prooffile = "/home/tassi/miohelm/tmp/currentproof";; (*CSC: the getter should handle the innertypes, not the FS *) -let innertypesfile = "/public/sacerdot/innertypes";; +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -684,8 +684,8 @@ let clear rendering_window = let fourier rendering_window = call_tactic ProofEngine.fourier rendering_window ;; -let rewrite rendering_window = - call_tactic_with_input ProofEngine.rewrite rendering_window +let rewritesimpl rendering_window = + call_tactic_with_input ProofEngine.rewrite_simpl rendering_window ;; @@ -746,7 +746,7 @@ let qed rendering_window () = (*???? let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; *) -let dtdname = "/projects/helm/V7/dtd/cic.dtd";; +let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";; let save rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -1465,8 +1465,8 @@ class rendering_window output proofw (label : GMisc.label) = let fourierb = GButton.button ~label:"Fourier" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let rewriteb = - GButton.button ~label:"Rewrite ->" + let rewritesimplb = + GButton.button ~label:"RewriteSimpl ->" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml @@ -1522,7 +1522,7 @@ object(self) ignore(clearbodyb#connect#clicked (clearbody self)) ; ignore(clearb#connect#clicked (clear self)) ; ignore(fourierb#connect#clicked (fourier self)) ; - ignore(rewriteb#connect#clicked (rewrite self)) ; + ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) @@ -1534,7 +1534,7 @@ let rendering_window = ref None;; let initialize_everything () = let module U = Unix in - let output = GMathView.math_view ~width:400 ~height:280 () + let output = GMathView.math_view ~width:350 ~height:280 () and proofw = GMathView.math_view ~width:400 ~height:275 () and label = GMisc.label ~text:"gTopLevel" () in let rendering_window' = diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 64d68a37e..5f0ba8aaa 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -274,4 +274,4 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) let elim_type term = apply_tactic (Ring.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac let fourier () = apply_tactic FourierR.fourier_tac -let rewrite term = apply_tactic (FourierR.rewrite_tac ~term) +let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index a11914a9a..f5c31067f 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -58,4 +58,4 @@ val clear : Cic.hypothesis -> unit val elim_type : Cic.term -> unit val ring : unit -> unit val fourier : unit -> unit -val rewrite : Cic.term -> unit +val rewrite_simpl : Cic.term -> unit -- 2.39.2