Commit e8dd12b6 authored by Heiko Becker's avatar Heiko Becker

Fix requires after refactoring

parent e44fc7c2
......@@ -2,7 +2,7 @@
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.Expressions.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions.
(**
Next define what a program is.
Currently no loops, only conditionals and assignments
......@@ -14,21 +14,13 @@ Let: nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V
| Nop: cmd V.
(**
Define environment update function for arbitrary type as abbreviation
**)
Definition upd_env (x:nat) (v: R) (E: nat -> R) (y:nat) :R :=
if y =? x
then v
else E y.
(**
Small Step semantics for Daisy language, parametric by evaluation function.
**)
Inductive sstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
let_s x e s env v eps:
eval_exp eps env e v ->
sstep (Let R x e s) env eps s (upd_env x v env)
sstep (Let R x e s) env eps s (updEnv x v env)
|condtrue_s c s t eps env:
bval eps env c True ->
sstep (Ite R c s t) env eps s env
......@@ -37,7 +29,7 @@ Inductive sstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
sstep (Ite R c s t) env eps s env
|ret_s e v eps env:
eval_exp eps env e v ->
sstep (Ret R e) env eps (Nop R) (upd_env 0 v env).
sstep (Ret R e) env eps (Nop R) (updEnv 0 v env).
(**
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function
......@@ -45,7 +37,7 @@ Inductive sstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
Inductive bstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
let_b x e s s' env v eps env2:
eval_exp eps env e v ->
bstep s (upd_env x v env) eps s' env2 ->
bstep s (updEnv x v env) eps s' env2 ->
bstep (Let R x e s) env eps s' env2
|condtrue_b c s1 s2 t eps env env2:
bval eps env c True ->
......@@ -57,4 +49,4 @@ Inductive bstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
bstep (Ite R c s t1) env eps t2 env2
|ret_b e v eps env:
eval_exp eps env e v ->
bstep (Ret R e) env eps (Nop R) (upd_env 0 v env).
\ No newline at end of file
bstep (Ret R e) env eps (Nop R) (updEnv 0 v env).
\ No newline at end of file
(**
Formalization of the base expression language for the daisy framework
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.Infra.RealConstruction.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic.
Require Import Daisy.Infra.RealConstruction Daisy.Infra.RealSimps.
Set Implicit Arguments.
(**
Expressions will use binary operators.
......@@ -64,20 +64,6 @@ Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
eval_exp eps env e1 v1 ->
eval_exp eps env e2 v2 ->
eval_exp eps env (Binop op e1 e2) (perturb (eval_binop op v1 v2) delta).
(**
Prove that using eps = 0 makes the evaluation deterministic
**)
Lemma Rabs_0_impl_eq (d:R):
Rle (Rabs d) R0 -> d = R0.
Proof.
intros abs_leq_0.
pose proof (Rabs_pos d) as abs_geq_0.
pose proof (Rle_antisym (Rabs d) R0 abs_leq_0 abs_geq_0) as Rabs_eq.
rewrite <- Rabs_R0 in Rabs_eq.
apply Rsqr_eq_asb_1 in Rabs_eq.
rewrite Rsqr_0 in Rabs_eq.
apply Rsqr_0_uniq in Rabs_eq; assumption.
Qed.
Lemma perturb_0_val (v:R) (delta:R):
(Rabs delta <= 0)%R ->
......@@ -105,93 +91,6 @@ Proof.
rewrite (IHe2 v3 v5); auto.
Qed.
Lemma Rsub_eq_Ropp_Rplus (a:R) (b:R) :
(a - b = a + (- b))%R.
Proof.
field_simplify; reflexivity.
Qed.
Lemma Rabs_err_simpl:
forall a b,
(Rabs (a - (a * (1 + b))) = Rabs (a * b))%R.
Proof.
intros a b.
rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_plus_distr.
assert (- a + (- (a * b)) = ( - (a * b) + - a))%R by (rewrite Rplus_comm; auto).
rewrite H.
rewrite <- Rsub_eq_Ropp_Rplus.
rewrite Rplus_minus.
rewrite Rabs_Ropp; reflexivity.
Qed.
(**
TODO: Check wether we need Rabs (n * machineEpsilon) instead
**)
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
forall cenv:nat -> R,
eval_exp 0%R cenv (Const n) nR ->
eval_exp machineEpsilon cenv (Const n) nF ->
(Rabs (nR - nF) <= Rabs n * machineEpsilon)%R.
Proof.
intros cenv eval_real eval_float.
inversion eval_real; subst.
rewrite perturb_0_val; auto.
inversion eval_float; subst.
unfold perturb; simpl.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
(**
TODO: Maybe improve bound by adding interval constraint and proving that it is leq than maxAbs of bounds
(nlo <= cenv n <= nhi)%R -> (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
**)
Lemma param_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R):
eval_exp 0%R cenv (Param R n) nR ->
eval_exp machineEpsilon cenv (Param R n) nF ->
(Rabs (nR - nF) <= Rabs (cenv n) * machineEpsilon)%R.
Proof.
intros eval_real eval_float.
inversion eval_real; subst.
rewrite perturb_0_val; auto.
inversion eval_float; subst.
unfold perturb; simpl.
rewrite Rabs_err_simpl.
repeat rewrite Rabs_mult.
apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
Qed.
(*
Lemma add_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp machineEpsilon cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp machineEpsilon cenv e2 e2F ->
eval_exp 0%R cenv (Binop Plus e1 e2) vR ->
eval_exp machineEpsilon cenv (Binop Plus e1 e2) vF ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= err1 + err2 + Rabs vR * machineEpsilon)%R.
Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
inversion plus_real; subst.
rewrite perturb_0_val; auto.
inversion plus_float; subst.
unfold perturb; simpl.
rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_plus_distr.
rewrite (eval_det e1_real H4) in e1_real.
rewrite (eval_det e2_real H5) in e2_real.
pose proof (Rabs_triang (v1 + v2) (- (v0 + v3) + - ((v0 + v3) * delta0))).
*)
(**
Using the parametric expressions, define boolean expressions for conditionals
**)
......
......@@ -3,7 +3,7 @@
TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps.
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound.
......
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