Commit 687917a3 authored by Heiko Becker's avatar Heiko Becker

Prove existential rewriting lemma for evaluations

parent c2fce16b
......@@ -93,6 +93,29 @@ Proof.
rewrite (IHe2 v3 v5); auto.
Qed.
Lemma existential_rewriting (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
(eval_exp eps cenv (Binop b e1 e2) v <->
exists v1 v2,
eval_exp eps cenv e1 v1 /\
eval_exp eps cenv e2 v2 /\
eval_exp eps (updEnv 1 v1 (updEnv 2 v2 cenv)) (Binop b (Var R 1) (Var R 2)) v).
Proof.
split.
- intros eval_bin.
inversion eval_bin; subst.
exists v1, v2.
repeat split; try auto.
constructor; try auto.
constructor; auto.
constructor; auto.
- intros exists_val.
destruct exists_val as [v1 [v2 [eval_e1 [eval_e2 eval_e_env]]]].
inversion eval_e_env; subst.
inversion H4; inversion H5; subst.
unfold updEnv in *; simpl in *.
constructor; auto.
Qed.
(**
Using the parametric expressions, define boolean expressions for conditionals
**)
......
Require Import Coq.QArith.QArith.
Require Export Daisy.Infra.Abbrevs Daisy.Expressions.
Definition analysisResult :Type := exp Q -> intv * error.
\ No newline at end of file
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.Setoids.Setoid.
Require Import Daisy.Infra.RealConstruction.
(**
TODO REORDER AND DOCUMENT
......@@ -76,3 +77,8 @@ Proof.
rewrite Rsqr_0 in Rabs_eq.
apply Rsqr_0_uniq in Rabs_eq; assumption.
Qed.
(**
Define the machine epsilon for floating point operations.
Current value: 2^(-53)
**)
Definition machineEpsilon:R := realFromNum 1 1 53.
\ No newline at end of file
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