Commit 29a02e9c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Recognize Flocq's bpow as a constant.

parent 5b2b4140
......@@ -114,8 +114,7 @@ Definition cons_unique (e : expr) (l : list expr) :=
Fixpoint split_expr (e : expr) (lp lc : list expr) :=
match e with
| Evar n => Scomposed lp lc
| Eint n => Sconst
| Econst_pi => Sconst
| Econst o => Sconst
| Eunary o e1 =>
match split_expr e1 lp lc with
| Sconst => Sconst
......@@ -138,15 +137,15 @@ Fixpoint split_expr (e : expr) (lp lc : list expr) :=
Theorem split_expr_correct :
forall vars e lp lc,
(forall n, eval (nth n lc (Eint 0)) vars = eval (nth n lc (Eint 0)) nil) ->
(forall n, eval (nth n lc (Econst (Int 0))) vars = eval (nth n lc (Econst (Int 0))) nil) ->
match split_expr e lp lc with
| Sconst => eval e vars = eval e nil
| Scomposed lp' lc' =>
forall n, eval (nth n lc' (Eint 0)) vars = eval (nth n lc' (Eint 0)) nil
forall n, eval (nth n lc' (Econst (Int 0))) vars = eval (nth n lc' (Econst (Int 0))) nil
end.
Proof.
intros vars.
induction e as [n|n| |o e1 IHe1|o e1 IHe1 e2 IHe2] ; intros lp lc Hc ; simpl ; try easy.
induction e as [n|o|o e1 IHe1|o e1 IHe1 e2 IHe2] ; intros lp lc Hc ; simpl ; try easy.
specialize (IHe1 lp lc Hc).
destruct split_expr as [|lp' lc'].
now apply f_equal.
......@@ -154,9 +153,9 @@ induction e as [n|n| |o e1 IHe1|o e1 IHe1 e2 IHe2] ; intros lp lc Hc ; simpl ; t
specialize (IHe2 lp lc Hc).
assert (H: forall e l,
eval e vars = eval e nil ->
(forall n, eval (nth n l (Eint 0)) vars = eval (nth n l (Eint 0)) nil) ->
(forall n, eval (nth n l (Econst (Int 0))) vars = eval (nth n l (Econst (Int 0))) nil) ->
forall n,
eval (nth n (rcons_unique e l) (Eint 0)) vars = eval (nth n (rcons_unique e l) (Eint 0)) nil).
eval (nth n (rcons_unique e l) (Econst (Int 0))) vars = eval (nth n (rcons_unique e l) (Econst (Int 0))) nil).
intros e l He Hl.
induction l as [|h t IH] ; simpl.
now intros [|[|n]].
......@@ -202,14 +201,14 @@ Definition find_expr (e : expr) (vars : nat) (lp lc : list expr) :=
Theorem find_expr_correct :
forall e vars lp lc,
match find_expr e vars lp lc with
| Some n => nth n (lp ++ map Evar (seq 0 vars) ++ lc) (Eint 0) = e
| Some n => nth n (lp ++ map Evar (seq 0 vars) ++ lc) (Econst (Int 0)) = e
| None => True
end.
Proof.
intros e vars lp lc.
assert (H1: forall l n,
match find_expr_aux e n l with
| Some k => (n <= k < n + length l)%nat /\ nth (k - n) l (Eint 0) = e
| Some k => (n <= k < n + length l)%nat /\ nth (k - n) l (Econst (Int 0)) = e
| None => True
end).
induction l as [|h t IH].
......@@ -242,7 +241,7 @@ set (foo :=
end).
assert (H2:
match foo with
| Some n => nth n (lp ++ map Evar (seq 0 vars) ++ lc) (Eint 0) = e
| Some n => nth n (lp ++ map Evar (seq 0 vars) ++ lc) (Econst (Int 0)) = e
| None => True
end).
unfold foo.
......@@ -261,7 +260,7 @@ assert (H2:
rewrite app_nth2 ; rewrite map_length, seq_length.
now rewrite <- Nat.sub_add_distr.
lia.
destruct e as [| | |o n1|o n1 n2] ; simpl ; try easy.
destruct e as [n|o|o n1|o n1 n2] ; simpl ; try easy.
destruct (Nat.ltb_spec n vars) as [H|H] ; try easy.
rewrite app_nth2 by apply le_plus_l.
rewrite minus_plus.
......@@ -278,8 +277,7 @@ Fixpoint decompose (vars : nat) (p : list term) (lp lc : list expr) :=
| cons h t =>
match h with
| Evar n => decompose vars (cons (Forward (length t + n)) p) t lc
| Eint _ => None
| Econst_pi => None
| Econst _ => None
| Eunary o e1 =>
match find_expr e1 vars t lc with
| Some n => decompose vars (cons (Unary o n) p) t lc
......@@ -299,7 +297,7 @@ Fixpoint decompose (vars : nat) (p : list term) (lp lc : list expr) :=
Theorem decompose_correct :
forall vars p lp lc,
(forall vars n, eval (nth n lc (Eint 0)) vars = eval (nth n lc (Eint 0)) nil) ->
(forall vars n, eval (nth n lc (Econst (Int 0))) vars = eval (nth n lc (Econst (Int 0))) nil) ->
let lc' := map (fun c => eval c nil) lc in
match decompose (length vars) p lp lc with
| None => True
......@@ -315,14 +313,14 @@ easy.
intros p.
simpl.
assert (H: forall n e,
nth n (t ++ map Evar (seq 0 (length vars)) ++ lc) (Eint 0) = e ->
nth n (t ++ map Evar (seq 0 (length vars)) ++ lc) (Econst (Int 0)) = e ->
nth n (map (fun c : expr => eval c (vars ++ lc')) t ++ vars ++ lc') 0%R = eval e (vars ++ lc')).
intros n e.
destruct (Nat.lt_ge_cases n (length t)) as [H1|H1].
rewrite app_nth1 by apply H1.
intros H.
rewrite app_nth1 by now rewrite map_length.
change 0%R with ((fun c => eval c (vars ++ lc')) (Eint 0)).
change 0%R with ((fun c => eval c (vars ++ lc')) (Econst (Int 0))).
rewrite map_nth.
now rewrite H.
rewrite app_nth2 by apply H1.
......@@ -341,11 +339,11 @@ assert (H: forall n e,
rewrite app_nth2 by apply H2.
intros H.
unfold lc'.
change 0%R with ((fun c => eval c nil) (Eint 0)).
change 0%R with ((fun c => eval c nil) (Econst (Int 0))).
rewrite map_nth, H.
rewrite <- H at 2.
now rewrite Hc, H.
destruct h as [| | |o e1|o e1 e2] ; try easy.
destruct h as [n|o|o e1|o e1 e2] ; try easy.
- specialize (IH (Forward (length t + n) :: p)).
destruct decompose ; try easy.
rewrite IH.
......@@ -384,8 +382,7 @@ Qed.
Fixpoint max_arity (e : expr) (n : nat) :=
match e with
| Evar k => Nat.ltb k n
| Eint _ => true
| Econst_pi => true
| Econst _ => true
| Eunary o e1 => max_arity e1 n
| Ebinary o e1 e2 => if max_arity e1 n then max_arity e2 n else false
end.
......@@ -454,7 +451,7 @@ unfold eval_real'.
intros H' ->.
simpl.
clear -H'.
induction e as [n| | |o e1|o e1 IHe1 e2 IHe2] ; simpl ; try easy.
induction e as [n|o|o e1|o e1 IHe1 e2 IHe2] ; simpl ; try easy.
apply app_nth1.
simpl in H'.
now apply Nat.ltb_lt.
......
......@@ -23,6 +23,9 @@ Require Import Xreal.
Require Import Basic.
Require Import Interval.
Inductive nullary_op : Set :=
| Int (n : Z) | Bpow (r n : Z) | Pi.
Inductive unary_op : Set :=
| Neg | Abs | Inv | Sqr | Sqrt
| Cos | Sin | Tan | Atan | Exp | Ln
......@@ -33,11 +36,24 @@ Inductive binary_op : Set :=
Inductive expr : Set :=
| Evar : nat -> expr
| Eint : Z -> expr
| Econst_pi : expr
| Econst : nullary_op -> expr
| Eunary : unary_op -> expr -> expr
| Ebinary : binary_op -> expr -> expr -> expr.
Definition bpow' (r e : Z) :=
match e with
| 0%Z => 1%R
| Z.pos p => IZR (Z.pow_pos r p)
| Z.neg p => (/ IZR (Z.pow_pos r p))%R
end.
Definition nullary_real (o : nullary_op) : R :=
match o with
| Int n => IZR n
| Bpow r n => bpow' r n
| Pi => PI
end.
Definition unary_real (o : unary_op) : R -> R :=
match o with
| Neg => Ropp
......@@ -66,8 +82,7 @@ Definition binary_real (o : binary_op) : R -> R -> R :=
Fixpoint eval (e : expr) (l : list R) :=
match e with
| Evar n => nth n l 0%R
| Eint n => IZR n
| Econst_pi => PI
| Econst o => nullary_real o
| Eunary o e1 => unary_real o (eval e1 l)
| Ebinary o e1 e2 => binary_real o (eval e1 l) (eval e2 l)
end.
......@@ -123,6 +138,7 @@ Ltac get_vars t l :=
| IZR (Raux.Zceil ?a) => aux_u a
| IZR (Round_NE.ZnearestE ?a) => aux_u a
| PI => l
| Raux.bpow _ _ => l
| IZR ?n => l
| _ => list_add t l
end in
......@@ -163,8 +179,9 @@ Ltac reify t l :=
| IZR (Raux.Zfloor ?a) => aux_u (Nearbyint rnd_DN) a
| IZR (Raux.Zceil ?a) => aux_u (Nearbyint rnd_UP) a
| IZR (Round_NE.ZnearestE ?a) => aux_u (Nearbyint rnd_NE) a
| PI => constr:(Econst_pi)
| IZR ?n => constr:(Eint n)
| PI => constr:(Econst Pi)
| Raux.bpow ?r ?n => constr:(Econst (Bpow (Zaux.radix_val r) n))
| IZR ?n => constr:(Econst (Int n))
| _ =>
let n := list_find t l in
constr:(Evar n)
......@@ -175,6 +192,27 @@ Module Bnd (I : IntervalOps).
Module J := IntervalExt I.
Definition nullary_bnd prec (o : nullary_op) : I.type :=
match o with
| Int n => I.fromZ n
| Bpow r n => I.power_int prec (I.fromZ r) n
| Pi => I.pi prec
end.
Lemma nullary_bnd_correct :
forall prec o,
contains (I.convert (nullary_bnd prec o)) (Xreal (nullary_real o)).
Proof.
intros prec [n|r n|].
- apply I.fromZ_correct.
- simpl.
replace (bpow' r n) with (powerRZ (IZR r) n).
apply J.power_int_correct.
apply I.fromZ_correct.
destruct n as [|n|n] ; simpl ; try rewrite Zpower_pos_powerRZ ; easy.
- apply I.pi_correct.
Qed.
Definition unary_bnd prec (o : unary_op) : I.type -> I.type :=
match o with
| Neg => I.neg
......@@ -239,8 +277,7 @@ Qed.
Fixpoint eval_bnd (prec : I.precision) (e : expr) :=
match e with
| Evar _ => I.nai
| Eint n => I.fromZ n
| Econst_pi => I.pi prec
| Econst o => nullary_bnd prec o
| Eunary o e1 => unary_bnd prec o (eval_bnd prec e1)
| Ebinary o e1 e2 => binary_bnd prec o (eval_bnd prec e1) (eval_bnd prec e2)
end.
......@@ -250,13 +287,11 @@ Theorem eval_bnd_correct :
contains (I.convert (eval_bnd prec e)) (Xreal (eval e nil)).
Proof.
intros prec.
induction e as [n|n| |o e1 IHe1|o e1 IHe1 e2 IHe2].
simpl.
now rewrite I.nai_correct.
apply I.fromZ_correct.
apply I.pi_correct.
now apply unary_bnd_correct.
now apply binary_bnd_correct.
induction e as [n|o|o e1 IHe1|o e1 IHe1 e2 IHe2].
- apply contains_Inan, I.nai_correct.
- apply nullary_bnd_correct.
- now apply unary_bnd_correct.
- now apply binary_bnd_correct.
Qed.
End Bnd.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment