diff options
Diffstat (limited to 'plugins/fourier/fourierR.ml')
-rw-r--r-- | plugins/fourier/fourierR.ml | 96 |
1 files changed, 54 insertions, 42 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 51bd3009..b1c003de 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -12,7 +14,7 @@ des inéquations et équations sont entiers. En attendant la tactique Field. *) -open Term +open Constr open Tactics open Names open Globnames @@ -27,11 +29,7 @@ qui donne le coefficient d'un terme du calcul des constructions, qui est zéro si le terme n'y est pas. *) -module Constrhash = Hashtbl.Make - (struct type t = constr - let equal = eq_constr - let hash = hash_constr - end) +module Constrhash = Hashtbl.Make(Constr) type flin = {fhom: rational Constrhash.t; fcste:rational};; @@ -76,15 +74,15 @@ let flin_emult a f = type ineq = Rlt | Rle | Rgt | Rge let string_of_R_constant kn = - match Names.repr_con kn with - | MPfile dir, sec_dir, id when + match Constant.repr3 kn with + | ModPath.MPfile dir, sec_dir, id when sec_dir = DirPath.empty && DirPath.to_string dir = "Coq.Reals.Rdefinitions" -> Label.to_string id | _ -> "constant_not_of_R" let rec string_of_R_constr c = - match kind_of_term c with + match Constr.kind c with Cast (c,_,_) -> string_of_R_constr c |Const (c,_) -> string_of_R_constant c | _ -> "not_of_constant" @@ -92,7 +90,7 @@ let rec string_of_R_constr c = exception NoRational let rec rational_of_constr c = - match kind_of_term c with + match Constr.kind c with | Cast (c,_,_) -> (rational_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with @@ -125,7 +123,7 @@ exception NoLinear let rec flin_of_constr c = try( - match kind_of_term c with + match Constr.kind c with | Cast (c,_,_) -> (flin_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with @@ -190,9 +188,11 @@ type hineq={hname:constr; (* le nom de l'hypothèse *) exception NoIneq let ineq1_of_constr (h,t) = - match (kind_of_term t) with + let h = EConstr.Unsafe.to_constr h in + let t = EConstr.Unsafe.to_constr t in + match (Constr.kind t) with | App (f,args) -> - (match kind_of_term f with + (match Constr.kind f with | Const (c,_) when Array.length args = 2 -> let t1= args.(0) in let t2= args.(1) in @@ -231,7 +231,7 @@ let ineq1_of_constr (h,t) = let t0= args.(0) in let t1= args.(1) in let t2= args.(2) in - (match (kind_of_term t0) with + (match (Constr.kind t0) with | Const (c,_) -> (match (string_of_R_constant c) with | "R"-> @@ -281,14 +281,17 @@ let fourier_lineq lineq1 = (* Defined constants *) let get = Lazy.force -let constant = Coqlib.gen_constant "Fourier" +let cget = get +let eget c = EConstr.of_constr (Lazy.force c) +let constant path s = Universes.constr_of_global @@ + Coqlib.coq_reference "Fourier" path s (* Standard library *) open Coqlib let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (build_coq_False ()) -let coq_not = lazy (build_coq_not ()) -let coq_eq = lazy (build_coq_eq ()) +let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ()) +let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ()) +let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ()) (* Rdefinitions *) let constant_real = constant ["Reals";"Rdefinitions"] @@ -373,6 +376,7 @@ let rational_to_real x = (* preuve que 0<n*1/d *) let tac_zero_inf_pos gl (n,d) = + let get = eget in let tacn=ref (apply (get coq_Rlt_zero_1)) in let tacd=ref (apply (get coq_Rlt_zero_1)) in for _i = 1 to n - 1 do @@ -385,6 +389,7 @@ let tac_zero_inf_pos gl (n,d) = (* preuve que 0<=n*1/d *) let tac_zero_infeq_pos gl (n,d)= + let get = eget in let tacn=ref (if n=0 then (apply (get coq_Rle_zero_zero)) else (apply (get coq_Rle_zero_1))) in @@ -399,7 +404,8 @@ 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 (apply (get coq_Rnot_lt0)) + let get = eget in +if n=0 then (apply (get coq_Rnot_lt0)) else (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt)) (tac_zero_infeq_pos gl (-n,d))) @@ -408,6 +414,7 @@ let tac_zero_inf_false gl (n,d) = (* preuve que 0<=(-n)*(1/d) => False *) let tac_zero_infeq_false gl (n,d) = + let get = eget in (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) (tac_zero_inf_pos gl (-n,d))) ;; @@ -415,7 +422,8 @@ let tac_zero_infeq_false gl (n,d) = let exact = exact_check;; let tac_use h = - let tac = exact h.hname in + let get = eget in + let tac = exact (EConstr.of_constr h.hname) in match h.htype with "Rlt" -> tac |"Rle" -> tac @@ -428,7 +436,7 @@ let tac_use h = (* let is_ineq (h,t) = - match (kind_of_term t) with + match (Constr.kind t) with App (f,args) -> (match (string_of_R_constr f) with "Rlt" -> true @@ -459,16 +467,19 @@ exception GoalDone (* Résolution d'inéquations linéaires dans R *) let rec fourier () = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = strip_outer_cast concl in + let goal = Termops.strip_outer_cast sigma concl in + let goal = EConstr.Unsafe.to_constr goal in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) try - match (kind_of_term goal) with + match (Constr.kind goal) with App (f,args) -> + let get = eget in (match (string_of_R_constr f) with "Rlt" -> (Tacticals.New.tclTHEN @@ -494,18 +505,18 @@ let rec fourier () = |_-> raise GoalDone with GoalDone -> (* les hypothèses *) - let hyps = List.map (fun (h,t)-> (mkVar h,t)) + let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t)) (list_of_sign (Proofview.Goal.hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) with NoIneq -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.error "No inequalities"; + if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] - then CErrors.error "fourier failed" + then CErrors.user_err Pp.(str "fourier failed") (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> @@ -547,6 +558,7 @@ let rec fourier () = !t2 |] in let tc=rational_to_real cres in (* puis sa preuve *) + let get = eget in let tac1=ref (if h1.hstrict then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt)) [tac_use h1; @@ -583,30 +595,30 @@ let rec fourier () = then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(Tacticals.New.tclTHENS (cut ineq) + tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq)) [Tacticals.New.tclTHEN (change_concl - (mkAppL [| get coq_not; ineq|] - )) + (EConstr.of_constr (mkAppL [| cget coq_not; ineq|] + ))) (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt else get coq_Rnot_le_le)) (Tacticals.New.tclTHENS (Equality.replace - (mkAppL [|get coq_Rminus;!t2;!t1|] - ) - tc) + (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|] + )) + (EConstr.of_constr tc)) [tac2; (Tacticals.New.tclTHENS (Equality.replace - (mkApp (get coq_Rinv, - [|get coq_R1|])) + (EConstr.of_constr (mkApp (cget coq_Rinv, + [|cget coq_R1|]))) (get coq_R1)) (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) [Tacticals.New.tclORELSE (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (get coq_sym_eqT) (fun symeq -> + Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq -> (Tacticals.New.tclTHEN (apply symeq) - (apply (get coq_Rinv_1))))] + (apply (get coq_Rinv_1)))] ) ])); @@ -619,7 +631,7 @@ let rec fourier () = (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) !tac (* ((tclABSTRACT None !tac) gl) *) - end } + end ;; (* |