From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- plugins/fourier/fourierR.ml | 321 ++++++++++++++++++++++---------------------- 1 file changed, 160 insertions(+), 161 deletions(-) (limited to 'plugins/fourier/fourierR.ml') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 763383dd..8006a3e1 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* r0;; +let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;; let flin_add f x c = let cx = flin_coef f x in - Constrhash.remove f.fhom x; - Constrhash.add f.fhom x (rplus cx c); + Constrhash.replace f.fhom x (rplus cx c); f ;; let flin_add_cste f c = @@ -75,24 +73,25 @@ let flin_emult a f = ;; (*****************************************************************************) -open Vernacexpr type ineq = Rlt | Rle | Rgt | Rge let string_of_R_constant kn = match Names.repr_con kn with | MPfile dir, sec_dir, id when - sec_dir = empty_dirpath && - string_of_dirpath dir = "Coq.Reals.Rdefinitions" - -> string_of_label id + 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 Cast (c,_,_) -> string_of_R_constr c - |Const c -> string_of_R_constant c + |Const (c,_) -> string_of_R_constant c | _ -> "not_of_constant" +exception NoRational + let rec rational_of_constr c = match kind_of_term c with | Cast (c,_,_) -> (rational_of_constr c) @@ -114,15 +113,17 @@ let rec rational_of_constr c = | "Rminus" -> rminus (rational_of_constr args.(0)) (rational_of_constr args.(1)) - | _ -> failwith "not a rational") - | Const kn -> + | _ -> raise NoRational) + | Const (kn,_) -> (match (string_of_R_constant kn) with "R1" -> r1 |"R0" -> r0 - | _ -> failwith "not a rational") - | _ -> failwith "not a rational" + | _ -> raise NoRational) + | _ -> raise NoRational ;; +exception NoLinear + let rec flin_of_constr c = try( match kind_of_term c with @@ -138,39 +139,34 @@ let rec flin_of_constr c = flin_minus (flin_of_constr args.(0)) (flin_of_constr args.(1)) | "Rmult"-> - (try (let a=(rational_of_constr args.(0)) in - try (let b = (rational_of_constr args.(1)) in - (flin_add_cste (flin_zero()) (rmult a b))) - with e when Errors.noncritical e -> - (flin_add (flin_zero()) - args.(1) - a)) - with e when Errors.noncritical e -> - (flin_add (flin_zero()) - args.(0) - (rational_of_constr args.(1)))) + (try + let a = rational_of_constr args.(0) in + try + let b = rational_of_constr args.(1) in + flin_add_cste (flin_zero()) (rmult a b) + with NoRational -> + flin_add (flin_zero()) args.(1) a + with NoRational -> + flin_add (flin_zero()) args.(0) + (rational_of_constr args.(1))) | "Rinv"-> - let a=(rational_of_constr args.(0)) in - flin_add_cste (flin_zero()) (rinv a) + let a = rational_of_constr args.(0) in + flin_add_cste (flin_zero()) (rinv a) | "Rdiv"-> - (let b=(rational_of_constr args.(1)) in - try (let a = (rational_of_constr args.(0)) in - (flin_add_cste (flin_zero()) (rdiv a b))) - with e when Errors.noncritical e -> - (flin_add (flin_zero()) - args.(0) - (rinv b))) - |_->assert false) - | Const c -> + (let b = rational_of_constr args.(1) in + try + let a = rational_of_constr args.(0) in + flin_add_cste (flin_zero()) (rdiv a b) + with NoRational -> + flin_add (flin_zero()) args.(0) (rinv b)) + |_-> raise NoLinear) + | Const (c,_) -> (match (string_of_R_constant c) with "R1" -> flin_one () |"R0" -> flin_zero () - |_-> assert false) - |_-> assert false) - with e when Errors.noncritical e -> - flin_add (flin_zero()) - c - r1 + |_-> raise NoLinear) + |_-> raise NoLinear) + with NoRational | NoLinear -> flin_add (flin_zero()) c r1 ;; let flin_to_alist f = @@ -179,9 +175,9 @@ let flin_to_alist f = !res ;; -(* Représentation des hypothèses qui sont des inéquations ou des équations. +(* Représentation des hypothèses qui sont des inéquations ou des équations. *) -type hineq={hname:constr; (* le nom de l'hypothèse *) +type hineq={hname:constr; (* le nom de l'hypothèse *) htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) hleft:constr; hright:constr; @@ -189,54 +185,57 @@ type hineq={hname:constr; (* le nom de l'hypoth hstrict:bool} ;; -(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 +(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 *) + +exception NoIneq + let ineq1_of_constr (h,t) = match (kind_of_term t) with - App (f,args) -> - (match kind_of_term f with - Const c when Array.length args = 2 -> - let t1= args.(0) in - let t2= args.(1) in + | App (f,args) -> + (match kind_of_term f with + | Const (c,_) when Array.length args = 2 -> + let t1= args.(0) in + let t2= args.(1) in (match (string_of_R_constant c) with - "Rlt" -> [{hname=h; + |"Rlt" -> [{hname=h; htype="Rlt"; hleft=t1; hright=t2; hflin= flin_minus (flin_of_constr t1) (flin_of_constr t2); hstrict=true}] - |"Rgt" -> [{hname=h; + |"Rgt" -> [{hname=h; htype="Rgt"; hleft=t2; hright=t1; hflin= flin_minus (flin_of_constr t2) (flin_of_constr t1); hstrict=true}] - |"Rle" -> [{hname=h; + |"Rle" -> [{hname=h; htype="Rle"; hleft=t1; hright=t2; hflin= flin_minus (flin_of_constr t1) (flin_of_constr t2); hstrict=false}] - |"Rge" -> [{hname=h; + |"Rge" -> [{hname=h; htype="Rge"; hleft=t2; hright=t1; hflin= flin_minus (flin_of_constr t2) (flin_of_constr t1); hstrict=false}] - |_->assert false) - | Ind (kn,i) -> - if IndRef(kn,i) = Coqlib.glob_eq then - let t0= args.(0) in - let t1= args.(1) in - let t2= args.(2) in - (match (kind_of_term t0) with - Const c -> - (match (string_of_R_constant c) with - "R"-> + |_-> raise NoIneq) + | Ind ((kn,i),_) -> + if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; + let t0= args.(0) in + let t1= args.(1) in + let t2= args.(2) in + (match (kind_of_term t0) with + | Const (c,_) -> + (match (string_of_R_constant c) with + | "R"-> [{hname=h; htype="eqTLR"; hleft=t1; @@ -251,20 +250,18 @@ let ineq1_of_constr (h,t) = hflin= flin_minus (flin_of_constr t2) (flin_of_constr t1); hstrict=false}] - |_-> assert false) - |_-> assert false) - else - assert false - |_-> assert false) - |_-> assert false + |_-> raise NoIneq) + |_-> raise NoIneq) + |_-> raise NoIneq) + |_-> raise NoIneq ;; -(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) +(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) *) let fourier_lineq lineq1 = let nvar=ref (-1) in - let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) + let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) List.iter (fun f -> Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin nvar:=(!nvar)+1; @@ -273,7 +270,7 @@ let fourier_lineq lineq1 = f.hflin.fhom) lineq1; let sys= List.map (fun h-> - let v=Array.create ((!nvar)+1) r0 in + let v=Array.make ((!nvar)+1) r0 in Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c) h.hflin.fhom; ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) @@ -345,14 +342,14 @@ let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le") let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp") (****************************************************************************** -Construction de la preuve en cas de succès de la méthode de Fourier, +Construction de la preuve en cas de succès de la méthode de Fourier, i.e. on obtient une contradiction. *) let is_int x = (x.den)=1 ;; (* fraction = couple (num,den) *) -let rec rational_to_fraction x= (x.num,x.den) +let rational_to_fraction x= (x.num,x.den) ;; (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) @@ -363,7 +360,7 @@ let int_to_real n = then get coq_R0 else (let s=ref (get coq_R1) in - for i=1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done; + for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done; if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s) ;; (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) @@ -379,11 +376,11 @@ let rational_to_real x = let tac_zero_inf_pos gl (n,d) = 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 - tacn:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done; - for i=1 to d-1 do - tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd]) + for _i = 1 to n - 1 do + tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done; + for _i = 1 to d - 1 do + tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; + (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd]) ;; (* preuve que 0<=n*1/d @@ -393,11 +390,11 @@ let tac_zero_infeq_pos gl (n,d)= then (apply (get coq_Rle_zero_zero)) else (apply (get coq_Rle_zero_1))) in let tacd=ref (apply (get coq_Rlt_zero_1)) in - for i=1 to n-1 do - tacn:=(tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done; - for i=1 to d-1 do - tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd]) + for _i = 1 to n - 1 do + tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done; + for _i = 1 to d - 1 do + tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; + (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd]) ;; (* preuve que 0<(-n)*(1/d) => False @@ -405,14 +402,14 @@ let tac_zero_infeq_pos gl (n,d)= let tac_zero_inf_false gl (n,d) = if n=0 then (apply (get coq_Rnot_lt0)) else - (tclTHEN (apply (get coq_Rle_not_lt)) + (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt)) (tac_zero_infeq_pos gl (-n,d))) ;; (* preuve que 0<=(-n)*(1/d) => False *) let tac_zero_infeq_false gl (n,d) = - (tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) + (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) (tac_zero_inf_pos gl (-n,d))) ;; @@ -425,18 +422,16 @@ let my_cut c gl= let exact = exact_check;; -let tac_use h = match h.htype with - "Rlt" -> exact h.hname - |"Rle" -> exact h.hname - |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt)) - (exact h.hname)) - |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le)) - (exact h.hname)) - |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) - (exact h.hname)) - |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) - (exact h.hname)) - |_->assert false +let tac_use h = + let tac = exact h.hname in + match h.htype with + "Rlt" -> tac + |"Rle" -> tac + |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac) + |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac) + |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac) + |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac) + |_->assert false ;; (* @@ -464,58 +459,61 @@ let mkAppL a = mkApp(List.hd l, Array.of_list (List.tl l)) ;; -(* Résolution d'inéquations linéaires dans R *) -let rec fourier gl= +exception GoalDone + +(* Résolution d'inéquations linéaires dans R *) +let rec fourier () = + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = strip_outer_cast (pf_concl gl) 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 (let tac = - match (kind_of_term goal) with + let goal = strip_outer_cast concl 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 App (f,args) -> (match (string_of_R_constr f) with "Rlt" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_ge_lt)) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt)) (intro_using fhyp)) - fourier) + (fourier ())) |"Rle" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_gt_le)) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le)) (intro_using fhyp)) - fourier) + (fourier ())) |"Rgt" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_le_gt)) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt)) (intro_using fhyp)) - fourier) + (fourier ())) |"Rge" -> - (tclTHEN - (tclTHEN (apply (get coq_Rfourier_not_lt_ge)) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge)) (intro_using fhyp)) - fourier) - |_->assert false) - |_->assert false - in tac gl) - with e when Errors.noncritical e -> - (* les hypothèses *) + (fourier ())) + |_-> raise GoalDone) + |_-> raise GoalDone + with GoalDone -> + (* les hypothèses *) let hyps = List.map (fun (h,t)-> (mkVar h,t)) - (list_of_sign (pf_hyps gl)) in + (list_of_sign (Proofview.Goal.hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) - with e when Errors.noncritical e -> ()) + with NoIneq -> ()) hyps; - (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then Util.error "No inequalities"; + (* lineq = les inéquations découlant des hypothèses *) + if !lineq=[] then Errors.error "No inequalities"; let res=fourier_lineq (!lineq) in - let tac=ref tclIDTAC in + let tac=ref (Proofview.tclUNIT ()) in if res=[] - then Util.error "fourier failed" - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) + then Errors.error "fourier failed" + (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> - (* lc=coefficients multiplicateurs des inéquations + (* lc=coefficients multiplicateurs des inéquations qui donnent 0 let s=ref (h1.hstrict) in @@ -554,11 +552,11 @@ let rec fourier gl= let tc=rational_to_real cres in (* puis sa preuve *) let tac1=ref (if h1.hstrict - then (tclTHENS (apply (get coq_Rfourier_lt)) + then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt)) [tac_use h1; tac_zero_inf_pos gl (rational_to_fraction c1)]) - else (tclTHENS (apply (get coq_Rfourier_le)) + else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le)) [tac_use h1; tac_zero_inf_pos gl (rational_to_fraction c1)])) in @@ -566,20 +564,20 @@ let rec fourier gl= List.iter (fun (h,c)-> (if (!s) then (if h.hstrict - then tac1:=(tclTHENS (apply (get coq_Rfourier_lt_lt)) + then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)]) - else tac1:=(tclTHENS (apply (get coq_Rfourier_lt_le)) + else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)])) else (if h.hstrict - then tac1:=(tclTHENS (apply (get coq_Rfourier_le_lt)) + then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)]) - else tac1:=(tclTHENS (apply (get coq_Rfourier_le_le)) + else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le)) [!tac1;tac_use h; tac_zero_inf_pos gl (rational_to_fraction c)]))); @@ -589,42 +587,43 @@ let rec fourier gl= then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(tclTHENS (my_cut ineq) - [tclTHEN (change_in_concl None + tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq)) + [Tacticals.New.tclTHEN (change_concl (mkAppL [| get coq_not; ineq|] )) - (tclTHEN (apply (if sres then get coq_Rnot_lt_lt + (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt else get coq_Rnot_le_le)) - (tclTHENS (Equality.replace + (Tacticals.New.tclTHENS (Equality.replace (mkAppL [|get coq_Rminus;!t2;!t1|] ) tc) [tac2; - (tclTHENS + (Tacticals.New.tclTHENS (Equality.replace (mkApp (get coq_Rinv, [|get coq_R1|])) (get coq_R1)) -(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) +(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) - [tclORELSE - (Ring.polynom []) - tclIDTAC; - (tclTHEN (apply (get coq_sym_eqT)) - (apply (get coq_Rinv_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.tclTHEN (apply symeq) + (apply (get coq_Rinv_1))))] ) ])); !tac1]); - tac:=(tclTHENS (cut (get coq_False)) - [tclTHEN intro (contradiction None); + tac:=(Tacticals.New.tclTHENS (cut (get coq_False)) + [Tacticals.New.tclTHEN intro (contradiction None); !tac]) |_-> assert false) |_-> assert false ); (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) - (!tac gl) + !tac (* ((tclABSTRACT None !tac) gl) *) - + end ;; (* -- cgit v1.2.3