Skip to content

GitLab

Commit 970c1b8a authored by Raphaël Monat's avatar Raphaël Monat
Browse files
Options

Port of Interval Validation to mixed precision. Needed some auxiliary lemmas... 

Port of Interval Validation to mixed precision. Needed some auxiliary lemmas related to the typing of expressions.
parent a084a817
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 433 additions and 477 deletions
coq/Expressions.v
View file @ 970c1b8a
......@@ -2,7 +2,7 @@
Formalization of the base expression language for the daisy framework
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.RealRationalProps.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
(**
......@@ -106,7 +106,30 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
end
end.
Lemma expEqBool_refl e:
(* Lemma expEqBool_eq e1 e2: *)
(* e1 = e2 -> *)
(* expEqBool e1 e2 = true. *)
(* Proof. *)
(* revert e1 e2. *)
(* induction e1; intros; split; intros. *)
(* - simpl in H. destruct e2; try inversion H; apply andb_true_iff in H; destruct H. *)
(* f_equal. *)
(* + apply EquivEqBoolEq; auto. *)
(* + apply beq_nat_true; auto. *)
(* - simpl. destruct e2; try inversion H. *)
(* rewrite mTypeEqBool_refl. *)
(* simpl. *)
(* symmetry; apply beq_nat_refl. *)
(* - simpl in H; destruct e2; try inversion H. apply andb_true_iff in H; destruct H. *)
(* f_equal. *)
(* + apply EquivEqBoolEq; auto. *)
(* + admit. *)
(* - *)
Lemma expEqBool_refl e:
expEqBool e e = true.
Proof.
induction e; apply andb_true_iff; split; simpl in *; auto; try (apply EquivEqBoolEq; auto).
......@@ -118,6 +141,45 @@ Proof.
apply IHe1. apply IHe2.
Qed.
Lemma beq_nat_sym a b:
beq_nat a b = beq_nat b a.
Proof.
case_eq (a =? b); intros.
- apply beq_nat_true in H.
rewrite H.
apply beq_nat_refl.
- apply beq_nat_false in H.
case_eq (b =? a); intros.
+ apply beq_nat_true in H0.
rewrite H0 in H.
auto.
+ auto.
Qed.
Lemma expEqBool_sym e e':
expEqBool e e' = expEqBool e' e.
Proof.
revert e'.
induction e; intros e'; destruct e'; simpl; try auto.
- f_equal.
+ apply mTypeEqBool_sym; auto.
+ apply beq_nat_sym.
- f_equal.
+ apply mTypeEqBool_sym; auto.
+ apply Qeq_bool_sym.
- f_equal.
+ destruct u; auto.
+ apply IHe.
- f_equal.
+ destruct b; auto.
+ f_equal.
* apply IHe1.
* apply IHe2.
- f_equal.
+ apply mTypeEqBool_sym; auto.
+ apply IHe.
Qed.
Fixpoint toRExp (e:exp Q) :=
match e with
|Var _ m v => Var R m v
......@@ -158,10 +220,10 @@ using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
**)
Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
| Var_load m (*m1*) x v:
(* isMorePrecise m m1 = true ->*)
| Var_load m m1 x v:
isMorePrecise m m1 = true ->
(**mTypeEqBool m m1 = true ->*)
E x = Some (v, m) ->
E x = Some (v, m1) ->
eval_exp E (Var R m x) v m
| Const_dist m n delta:
Rle (Rabs delta) (Q2R (meps m)) ->
......@@ -222,7 +284,7 @@ Proof.
induction f; intros v1 v2 m1 m10_eq eval_v1 eval_v2.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
rewrite H7 in H3; inversion H3; subst; auto.
rewrite H9 in H4; inversion H4; subst; auto.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
- inversion eval_v1; inversion eval_v2; subst; auto;
......
coq/Infra/MachineType.v
View file @ 970c1b8a
......@@ -54,6 +54,20 @@ Definition mTypeEqBool (m1:mType) (m2:mType) :=
| _, _ => false
end.
Lemma mTypeEqBool_sym (m1:mType) (m2:mType):
forall b, mTypeEqBool m1 m2 = b -> mTypeEqBool m2 m1 = b.
Proof.
intros.
destruct b, m1, m2; simpl; cbv; auto.
Qed.
Lemma mTypeEqBool_refl (m:mType):
mTypeEqBool m m = true.
Proof.
intros. destruct m; cbv; auto.
Qed.
(* Definition mTypeEqComp (m1:mType) (m2:mType) := *)
(* Qeq_bool (meps m1) (meps m2). *)
......@@ -71,6 +85,7 @@ Proof.
split; intros; case_eq m1; intros; case_eq m2; intros; auto; rewrite H0 in H; rewrite H1 in H; cbv in H; inversion H; auto.
Qed.
(* Definition mTypeEq: relation mType := *)
(* fun m1 m2 => Qeq (meps m1) (meps m2). *)
......
coq/IntervalValidation.v
View file @ 970c1b8a
This diff is collapsed.
coq/Typing.v
View file @ 970c1b8a
(**
Right now, we need to know the types of each expression in the
~validErrorbound~ function (otherwise, it is impossible to know which
epsilon to use to check the error bounds). For now, expressions are
only typed for the variables and downcasting operators.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.RealRationalProps Daisy.Expressions.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals Coq.MSets.MSets.
Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
......@@ -51,6 +44,17 @@ Fixpoint typeExpression (e:exp Q) (e':exp Q) : option mType :=
else (tE1 e')
end.
(* NB: one might be tempted to prove the following lemma: *)
(* Lemma typeExpressionPropagatesNone e e0: *)
(* isSubExpression e0 e = true -> *)
(* typeExpression e e0 = None -> *)
(* typeExpression e e = None. *)
(* However, due to the definition of typeExpression, this is not true: *)
(* typeExpression (Binop b e1 e2) (Binop b e1 e2) = computeJoin (typeExpression e1 e1) (typeExpression e2 e2). *)
(* But we can have typeExpression e1 e0 = typeExpression e2 e0 = None. *)
(* Ie, when computing the types of Binop b e1 e2, we do not check if typing is coherent for all subexpressions *)
Lemma detTypingBinop (f1 f2: exp Q) (b:binop) (m m0 m1 m2: mType) x:
typeExpression (Binop b f1 f2) (Var Q m0 x) = Some m ->
typeExpression f1 (Var Q m0 x) = Some m1 ->
......@@ -71,8 +75,6 @@ Proof.
+ inversion H.
Qed.
Eval compute in (typeExpression (Binop Plus (Unop Neg (Var Q M32 1)) (Var Q M64 2)) (Var Q M32 1)).
Lemma typeExpressionIsSound e E v m:
eval_exp E (toRExp e) v m ->
(typeExpression e) e = Some m.
......@@ -105,211 +107,113 @@ Proof.
rewrite H1,H2; auto.
Qed.
(* (** A function computing a correct typing of expressions (option needed in case of error) **) *)
(* Fixpoint typeExpression (e:exp Q) : option mType := *)
(* match e with *)
(* |Var _ m n => Some m *)
(* |Const m n => Some m *)
(* |Unop o e1 => *)
(* match (typeExpression e1) with *)
(* | None => None *)
(* | Some m => Some m *)
(* end *)
(* |Binop b e1 e2 => *)
(* match (typeExpression e1), (typeExpression e2) with *)
(* | Some m1, Some m2 => Some (computeJoin m1 m2) *)
(* | _, _ => None *)
(* end *)
(* |Downcast m e1 => *)
(* match (typeExpression e1) with *)
(* | Some m1 => if isMorePrecise m1 m then Some m else None *)
(* | None => None *)
(* end *)
(* end. *)
(* (** A soundness theorem for typing **) *)
(* (** TODO: equivalence? **) *)
(* Theorem typingIsSound (e:exp Q): *)
(* forall v E M, *)
(* eval_exp E (toRExp e) v M -> *)
(* typeExpression e = Some M. *)
(* Proof. *)
(* revert e; induction e; intros; inversion H; subst; simpl; try auto. *)
(* - remember (typeExpression e) as te; destruct te; eapply IHe; eauto. *)
(* - remember (typeExpression e) as te; destruct te; eapply IHe; eauto. *)
(* - remember (typeExpression e1) as te1; destruct te1; *)
(* remember (typeExpression e2) as te2; destruct te2; *)
(* pose proof (IHe1 v1 E m1 H7); *)
(* pose proof (IHe2 v2 E m2 H8); *)
(* inversion H0; inversion H1; subst. *)
(* assert (computeJoin m1 m2 = M) by (symmetry; apply isJoinComputeJoin; auto). *)
(* rewrite H2; auto. *)
(* - remember (typeExpression e) as te; destruct te; *)
(* pose proof (IHe v1 E m1 H6); inversion H0; subst. *)
(* rewrite H2; auto. *)
(* Qed. *)
(* (** Fully typed Expression **) *)
(* Inductive typedExp (V:Type): Type := *)
(* | tVar: mType -> nat -> typedExp V *)
(* | tConst: mType -> V -> typedExp V *)
(* | tUnop: mType -> unop -> typedExp V -> typedExp V *)
(* | tBinop: mType -> binop -> typedExp V -> typedExp V -> typedExp V *)
(* | tDowncast: mType -> typedExp V -> typedExp V. *)
(* Fixpoint getTypeR (e: typedExp R) : mType := *)
(* match e with *)
(* | tVar _ m _ => m *)
(* | tConst m _ => m *)
(* | tUnop m _ _ => m *)
(* | tBinop m _ _ _ => m *)
(* | tDowncast m _ => m *)
(* end. *)
(* Fixpoint getTypeQ (e: typedExp Q) : mType := *)
(* match e with *)
(* | tVar _ m _ => m *)
(* | tConst m _ => m *)
(* | tUnop m _ _ => m *)
(* | tBinop m _ _ _ => m *)
(* | tDowncast m _ => m *)
(* end. *)
(* Fixpoint toRTExp (e: typedExp Q) : typedExp R := *)
(* match e with *)
(* | tVar _ m n => tVar R m n *)
(* | tConst m n => tConst m (Q2R n) *)
(* | tUnop m o e1 => tUnop m o (toRTExp e1) *)
(* | tBinop m o e1 e2 => tBinop m o (toRTExp e1) (toRTExp e2) *)
(* | tDowncast m e1 => tDowncast m (toRTExp e1) *)
(* end. *)
(* Fixpoint texpEquivBool (e1:typedExp Q) (e2:typedExp Q) := *)
(* match e1,e2 with *)
(* |tVar _ m1 v1, tVar _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2) *)
(* |tConst m1 n1, tConst m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2) *)
(* |tUnop _ o1 e11, tUnop _ o2 e22 => andb (unopEqBool o1 o2) (texpEquivBool e11 e22) *)
(* |tBinop _ o1 e11 e12, tBinop _ o2 e21 e22 => andb (binopEqBool o1 o2) (andb (texpEquivBool e11 e21) (texpEquivBool e12 e22)) *)
(* |tDowncast m1 f1, tDowncast m2 f2 => andb (mTypeEqBool m1 m2) (texpEquivBool f1 f2) *)
(* |_, _ => false *)
(* end. *)
(* (** Eval_exp for typed expressions **) *)
(* (** TODO: not the same as eval_exp (binop_dist, and var_load?) **) *)
(* Inductive eval_exp_t (E:env) : typedExp R -> R -> Prop := *)
(* | tVar_load m m1 x v: *)
(* isMorePrecise m m1 = true -> *)
(* E x = Some (v, m1) -> *)
(* eval_exp_t E (tVar R m x) v *)
(* | tConst_dist m n delta: *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E (tConst m n) (perturb n delta) *)
(* | tUnop_neg m f1 v1: *)
(* m = getTypeR f1 -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E (tUnop m Neg f1) (evalUnop Neg v1) *)
(* | tUnop_inv m m1 f1 v1 delta: *)
(* m1 = getTypeR f1 -> *)
(* isMorePrecise m m1 = true -> *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E (tUnop m Inv f1) (perturb (evalUnop Inv v1) delta) *)
(* | tBinop_dist m m1 m2 op f1 f2 v1 v2 delta: *)
(* m1 = getTypeR f1 -> *)
(* m2 = getTypeR f2 -> *)
(* isJoinOf m m1 m2 = true -> *)
(* (* isMorePrecise m m1 = true -> *) *)
(* (* isMorePrecise m m2 = true -> *) *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E f2 v2 -> *)
(* eval_exp_t E (tBinop m op f1 f2) (perturb (evalBinop op v1 v2) delta) *)
(* | tDowncast_dist m m1 f1 v1 delta: *)
(* (* Qle_bool (meps m1) (meps m) = true ->*) *)
(* isMorePrecise m1 m = true -> *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E (tDowncast m f1) (perturb v1 delta). *)
Fixpoint isSubExpression (e':exp Q) (e:exp Q) :=
orb (expEqBool e e') (
match e with
|Var _ _ _ => false
|Const _ _ => false
|Unop o1 e1 => isSubExpression e' e1
|Binop b e1 e2 => orb (isSubExpression e' e1) (isSubExpression e' e2)
|Downcast m e1 => isSubExpression e' e1
end).
Lemma typeNotSubExpr e e1:
isSubExpression e1 e = false -> typeExpression e e1 = None.
Proof.
revert e e1; induction e; intros.
- simpl in H. rewrite orb_false_r in H.
simpl; rewrite H; auto.
- simpl in H; rewrite orb_false_r in H.
simpl; rewrite H; auto.
- simpl in H.
case_eq (isSubExpression e1 e); intros; rewrite H0 in H; auto.
+ rewrite orb_true_r in H.
inversion H.
+ rewrite orb_false_r in H.
simpl; rewrite H; auto.
- simpl in H.
case_eq (isSubExpression e0 e1); intros;
case_eq (isSubExpression e0 e2); intros; rewrite H0,H1 in H; auto.
+ rewrite orb_true_r in H; inversion H.
+ rewrite orb_true_r in H; inversion H.
+ rewrite orb_true_r in H; inversion H.
+ rewrite orb_false_r in H.
simpl; rewrite H.
specialize (IHe1 e0 H0).
specialize (IHe2 e0 H1).
rewrite IHe1, IHe2.
auto.
- simpl in H.
case_eq (isSubExpression e1 e); intros; rewrite H0 in H.
+ rewrite orb_true_r in H; inversion H.
+ rewrite orb_false_r in H. simpl; rewrite H; auto.
Qed.
(* (** A function computing a correct typing of expressions (option needed in case of error) **) *)
(* Fixpoint typeExpression (e:exp Q) : option (typedExp Q) := *)
(* match e with *)
(* |Var _ m n => Some (tVar Q m n) *)
(* |Const m n => Some (tConst m n) *)
(* |Unop o e1 => *)
(* match (typeExpression e1) with *)
(* | None => None *)
(* | Some te1 => Some (tUnop (getTypeQ te1) o te1) *)
(* end *)
(* |Binop b e1 e2 => *)
(* match (typeExpression e1), (typeExpression e2) with *)
(* | Some te1, Some te2 => *)
(* let prec := computeJoin (getTypeQ te1) (getTypeQ te2) in *)
(* Some (tBinop prec b te1 te2) *)
(* | _, _ => None *)
(* end *)
(* |Downcast m e1 => *)
(* match (typeExpression e1) with *)
(* | Some te1 => *)
(* Some (tDowncast m te1) *)
(* | None => None *)
(* end *)
(* end. *)
(* Lemma convQR (e: typedExp Q): *)
(* getTypeQ e = getTypeR (toRTExp e). *)
(* Proof. *)
(* revert e; induction e; try (simpl in *; auto). *)
(* Qed. *)
Lemma typedVarIsUsed e m m0 v:
typeExpression e (Var Q m0 v) = Some m ->
NatSet.In v (usedVars e).
Proof.
intros; induction e.
- simpl in *.
case_eq (mTypeEqBool m1 m0 && (n =? v)); intros; auto; rewrite H0 in H.
+ andb_to_prop H0.
apply InA_cons.
left; symmetry.
apply beq_nat_true; auto.
+ inversion H.
- simpl in *; inversion H.
- simpl in *; apply IHe; auto.
- pose proof (detTypingBinop e1 e2 b).
case_eq (typeExpression e1 (Var Q m0 v)); case_eq (typeExpression e2 (Var Q m0 v)); intros; auto.
+ specialize (H0 _ _ _ _ _ H H2 H1) as [H01 H02]; subst.
simpl; apply NatSet.union_spec; left; apply IHe1; auto.
+ simpl.
simpl in H; rewrite H1,H2 in H; inversion H; subst.
apply NatSet.union_spec; left; apply IHe1; auto.
+ simpl; simpl in H.
rewrite H1,H2 in H; inversion H; subst.
apply NatSet.union_spec; right; apply IHe2; auto.
+ simpl in H; rewrite H1, H2 in H.
inversion H.
- apply IHe; auto.
Qed.
Lemma binop_type_unfolding b f1 f2 mf:
typeExpression (Binop b f1 f2) (Binop b f1 f2) = Some mf ->
(exists m0 m1, typeExpression f1 f1 = Some m0 /\ typeExpression f2 f2 = Some m1 /\ mf = computeJoin m0 m1).
Proof.
intros.
simpl in H.
pose proof (expEqBool_refl (Binop b f1 f2)); simpl in H0; rewrite H0 in H.
case_eq (typeExpression f1 f1); intros; case_eq (typeExpression f2 f2); intros; try rewrite H1 in H; try rewrite H2 in H; inversion H.
exists m, m0.
auto.
Qed.
(* (** A soundness theorem for typing **) *)
(* (** TODO: equivalence? **) *)
(* Theorem typing_sound (e:exp Q) (e': typedExp Q): *)
(* forall v E M, *)
(* typeExpression e = Some e' -> *)
(* eval_exp E (toRExp e) v M -> *)
(* eval_exp_t E (toRTExp e') v /\ (getTypeQ e' = M). *)
(* Lemma helpinglemma (e:exp Q) m v : *)
(* typeExpression e (Var Q m v) = Some m -> *)
(* isSubExpression (Var Q m v) e = true. *)
(* Proof. *)
(* revert e e'. *)
(* induction e; intros; inversion H; subst; inversion H0; subst. *)
(* - split; try auto. *)
(* econstructor; eauto. *)
(* - split; try auto. *)
(* constructor; auto. *)
(* - remember (typeExpression e) as te; destruct te; inversion H2; subst; *)
(* assert (eval_exp_t E (toRTExp t) v1 /\ getTypeQ t = M) as [Hi1 Hi2] by (apply IHe; auto); subst. *)
(* split; try auto. *)
(* constructor; try auto. *)
(* apply convQR. *)
(* - remember (typeExpression e) as te; destruct te; inversion H2; subst; *)
(* assert (eval_exp_t E (toRTExp t) v1 /\ getTypeQ t = M) as [Hi1 Hi2] by (apply IHe; auto); subst. *)
(* split; try auto. *)
(* econstructor; try auto. *)
(* rewrite convQR; apply isMorePrecise_refl. *)
(* - remember (typeExpression e1) as te1; destruct te1; inversion H2; *)
(* remember (typeExpression e2) as te2; destruct te2; inversion H2; subst; *)
(* assert (Some t = Some t) as St by auto; assert (Some t0 = Some t0) as St0 by auto; *)
(* destruct (IHe1 t v1 E m1 St H9) as [Hi1e Hi1m]; *)
(* destruct (IHe2 t0 v2 E m2 St0 H10) as [Hi2e Hi2m]. *)
(* split. *)
(* + econstructor; eauto. *)
(* * rewrite <- convQR. *)
(* rewrite <- convQR. *)
(* apply computeJoinIsJoin. *)
(* * assert (M = computeJoin m1 m2). *)
(* unfold computeJoin. *)
(* case_eq (isMorePrecise m1 m2); intros; auto; unfold isJoinOf in H5; rewrite H1 in H5; *)
(* apply EquivEqBoolEq; auto. *)
(* rewrite Hi1m; rewrite Hi2m; rewrite <- H1; auto. *)
(* + rewrite Hi1m; rewrite Hi2m. *)
(* unfold getTypeQ. *)
(* unfold computeJoin. *)
(* case_eq (isMorePrecise m1 m2); intros; auto; unfold isJoinOf in H5; rewrite H1 in H5; symmetry; apply EquivEqBoolEq; auto. *)
(* - remember (typeExpression e) as te; destruct te; inversion H2; subst; *)
(* assert (eval_exp_t E (toRTExp t) v1 /\ getTypeQ t = m1) as [Hi1 Hi2] by (apply IHe; auto); subst. *)
(* split. *)
(* + econstructor; eauto. *)
(* + simpl; trivial. *)
(* revert e; induction e; intros. *)
(* - unfold typeExpression in H. *)
(* case_eq (expEqBool (Var Q m0 n) (Var Q m v)); intros; rewrite H0 in H; inversion H; auto. *)
(* subst; simpl. *)
(* unfold expEqBool in H0. *)
(* rewrite orb_false_r. *)
(* auto. *)
(* - simpl in H; inversion H. *)
(* - simpl in *; apply IHe; auto. *)
(* - simpl in *. *)
(* apply orb_true_iff. *)
(* case_eq (typeExpression e1 (Var Q m v)); intros; rewrite H0 in H; auto. *)
(* + left. *)
(* apply IHe1. *)
(* rewrite H0. *)
(* apply typingVarDet in H0; rewrite H0; auto. *)
(* + case_eq (typeExpression e2 (Var Q m v)); intros; rewrite H1 in H; auto. *)
(* * right. apply IHe2. rewrite H1; apply typingVarDet in H1; rewrite H1; auto. *)
(* * inversion H. *)
(* - simpl in *; apply IHe; auto. *)
(* Qed. *)
coq/ssaPrgs.v
View file @ 970c1b8a
......@@ -50,6 +50,7 @@ Proof.
specialize (fVars_live n in_n).
destruct fVars_live as [vR E_def].
exists vR; econstructor; eauto.
cbv; auto.
- exists (perturb (Q2R v) 0); constructor.
simpl (meps M0); rewrite Rabs_R0; rewrite Q2R0_is_0; lra.
- assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0)
......@@ -208,11 +209,11 @@ Proof.
- split; intros eval_Var.
+ inversion eval_Var; subst.
(*assert (m1 = M0) by (apply ifisMorePreciseM0; auto); subst.*)
rewrite agree_on_vars in H2.
apply Var_load; auto.
rewrite agree_on_vars in H3.
eapply Var_load; eauto.
+ inversion eval_Var; subst.
rewrite <- agree_on_vars in H2.
apply Var_load; auto.
rewrite <- agree_on_vars in H3.
eapply Var_load; eauto.
- split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
- split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
+ erewrite IHe; eauto.
......@@ -279,7 +280,7 @@ Proof.
rewrite <- NatSet.mem_spec in valid_vars.
rewrite valid_vars in *; congruence.
+ econstructor.
auto.
eauto.
rewrite H; auto.
- inversion eval_e; subst; constructor; auto.
- inversion eval_e; subst; econstructor; eauto.
......@@ -321,10 +322,10 @@ Proof.
+ unfold updEnv in eval_upd. simpl in *.
inversion eval_upd; subst.
case_eq (n =? x); intros; try auto.
* rewrite H in H2.
inversion H2; subst; auto.
* rewrite H in H2.
apply Var_load; auto.
* rewrite H in H3.
inversion H3; subst; auto.
* rewrite H in H3.
eapply Var_load; eauto.
+ simpl in eval_subst.
case_eq (n =? x); intros n_eq_case;
rewrite n_eq_case in eval_subst.
......@@ -332,11 +333,11 @@ Proof.
assert (updEnv x M0 v E n = Some (v_res, M0)).
{ unfold updEnv; rewrite n_eq_case.
f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. }
{ econstructor; eauto. }
{ econstructor; eauto. cbv; auto. }
* simpl. inversion eval_subst; subst.
assert (E n = updEnv x M0 v E n).
{ unfold updEnv; rewrite n_eq_case; reflexivity. }
{ rewrite H in H2. apply Var_load; auto. } (*unfold updEnv in *. rewrite n_eq_case in *. unfold toREvalEnv. apply H4. }*)
{ rewrite H in H3. eapply Var_load; eauto. } (*unfold updEnv in *. rewrite n_eq_case in *. unfold toREvalEnv. apply H4. }*)
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; auto.
+ inversion eval_subst; constructor; auto.
......
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