From 1d4de3a17c0a41781cc8e415361d228ded4f1d8f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Sep 2002 06:57:55 +0000 Subject: [PATCH] Tactic update --- helm/gTopLevel/fourierR.ml | 259 +++++++++++++++++++++---------------- 1 file changed, 147 insertions(+), 112 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 815a39aa1..79b3743da 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -29,11 +29,6 @@ des inéquations et équations sont entiers. En attendant la tactique Field. *) -(*open Term // in coq/kernel -open Tactics -open Clenv -open Names -open Tacmach*) open Fourier (****************************************************************************** @@ -398,6 +393,35 @@ Construction de la preuve en cas de succ i.e. on obtient une contradiction. *) +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 _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.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_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 _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.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_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 is_int x = (x.den)=1 ;; @@ -407,22 +431,6 @@ let rec rational_to_fraction x= (x.num,x.den) (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) *) -(*et int_to_real n = - let nn=abs n in - let s=ref Cic.term - if nn=0 - then s:="R0" - else (s:="R1"; - for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;); - if n<0 then s:="(Ropp "^(!s)^")"; - !s -;;*) -let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.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 _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;; - let rec int_to_real_aux n = match n with @@ -442,9 +450,6 @@ let int_to_real n = (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) *) -let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;; -let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;; - let rational_to_real x = let (n,d)=rational_to_fraction x in @@ -454,13 +459,6 @@ let rational_to_real x = (* preuve que 0 False *) -(*let tac_zero_inf_false gl (n,d) = - let cste = pf_parse_constr gl in - if n=0 then (apply (cste "Rnot_lt0")) + +let tac_zero_inf_false gl (n,d) = + if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) else - (tclTHEN (apply (cste "Rle_not_lt")) - (tac_zero_infeq_pos gl (-n,d))) -;;*) + (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt) + ~continuation:(tac_zero_infeq_pos gl (-n,d))) +;; (* preuve que 0<=(-n)*(1/d) => False *) -(*let tac_zero_infeq_false gl (n,d) = - let cste = pf_parse_constr gl in - (tclTHEN (apply (cste "Rlt_not_le")) - (tac_zero_inf_pos 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))) ;; + +(* *********** ********** ******** ??????????????? *********** ************** + +let mkMeta proof = Cic.Meta (ProofEngineHelpers.new_meta proof) (ProofEngineHelpers.identity_relocation_list_for_metavariable []);; + +let apply_type_tac t al (proof,goals) = + let new_m = mkMeta proof in + PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast new_m t)::al)) +;; + + + + let create_meta () = mkMeta(new_meta());; let my_cut c gl= let concl = pf_concl gl in apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl ;; -let exact = exact_check;; + +*********** * ********************************* ***************************** *) + +let exact = PrimitiveTactics.exact_tac;; let tac_use h = match h.htype with - "Rlt" -> exact h.hname - |"Rle" -> exact h.hname - |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt")) - (exact h.hname)) - |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le")) - (exact h.hname)) - |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le")) - (exact h.hname)) - |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le")) - (exact h.hname)) + "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 ;; + + +(* servono tutti ????????????????????????? *) +let uri_of_term t = + match t with + Cic.Const(u,_) -> u + |Cic.Var(u) -> u + |Cic.MutInd(u,_,_) -> u + |Cic.MutConstruct(u,_,_,_) -> u + |Cic.MutCase(u,_,_,_,_,_) -> u + | _ -> UriManager.uri_of_string "??????" + ;; + + + let is_ineq (h,t) = - match (kind_of_term t) with - App (f,args) -> - (match (string_of_constr f) with - "Coq.Reals.Rdefinitions.Rlt" -> true - |"Coq.Reals.Rdefinitions.Rgt" -> true - |"Coq.Reals.Rdefinitions.Rle" -> true - |"Coq.Reals.Rdefinitions.Rge" -> true - |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with - "Coq.Reals.Rdefinitions.R"->true + match t with + Cic.Appl ( Cic.Const(u,boh)::next) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true + |"cic:/Coq/Init/Logic_Type/eqT.con" -> (match (UriManager.string_of_uri (uri_of_term(List.hd next))) with + "cic:/Coq/Reals/Rdefinitions/R.con"->true |_->false) |_->false) |_->false @@ -545,59 +579,60 @@ let is_ineq (h,t) = let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; let mkAppL a = - let l = Array.to_list a in - mkApp(List.hd l, Array.of_list (List.tl l)) -;;*) + Cic.Appl(Array.to_list a) +;; (* Résolution d'inéquations linéaires dans R *) - -(* -let rec fourier gl= - let parse = pf_parse_constr gl in - let goal = strip_outer_cast (pf_concl gl) in - let fhyp=id_of_string "new_hyp_for_fourier" in +let rec strip_outer_cast c = match c with + | Cic.Cast (c,_) -> strip_outer_cast c + | _ -> c + +(* se pf_concl estrae la concl*) +(*let rec fourier ~status:(((p_uri,p_meta,p_incom,p_tes) as proof,goal) as status)= + let goal = strip_outer_cast p_tes in + let fhyp = String.copy "new_hyp_for_fourier" in *) (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) - try (let tac = - match (kind_of_term goal) with - App (f,args) -> - (match (string_of_constr f) with - "Coq.Reals.Rdefinitions.Rlt" -> - (tclTHEN - (tclTHEN (apply (parse "Rfourier_not_ge_lt")) - (intro_using fhyp)) - fourier) - |"Coq.Reals.Rdefinitions.Rle" -> - (tclTHEN - (tclTHEN (apply (parse "Rfourier_not_gt_le")) - (intro_using fhyp)) - fourier) - |"Coq.Reals.Rdefinitions.Rgt" -> - (tclTHEN - (tclTHEN (apply (parse "Rfourier_not_le_gt")) - (intro_using fhyp)) - fourier) - |"Coq.Reals.Rdefinitions.Rge" -> - (tclTHEN - (tclTHEN (apply (parse "Rfourier_not_lt_ge")) - (intro_using fhyp)) - fourier) +(* try (let tac = + match goal with + Cic.Appl ( Cic.Const(u,boh)::args) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> + (Tacticals.then_ + ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt) + ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)) + ~continuation:fourier) + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> + (Tacticals.then_ + ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le) + ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)) + ~continuation:fourier) + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> + (Tacticals.then_ + ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt) + ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)) + ~continuation:fourier) + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> + (Tacticals.then_ + ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge) + ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)) + ~continuation:fourier) |_->assert false) |_->assert false - in tac gl) - with _ -> -*) + in tac status) + with _ -> *) + (* les hypothèses *) -(* - let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t))) + (***** Come estraggo pf_hyps?????????????? *******) +(* let hyps = List.map (fun (h,t) -> (Cic.Var(h),t)) (list_of_sign (pf_hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) with _-> ()) hyps; -*) - + + *) (* lineq = les inéquations découlant des hypothèses *) -- 2.39.2