diff options
| -rw-r--r-- | contrib/dp/Gappa.v | 489 | ||||
| -rw-r--r-- | contrib/dp/dp_gappa.ml | 199 | ||||
| -rw-r--r-- | contrib/dp/g_dp.ml4 | 2 | ||||
| -rw-r--r-- | contrib/dp/test_gappa.v | 46 |
4 files changed, 586 insertions, 150 deletions
diff --git a/contrib/dp/Gappa.v b/contrib/dp/Gappa.v index 2259cb269..0e2e9a4d2 100644 --- a/contrib/dp/Gappa.v +++ b/contrib/dp/Gappa.v @@ -1,122 +1,407 @@ -Require Export ZArith. -Require Export Reals. - -Inductive float := - | Fzero : float - | Float (b : positive) (s : bool) (m : positive) (e : Z) : float. - -Fixpoint P2R (p : positive) := - match p with - | xH => 1%R - | xO xH => 2%R - | xO t => (2 * P2R t)%R - | xI xH => 3%R - | xI t => (1 + 2 * P2R t)%R - end. +Require Import Reals. +Require Import List. +Require Import Gappa_library. +Require Import Gappa_integer. + +Inductive UnaryOp : Set := + | uoNeg | uoSqrt | uoAbs | uoInv. + +Inductive BinaryOp : Set := + | boAdd | boSub | boMul | boDiv. + +(* represent an expression on real numbers *) +Inductive RExpr : Set := + | reUnknown : R -> RExpr + | reInteger : Z -> RExpr + | reFloat2 : Z -> Z -> RExpr + | reUnary : UnaryOp -> RExpr -> RExpr + | reBinary : BinaryOp -> RExpr -> RExpr -> RExpr + | rePow2 : Z -> RExpr + | reINR : positive -> RExpr. -Definition Z2R n := - match n with - | Zpos p => P2R p - | Zneg p => Ropp (P2R p) - | Z0 => R0 +(* convert to an expression on real numbers *) +Fixpoint convert t : R := + match t with + | reUnknown x => x + | reInteger x => Float1 x + | reFloat2 x y => float2R (Float2 x y) + | reUnary o x => + match o with + | uoNeg => Ropp + | uoSqrt => sqrt + | uoAbs => Rabs + | uoInv => Rinv + end (convert x) + | reBinary o x y => + match o with + | boAdd => Rplus + | boSub => Rminus + | boMul => Rmult + | boDiv => Rdiv + end (convert x) (convert y) + | rePow2 x => + powerRZ 2%R x + | reINR x => + INR (nat_of_P x) end. -Lemma IZR_Z2R : - forall x, IZR x = Z2R x. -Admitted. - -Ltac get_float t := - let get_mantissa t := - let rec aux t := - match t with - | 1%R => xH - | 2%R => constr:(xO xH) - | 3%R => constr:(xI xH) - | (2 * ?v)%R => - let w := aux v in constr:(xO w) - | (1 + 2 * ?v)%R => - let w := aux v in constr:(xI w) - end in - aux t in - let get_float_rational s n d := - let rec aux t := - match t with - | 2%R => xH - | (2 * ?v)%R => - let w := aux v in - eval vm_compute in (Psucc w) - end in - let e := aux d in - let m := get_mantissa n in - eval vm_compute in (Float 2 s m (Zneg e)) in - let get_float_integer s t := - let rec aux m e := - match m with - | xO ?v => - let u := eval vm_compute in (Zsucc e) in - aux v u - | _ => constr:(m, e) - end in - let m := get_mantissa t in - let v := aux m Z0 in - match v with - | (?m, ?e) => eval vm_compute in (Float 2 s m e) +Definition is_stable f := + forall t, convert (f t) = convert t. + +(* apply a function recursively, starting from the leafs of an expression *) +Definition recursive_transform f := + let fix aux (t : RExpr) := f + match t with + | reUnary o x => reUnary o (aux x) + | reBinary o x y => reBinary o (aux x) (aux y) + | _ => t end in + aux. + +Theorem recursive_transform_correct : + forall f, + is_stable f -> + is_stable (recursive_transform f). +unfold is_stable. +intros f Hf t. +induction t ; simpl ; rewrite Hf ; try apply refl_equal. +simpl. +rewrite IHt. +apply refl_equal. +simpl. +rewrite IHt1. +rewrite IHt2. +apply refl_equal. +Qed. + +Record TF : Set := mkTF + { trans_func :> RExpr -> RExpr ; + trans_prop : is_stable trans_func }. + +(* apply several recursive transformations in a row (selected from head to tail) *) +Definition multi_transform := + fold_left (fun v f => recursive_transform (trans_func f) v). + +Theorem multi_transform_correct : + forall l t, + convert (multi_transform l t) = convert t. +intros l. +unfold multi_transform. +rewrite <- (rev_involutive l). +induction (rev l) ; intros t. +apply refl_equal. +simpl. +rewrite fold_left_app. +simpl. +rewrite recursive_transform_correct. +apply IHl0. +apply trans_prop. +Qed. + +(* detect closed integers *) +Ltac is_natural t := match t with - | 0%R => Fzero - | (-?n * /?d)%R => get_float_rational true n d - | (?n * /?d)%R => get_float_rational false n d - | (-?n / ?d)%R => get_float_rational true n d - | (?n / ?d)%R => get_float_rational false n d - | (-?n)%R => get_float_integer true n - | ?n => get_float_integer false n + | O => true + | S ?t' => is_natural t' | _ => false end. -Definition FtoR radix (s : bool) m e := - let sm := if s then Zneg m else Zpos m in - match e with - | Zpos p => Z2R (sm * Zpower_pos (Zpos radix) p) - | Z0 => Z2R sm - | Zneg p => (Z2R sm / Z2R (Zpower_pos (Zpos radix) p))%R +Ltac is_positive t := + match t with + | xH => true + | xO ?t' => is_positive t' + | xI ?t' => is_positive t' + | _ => false end. -Definition F2R f := - match f with - | Fzero => R0 - | Float b s m e => FtoR b s m e +Ltac is_integer t := + match t with + | Z0 => true + | Zpos ?t' => is_positive t' + | Zneg ?t' => is_positive t' + | _ => false end. -Ltac get_term t := - match get_float t with - | false => - match t with - | (?a + ?b)%R => - let a' := get_term a in - let b' := get_term b in - constr:(Rplus a' b') - | ?e => e +(* produce an inductive object u such that convert(u) is convertible to t, + all the integers contained in u are closed expressions *) +Ltac get_inductive_term t := + match t with + | 0%R => + constr:(reInteger 0%Z) + | 1%R => + constr:(reInteger 1%Z) + | 2%R => + constr:(reInteger 2%Z) + | 3%R => + constr:(reInteger 3%Z) + | (2 * ?x)%R => + match get_inductive_term x with + | reInteger (Zpos (?c ?y)) => constr:(reInteger (Zpos (xO (c y)))) + | ?x' => constr:(reBinary boMul (reInteger 2%Z) x') + end + | (1 + 2 * ?x)%R => + match get_inductive_term x with + | reInteger (Zpos (?c ?y)) => constr:(reInteger (Zpos (xI (c y)))) + | ?x' => constr:(reBinary boAdd (reInteger 1%Z) (reBinary boMul (reInteger 2%Z) x')) end - | ?f =>constr:(F2R f) + | IZR 0%Z => + constr:(reInteger 0%Z) + | IZR 1%Z => + constr:(reInteger 1%Z) + | IZR 2%Z => + constr:(reInteger 2%Z) + | IZR (-1)%Z => + constr:(reInteger (-1)%Z) + | IZR (-2)%Z => + constr:(reInteger (-2)%Z) + | INR 0%nat => + constr:(reInteger 0%Z) + | INR 1%nat => + constr:(reInteger 1%Z) + | INR 2%nat => + constr:(reInteger 2%Z) + | INR (S ?x) => + match is_natural x with + | true => + let x' := eval vm_compute in (P_of_succ_nat x) in + constr:(reINR x') + end + | IZR (Zpos ?x) => + match is_positive x with + | true => constr:(reINR x) + end + | IZR (Zneg ?x) => + match is_positive x with + | true => constr:(reUnary uoNeg (reINR x)) + end + | Ropp ?x => + match get_inductive_term x with + | reInteger (Zpos ?y) => constr:(reInteger (Zneg y)) + | ?x' => constr:(reUnary uoNeg x') + end + | (?x + -?y)%R => + let x' := get_inductive_term x in + let y' := get_inductive_term y in + constr:(reBinary boSub x' y') + | (?x * /?y)%R => + let x' := get_inductive_term x in + let y' := get_inductive_term y in + constr:(reBinary boDiv x' y') + | powerRZ ?x ?y => + match get_inductive_term x with + | reInteger 2%Z => + match is_integer y with + | true => constr:(rePow2 y) + end + end + | ?f ?x ?y => + let bo := + match f with + | Rplus => boAdd + | Rminus => boSub + | Rmult => boMul + | Rdiv => boDiv + end in + let x' := get_inductive_term x in + let y' := get_inductive_term y in + constr:(reBinary bo x' y') + | ?f ?x => + let bo := + match f with + | Ropp => uoNeg + | sqrt => uoSqrt + | Rinv => uoInv + | Rabs => uoAbs + end in + let x' := get_inductive_term x in + constr:(reUnary bo x') + | _ => + constr:(reUnknown t) end. -Ltac gappar := +(* factor an integer into odd*2^e *) +Definition get_float2 x := + let fix aux (m : positive) e { struct m } := + match m with + | xO p => aux p (Zsucc e) + | _ => Float2 (Zpos m) e + end in + aux x Z0. + +Lemma get_float2_correct : + forall x, float2R (get_float2 x) = Z2R (Zpos x). +intros x. +unfold get_float2. +change (Z2R (Zpos x)) with (float2R (Float2 (Zpos x) 0%Z)). +generalize 0%Z. +induction x ; intros e ; try apply refl_equal. +rewrite IHx. +unfold float2R. +simpl. +replace (Zpos (xO x)) with (Zpos x * 2)%Z. +exact (Gappa_round_aux.float2_shift_p1 _ _). +rewrite Zmult_comm. +apply refl_equal. +Qed. + +(* transform INR and IZR into real integers, change a/b and a*2^b into floats *) +Definition gen_float2_func t := + match t with + | reUnary uoNeg (reInteger (Zpos x)) => + reInteger (Zneg x) + | reBinary boDiv (reInteger x) (reInteger (Zpos y)) => + match get_float2 y with + | Float2 1 (Zpos y') => reFloat2 x (Zneg y') + | _ => t + end + | reBinary boMul (reInteger x) (rePow2 y) => + reFloat2 x y + | reINR x => + reInteger (Zpos x) + | _ => t + end. + +Lemma gen_float2_prop : + is_stable gen_float2_func. +intros [x|x|x y|o x|o x y|x|x] ; try apply refl_equal. +(* unary ops *) +destruct o ; try apply refl_equal. +destruct x ; try apply refl_equal. +destruct z ; apply refl_equal. +(* binary ops *) +destruct o ; try apply refl_equal ; + destruct x ; try apply refl_equal ; + destruct y ; try apply refl_equal. +(* . x * 2^y *) +simpl. +unfold float2R. +rewrite F2R_split. +apply refl_equal. +(* . x / 2*2*2*2 *) +destruct z0 ; try apply refl_equal. +generalize (get_float2_correct p). +simpl. +destruct (get_float2 p) as ([|[m|m|]|m], [|e|e]) ; intros H ; try apply refl_equal. +rewrite <- H. +simpl. +unfold float2R. +do 2 rewrite F2R_split. +simpl. +rewrite Rmult_1_l. +apply refl_equal. +(* INR *) +exact (P2R_INR _). +Qed. + +Definition gen_float2 := mkTF gen_float2_func gen_float2_prop. + +(* remove pending powerRZ 2 *) +Definition clean_pow2_func t := + match t with + | rePow2 x => reFloat2 1 x + | _ => t + end. + +Lemma clean_pow2_prop : + is_stable clean_pow2_func. +intros [x|x|x y|o x|o x y|x|x] ; try apply refl_equal. +simpl. +apply Gappa_round_aux.float2_pow2. +Qed. + +Definition clean_pow2 := mkTF clean_pow2_func clean_pow2_prop. + +(* compute on constant terms, so that they are hopefully represented by a single float *) +Definition merge_float2_func t := + match t with + | reInteger x => reFloat2 x 0 + | reUnary uoNeg (reFloat2 x y) => reFloat2 (- x) y + | reBinary boMul (reFloat2 x1 y1) (reFloat2 x2 y2) => reFloat2 (x1 * x2) (y1 + y2) + | _ => t + end. + +Lemma merge_float2_prop : + is_stable merge_float2_func. +intros [x|x|x y|o x|o x y|x|x] ; try apply refl_equal. +(* unary ops *) +destruct o ; try apply refl_equal. +destruct x ; try apply refl_equal. +simpl. +rewrite <- Gappa_dyadic.Fopp2_correct. +apply refl_equal. +(* binary ops *) +destruct o ; try apply refl_equal. +destruct x ; try apply refl_equal. +destruct y ; try apply refl_equal. +simpl. +rewrite <- Gappa_dyadic.Fmult2_correct. +apply refl_equal. +Qed. + +Definition merge_float2 := mkTF merge_float2_func merge_float2_prop. + +(* some dummy definition to ensure precise rewriting of the terms and termination *) +Definition convertTODO1 := convert. +Definition convertTODO2 := convert. +Definition convertTODO3 := convert. +Definition reUnknownTODO := reUnknown. + +(* produce a compatible goal where all the Gappa-usable enclosures have been converted, + some integers may no longer be closed terms, but they can be evaluated to closed terms *) +Ltac gappa_prepare := intros ; subst ; + let trans_expr := constr:(gen_float2 :: clean_pow2 :: nil) in + let trans_bound := constr:(gen_float2 :: clean_pow2 :: merge_float2 :: nil) in + (* - get an inductive object for the bounded expression without any INR, INZ, powerRZ 2 + - same for the bounds, but try harder to get single floats *) + match goal with + | |- (?a <= ?e <= ?b)%R => + let a' := get_inductive_term a in + let b' := get_inductive_term b in + let e' := get_inductive_term e in + change (convertTODO1 a' <= convertTODO2 e' <= convertTODO3 b')%R ; + let w := eval simpl in (multi_transform trans_bound a') in + replace (convertTODO1 a') with (convert w) ; [idtac | exact (multi_transform_correct trans_bound a')] ; + let w := eval simpl in (multi_transform trans_bound b') in + replace (convertTODO3 b') with (convert w) ; [idtac | exact (multi_transform_correct trans_bound b')] ; + let w := eval simpl in (multi_transform trans_expr e') in + replace (convertTODO2 e') with (convert w) ; [idtac | exact (multi_transform_correct trans_expr e')] + end ; + (* apply the same transformation to the hypotheses and move them to the goal *) repeat match goal with | H: (?a <= ?e <= ?b)%R |- _ => - let a' := get_float a in - let b' := get_float b in - let e' := get_term e in - change (F2R a' <= e' <= F2R b')%R in H - | |- (?a <= ?e <= ?b)%R => - let a' := get_float a in - let b' := get_float b in - let e' := get_term e in - change (F2R a' <= e' <= F2R b')%R - end. - -Ltac gappa2 := - gappar; - gappa. + let a' := get_inductive_term a in + let b' := get_inductive_term b in + let e' := get_inductive_term e in + change (convertTODO1 a' <= convertTODO2 e' <= convertTODO3 b')%R in H ; + generalize H ; clear H ; + let w := eval simpl in (multi_transform trans_bound a') in + replace (convertTODO1 a') with (convert w) ; [idtac | exact (multi_transform_correct trans_bound a')] ; + let w := eval simpl in (multi_transform trans_bound b') in + replace (convertTODO3 b') with (convert w) ; [idtac | exact (multi_transform_correct trans_bound b')] ; + let w := eval simpl in (multi_transform trans_expr e') in + replace (convertTODO2 e') with (convert w) ; [idtac | exact (multi_transform_correct trans_expr e')] + end ; + (* generalize any unrecognized expression *) + change reUnknown with reUnknownTODO ; + repeat + match goal with + | z: R |- _ => + match goal with + | |- context [reUnknownTODO z] => + change (reUnknownTODO z) with (reUnknown z) + end + | |- context [reUnknownTODO ?z] => + change (reUnknownTODO z) with (reUnknown z) ; + generalize z ; intro + end ; + intros. +(* +Goal + forall y x, + (1 <= x + INR 7 * (y * sin y) <= IZR 12/16 * powerRZ 2 3)%R -> + (1 <= sqrt x <= 3/2)%R. +gappa_prepare. +*) diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml index 65ec7124f..1fd9190f7 100644 --- a/contrib/dp/dp_gappa.ml +++ b/contrib/dp/dp_gappa.ml @@ -13,6 +13,7 @@ open Coqlib open Hipattern open Libnames open Declarations +open Evarutil (* 1. gappa syntax trees and output *) @@ -21,7 +22,6 @@ module Constant = struct type t = { mantissa : int; base : int; exp : int } let create (b, m, e) = - if b <> 2 && b <> 10 then invalid_arg "Constant.create"; { mantissa = m; base = b; exp = e } let of_int x = @@ -73,16 +73,53 @@ let print_pred fmt = function fprintf fmt "%a in [%a, %a]" print_term t Constant.print c1 Constant.print c2 +let read_gappa_proof f = + let buf = Buffer.create 1024 in + Buffer.add_char buf '('; + let cin = open_in f in + let rec skip_space () = + let c = input_char cin in if c = ' ' then skip_space () else c + in + while input_char cin <> '=' do () done; + try + while true do + let c = skip_space () in + if c = ':' then raise Exit; + Buffer.add_char buf c; + let s = input_line cin in + Buffer.add_string buf s; + Buffer.add_char buf '\n'; + done; + assert false + with Exit -> + Buffer.add_char buf ')'; + Buffer.contents buf + +exception GappaFailed +exception GappaProofFailed + let call_gappa hl p = - let f = "test.gappa" in - let c = open_out f in + let gappa_in = "test.gappa" in + let c = open_out gappa_in in let fmt = formatter_of_out_channel c in fprintf fmt "@[{ "; List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl; fprintf fmt "%a }@]@." print_pred p; close_out c; - let out = Sys.command (sprintf "gappa < %s" f) in - msgnl (str ("gappa exit code is " ^ string_of_int out)) + let gappa_out = "gappa.v" in + let cmd = sprintf "gappa -Bcoq < %s > %s" gappa_in gappa_out in + let out = Sys.command cmd in + if out <> 0 then raise GappaFailed; + let cmd = sprintf "sed -e '/^Lemma/ h ; s/Qed/Defined/ ; $ { p ; g ; s/Lemma \\([^ ]*\\).*/Eval compute in \\1./ }' -i %s" gappa_out + in + let _ = Sys.command cmd in + let lambda = "test.lambda" in + let cmd = + sprintf "coqc -I ~/src/gappalib-coq-0.7 %s > %s" gappa_out lambda + in + let out = Sys.command cmd in + if out <> 0 then raise GappaProofFailed; + read_gappa_proof lambda (* 2. coq -> gappa translation *) @@ -103,6 +140,8 @@ let coq_modules = let constant = gen_constant_in_modules "gappa" coq_modules let coq_Rle = lazy (constant "Rle") +let coq_R = lazy (constant "R") +(* let coq_Rplus = lazy (constant "Rplus") let coq_Rminus = lazy (constant "Rminus") let coq_Rmult = lazy (constant "Rmult") @@ -112,10 +151,21 @@ let coq_R1 = lazy (constant "R1") let coq_Ropp = lazy (constant "Ropp") let coq_Rabs = lazy (constant "Rabs") let coq_sqrt = lazy (constant "sqrt") - -let coq_F2R = lazy (constant "F2R") -let coq_Fzero = lazy (constant "Fzero") -let coq_Float = lazy (constant "Float") +*) + +let coq_convert = lazy (constant "convert") +let coq_reUnknown = lazy (constant "reUnknown") +let coq_reFloat2 = lazy (constant "reFloat2") +let coq_reInteger = lazy (constant "reInteger") +let coq_reBinary = lazy (constant "reBinary") +let coq_reUnary = lazy (constant "reUnary") +let coq_boAdd = lazy (constant "boAdd") +let coq_boSub = lazy (constant "boSub") +let coq_boMul = lazy (constant "boMul") +let coq_boDiv = lazy (constant "boDiv") +let coq_uoAbs = lazy (constant "uoAbs") +let coq_uoNeg = lazy (constant "uoNeg") +let coq_uoSqrt = lazy (constant "uoSqrt") let coq_true = lazy (constant "true") let coq_false = lazy (constant "false") @@ -163,64 +213,119 @@ let tr_bool c = match decompose_app c with | c, [] when c = Lazy.force coq_false -> false | _ -> raise NotGappa -let tr_float c = match decompose_app c with - | c, [] when c = Lazy.force coq_Fzero -> - (2,0,0) - | c, [b; s; m; e] when c = Lazy.force coq_Float -> - let m = tr_positive m in - let m' = if tr_bool s then - m else m in - (tr_positive b, m', tr_arith_constant e) - | _ -> - raise NotGappa +let tr_float b m e = + (b, tr_arith_constant m, tr_arith_constant e) + +let tr_binop c = match decompose_app c with + | c, [] when c = Lazy.force coq_boAdd -> Bplus + | c, [] when c = Lazy.force coq_boSub -> Bminus + | c, [] when c = Lazy.force coq_boMul -> Bmult + | c, [] when c = Lazy.force coq_boDiv -> Bdiv + | _ -> assert false + +let tr_unop c = match decompose_app c with + | c, [] when c = Lazy.force coq_uoNeg -> Uopp + | c, [] when c = Lazy.force coq_uoSqrt -> Usqrt + | c, [] when c = Lazy.force coq_uoAbs -> Uabs + | _ -> raise NotGappa + +let tr_var c = match decomp c with + | Var x, [] -> string_of_id x + | _ -> assert false +(* REexpr -> term *) let rec tr_term c0 = let c, args = decompose_app c0 in match kind_of_term c, args with - | Var id, [] -> - Tvar (string_of_id id) - | _, [a] when c = Lazy.force coq_F2R -> - Tconst (Constant.create (tr_float a)) - | _, [a;b] when c = Lazy.force coq_Rplus -> - Tbinop (Bplus, tr_term a, tr_term b) - | _, [a;b] when c = Lazy.force coq_Rminus -> - Tbinop (Bminus, tr_term a, tr_term b) - | _, [a;b] when c = Lazy.force coq_Rmult -> - Tbinop (Bmult, tr_term a, tr_term b) - | _, [a;b] when c = Lazy.force coq_Rdiv -> - Tbinop (Bmult, tr_term a, tr_term b) - | _, [a] when c = Lazy.force coq_sqrt -> - Tunop (Usqrt, tr_term a) - | _, [a] when c = Lazy.force coq_Rabs -> - Tunop (Uabs, tr_term a) - | _, [a] when c = Lazy.force coq_Ropp -> - Tunop (Uopp, tr_term a) + | _, [a] when c = Lazy.force coq_reUnknown -> + Tvar (tr_var a) + | _, [a; b] when c = Lazy.force coq_reFloat2 -> + Tconst (Constant.create (tr_float 2 a b)) + | _, [a] when c = Lazy.force coq_reInteger -> + Tconst (Constant.create (1, tr_arith_constant a, 0)) + | _, [op;a;b] when c = Lazy.force coq_reBinary -> + Tbinop (tr_binop op, tr_term a, tr_term b) + | _, [op;a] when c = Lazy.force coq_reUnary -> + Tunop (tr_unop op, tr_term a) | _ -> - msgnl (str "tr_term: " ++ Printer.pr_constr c0); raise NotGappa + msgnl (str "tr_term: " ++ Printer.pr_constr c0); + assert false let tr_rle c = let c, args = decompose_app c in match kind_of_term c, args with - | _, [a;b] when c = Lazy.force coq_Rle -> tr_term a, tr_term b - | _ -> raise NotGappa + | _, [a;b] when c = Lazy.force coq_Rle -> + begin match decompose_app a, decompose_app b with + | (ac, [at]), (bc, [bt]) + when ac = Lazy.force coq_convert && bc = Lazy.force coq_convert -> + at, bt + | _ -> + raise NotGappa + end + | _ -> + raise NotGappa let tr_pred c = let c, args = decompose_app c in match kind_of_term c, args with | _, [a;b] when c = build_coq_and () -> begin match tr_rle a, tr_rle b with - | (Tconst c1, t1), (t2, Tconst c2) when t1 = t2 -> Pin (t1,c1,c2) - | _ -> raise NotGappa + | (c1, t1), (t2, c2) when t1 = t2 -> + begin match tr_term c1, tr_term c2 with + | Tconst c1, Tconst c2 -> + Pin (tr_term t1, c1, c2) + | _ -> + raise NotGappa + end + | _ -> + raise NotGappa end - | _ -> raise NotGappa + | _ -> + raise NotGappa + +let is_R c = match decompose_app c with + | c, [] when c = Lazy.force coq_R -> true + | _ -> false let tr_hyps = List.fold_left (fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) [] -let gappa gl = +let constr_of_string gl s = + let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in + Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s) + +let var_name = function + | Name id -> + let s = string_of_id id in + let s = String.sub s 1 (String.length s - 1) in + mkVar (id_of_string s) + | Anonymous -> + assert false + +let build_proof_term c0 = + let bl,c = decompose_lam c0 in + List.fold_right + (fun (x,t) pf -> + mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |])) + bl c0 + +let gappa_internal gl = try let c = tr_pred (pf_concl gl) in - call_gappa (tr_hyps (pf_hyps_types gl)) c; - Tacticals.tclIDTAC gl - with NotGappa -> - error "not a gappa goal" + let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in + msgnl (str s); + let pf = constr_of_string gl s in + let pf = build_proof_term pf in + Tacticals.tclTHEN (Tactics.refine pf) Tactics.assumption gl + with + | NotGappa -> error "not a gappa goal" + | GappaFailed -> error "gappa failed" + | GappaProofFailed -> error "incorrect gappa proof term" + +(* +Local Variables: +compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt contrib/dp/Gappa.vo" +End: +*) + diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4 index f7c5135bd..7acbce26d 100644 --- a/contrib/dp/g_dp.ml4 +++ b/contrib/dp/g_dp.ml4 @@ -41,7 +41,7 @@ TACTIC EXTEND Gwhy END TACTIC EXTEND Gappa - [ "gappa" ] -> [ Dp_gappa.gappa ] + [ "gappa_internal" ] -> [ Dp_gappa.gappa_internal ] END (* should be part of basic tactics syntax *) diff --git a/contrib/dp/test_gappa.v b/contrib/dp/test_gappa.v new file mode 100644 index 000000000..1eba44d90 --- /dev/null +++ b/contrib/dp/test_gappa.v @@ -0,0 +1,46 @@ +Require Export Gappa. +Require Export Gappa_library. +Require Export Reals. + +Open Scope Z_scope. +Open Scope R_scope. + +Ltac gappa := gappa_prepare; gappa_internal. + +Lemma test1 : + forall x y:R, + 0 <= x <= 1 -> + 0 <= -y <= 1 -> + 0 <= x * (-y) <= 1. +Proof. + gappa. +Qed. + +Lemma test2 : + forall x y:R, + 0 <= x <= 3 -> + 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)). +Proof. + gappa. +Qed. + +Lemma test3 : + forall x y z:R, + 0 <= x - y <= 3 -> + -2 <= y - z <= 4 -> + -2 <= x - z <= 7. +Proof. + gappa. +Qed. + +Lemma test4 : + forall x1 x2 y1 y2 : R, + 1 <= Rabs y1 <= 1000 -> + 1 <= Rabs y2 <= 1000 -> + - powerRZ 2 (-53) <= (x1 - y1) / y1 <= powerRZ 2 (-53) -> + - powerRZ 2 (-53) <= (x2 - y2) / y2 <= powerRZ 2 (-53) -> + - powerRZ 2 (-51) <= (x1 * x2 - y1 * y2) / (y1 * y2) <= powerRZ 2 (-51). +Proof. + gappa. + + |