Skip to content

GitLab

Commit 8b9d6c33 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'master' into FM19

parents 02b248c7 c166ad0b
Hide whitespace changes
Inline Side-by-side
README.md
View file @ 8b9d6c33
# Project FloVer
## FM 2019
All implementations included in the FM2019 submission are on the branch [FM2019][2].
The folder `scripts` contains the scripts we used to run the evaluation from the paper.
Changes described in the paper can be found in the folder `coq`. The overall soundness theorem is stated in file `CertificateChecker.v`.
The SMT-based range validator and its soundness proof can be found in file [SMTValidation.v][3], and the Subdivision checker can be found in file [SubdivsChecker.v][4].
## FMCAD 2018
The artifact and scripts used to run the evaluation for FMCAD 2018 can be found on the branch [FMCAD 2018][1].
......@@ -30,7 +37,7 @@ Full support for fixed-point programs is also only available in `affine_arithmet
## Checking Coq certificates
FloVer is known to compile with coq `8.7.2` and `8.8.0`.
FloVer is known to compile with coq `8.8.2`.
To check the Coq certificate, you need to enter the `coq` directory.
Place any certificate you want to have checked into the `output` folder in the
coq directory and then run
......@@ -43,9 +50,8 @@ This will compile all coq files and then in the end the certificate in the outpu
To compile the file `IEEE_connection.v` showing the relation to IEEE754 semantics, it is necessary to install
the Flocq library via opam:
```bash
$ opam install coq-flocq.2.6.1
$ opam install coq-flocq.3.1.0
```
Note that due to some incompatibilities, FloVer currently does not support flocq 3.0.
The coq binary is build in the directory `coq/binary` and you can compile it by
running `make native` in the directory.
......@@ -99,7 +105,7 @@ $ ./cake_checker CERTIFICATE_FILE
## Contributors
In no particular order: Raphael Monat, Nikita Zyuzin, Heiko Becker
In no particular order: Raphael Monat, Nikita Zyuzin, Joachim Bard, Heiko Becker
Acknowledgements
......@@ -107,4 +113,7 @@ Acknowledgements
We would like to thank Jacques-Henri Jourdan for the many insightful discussions
and technical help while working on the initial version of FloVer.
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
\ No newline at end of file
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
[2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FM2019
[3]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SMTValidation.v
[4]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SubdivsChecker.v
\ No newline at end of file
attic/coq/ssaAttic.v 0 → 100644
View file @ 8b9d6c33
(*
Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
(forall n, E1 n = E2 n)->
eval_expr E1 defVars (toREval e) v REAL <->
eval_expr E2 defVars (toREval e) v REAL.
Proof.
revert v E1 E2.
induction e; intros v' E1 E2 agree_on_vars.
- split; intros eval_Var.
+ inversion eval_Var; subst.
rewrite agree_on_vars in H1.
constructor; auto.
+ inversion eval_Var; subst.
rewrite <- agree_on_vars in H1.
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.
+ erewrite IHe; eauto.
+ erewrite <- IHe; eauto.
+ erewrite <- IHe; eauto.
- split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto.
destruct m1; destruct m2; inversion H2.
try (erewrite IHe1; eauto);
try (erewrite IHe2; eauto); auto.
- split; intros eval_Downcast; simpl; simpl in eval_Downcast; erewrite IHe; eauto.
Qed.
Lemma shadowing_free_rewriting_cmd f E1 E2 vR defVars:
(forall n, E1 n = E2 n) ->
bstep (toREvalCmd f) E1 defVars vR REAL <->
bstep (toREvalCmd f) E2 defVars vR REAL.
Proof.
revert E1 E2 defVars vR.
induction f; intros E1 E2 vR agree_on_vars.
- split; intros bstep_Let; inversion bstep_Let; subst.
+ erewrite shadowing_free_rewriting_expr in H8; auto.
econstructor; eauto.
rewrite <- IHf.
apply H10.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
+ erewrite <- shadowing_free_rewriting_expr in H8; auto.
econstructor; eauto.
rewrite IHf.
apply H10.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
- split; intros bstep_Ret; inversion bstep_Ret; subst.
+ erewrite shadowing_free_rewriting_expr in H1; auto.
constructor; auto.
+ erewrite <- shadowing_free_rewriting_expr in H1; auto.
constructor; auto.
Qed.
Lemma dummy_bind_ok e v x v' inVars E defVars:
NatSet.Subset (usedVars e) inVars ->
NatSet.mem x inVars = false ->
eval_expr E defVars (toREval (toRExp e)) v REAL ->
eval_expr (updEnv x v' E) defVars (toREval (toRExp e)) v REAL.
Proof.
revert v x v' inVars E.
induction e; intros v1 x v2 inVars E valid_vars x_not_free eval_e.
- inversion eval_e; subst.
assert ((updEnv x v2 E) n = E n).
+ unfold updEnv.
case_eq (n =? x); try auto.
intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
subst; simpl in *.
hnf in valid_vars.
assert (NatSet.mem x (NatSet.singleton x) = true)
as in_singleton by (rewrite NatSet.mem_spec, NatSet.singleton_spec; auto).
rewrite NatSet.mem_spec in *.
specialize (valid_vars x in_singleton).
rewrite <- NatSet.mem_spec in valid_vars.
rewrite valid_vars in *; congruence.
+ econstructor; eauto.
rewrite H; auto.
- inversion eval_e; subst; constructor; auto.
- inversion eval_e; subst; econstructor; eauto.
- simpl in valid_vars.
inversion eval_e; subst; econstructor; eauto;
destruct m1; destruct m2; inversion H2;
subst.
+ eapply IHe1; eauto.
hnf; intros a in_e1.
apply valid_vars;
rewrite NatSet.union_spec; auto.
+ eapply IHe2; eauto.
hnf; intros a in_e2.
apply valid_vars;
rewrite NatSet.union_spec; auto.
- apply (IHe v1 x v2 inVars E); auto.
Qed.
Fixpoint expr_subst (e:expr Q) x e_new :=
match e with
|Var _ v => if v =? x then e_new else Var Q v
|Unop op e1 => Unop op (expr_subst e1 x e_new)
|Binop op e1 e2 => Binop op (expr_subst e1 x e_new) (expr_subst e2 x e_new)
|Downcast m e1 => Downcast m (expr_subst e1 x e_new)
| e => e
end.
*)
(* Lemma expr_subst_correct e e_sub E x v v_res defVars: *)
(* eval_expr E defVars (toREval (toRExp e_sub)) v REAL -> *)
(* eval_expr (updEnv x v E) defVars (toREval (toRExp e)) v_res REAL <-> *)
(* eval_expr E defVars (toREval (toRExp (expr_subst e x e_sub))) v_res REAL. *)
(* Proof. *)
(* intros eval_e. *)
(* revert v_res. *)
(* induction e. *)
(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(* + unfold updEnv in eval_upd. simpl in *. *)
(* inversion eval_upd; subst. *)
(* case_eq (n =? x); intros; try auto. *)
(* * rewrite H in H1. *)
(* inversion H1; subst; auto. *)
(* * rewrite H in H1. *)
(* eapply Var_load; eauto. *)
(* + simpl in eval_subst. *)
(* case_eq (n =? x); intros n_eq_case; *)
(* rewrite n_eq_case in eval_subst. *)
(* * simpl. *)
(* assert (updEnv x v E n = Some v_res). *)
(* { unfold updEnv; rewrite n_eq_case. *)
(* f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. } *)
(* { econstructor; eauto. *)
(* rewrite n_eq_case; auto. } *)
(* * simpl. inversion eval_subst; subst. *)
(* assert (E n = updEnv x v E n). *)
(* { unfold updEnv; rewrite n_eq_case; reflexivity. } *)
(* { rewrite H in H1. eapply Var_load; eauto. rewrite n_eq_case. auto. } *)
(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(* + inversion eval_upd; constructor; auto. *)
(* + inversion eval_subst; constructor; auto. *)
(* - split; [intros eval_upd | intros eval_subst]. *)
(* + inversion eval_upd; econstructor; auto; *)
(* rewrite <- IHe; auto. *)
(* + inversion eval_subst; constructor; try auto; *)
(* rewrite IHe; auto. *)
(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(* + inversion eval_upd; econstructor; auto; *)
(* destruct m1; destruct m2; inversion H2. *)
(* * rewrite <- IHe1; auto. *)
(* * rewrite <- IHe2; auto. *)
(* + inversion eval_subst; econstructor; auto; *)
(* destruct m1; destruct m2; inversion H2. *)
(* * rewrite IHe1; auto. *)
(* * rewrite IHe2; auto. *)
(* - split; [intros eval_upd | intros eval_subst]. *)
(* + rewrite <- IHe; auto. *)
(* + rewrite IHe; auto. *)
(* Qed. *)
(* Fixpoint map_subst (f:cmd Q) x e := *)
(* match f with *)
(* |Let m y e_y g => Let m y (expr_subst e_y x e) (map_subst g x e) *)
(* |Ret e_r => Ret (expr_subst e_r x e) *)
(* end. *)
(* Lemma stepwise_substitution x e v f E vR inVars outVars defVars: *)
(* ssa (toREvalCmd (toRCmd f)) inVars outVars -> *)
(* NatSet.In x inVars -> *)
(* NatSet.Subset (usedVars e) inVars -> *)
(* eval_expr E defVars (toREval (toRExp e)) v REAL -> *)
(* bstep (toREvalCmd (toRCmd f)) (updEnv x v E) (fun n => if (n =? x) then Some REAL else defVars n) vR REAL <-> *)
(* bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR REAL. *)
(* Proof. *)
(* revert E e x vR inVars outVars defVars. *)
(* induction f; intros E e0 x vR inVars outVars defVars ssa_f x_free valid_vars_e eval_e. *)
(* - split; [ intros bstep_let | intros bstep_subst]. *)
(* + inversion bstep_let; subst. *)
(* inversion ssa_f; subst. *)
(* assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var). *)
(* * eapply ssa_shadowing_free. *)
(* apply ssa_f. *)
(* apply x_free. *)
(* eauto. *)
(* * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H8; try eauto. *)
(* simpl in *. *)
(* econstructor; eauto. *)
(* { rewrite <- expr_subst_correct; eauto. } *)
(* { rewrite <- IHf; eauto. *)
(* admit. *)
(* rewrite NatSet.add_spec; right; auto. *)
(* apply validVars_add; auto. *)
(* eapply dummy_bind_ok; eauto. } *)
(* + inversion bstep_subst; subst. *)
(* simpl in *. *)
(* inversion ssa_f; subst. *)
(* econstructor; try auto. *)
(* rewrite expr_subst_correct; eauto. *)
(* rewrite <- IHf in H8; eauto. *)
(* * rewrite <- shadowing_free_rewriting_cmd in H8; eauto. *)
(* admit. *)
(* (* eapply ssa_shadowing_free; eauto. *) *)
(* (* rewrite <- expr_subst_correct in H7; eauto. *) *)
(* * rewrite NatSet.add_spec; auto. *)
(* * apply validVars_add; auto. *)
(* * eapply dummy_bind_ok; eauto. *)
(* - split; [intros bstep_let | intros bstep_subst]. *)
(* + inversion bstep_let; subst. *)
(* simpl in *. *)
(* rewrite expr_subst_correct in H0; eauto. *)
(* constructor. assumption. *)
(* + inversion bstep_subst; subst. *)
(* simpl in *. *)
(* rewrite <- expr_subst_correct in H0; eauto. *)
(* econstructor; eauto. *)
(* Abort. *)
(* Fixpoint let_subst (f:cmd Q) := *)
(* match f with *)
(* | Let m x e1 g => *)
(* expr_subst (let_subst g) x e1 *)
(* | Ret e1 => e1 *)
(* end. *)
(* Lemma eval_subst_subexpr E e' n e vR defVars: *)
(* NatSet.In n (usedVars e) -> *)
(* eval_expr E defVars (toREval (toRExp (expr_subst e n e'))) vR REAL -> *)
(* exists v, eval_expr E defVars (toREval (toRExp e')) v REAL. *)
(* Proof. *)
(* revert E e' n vR. *)
(* induction e; *)
(* intros E e' n' vR n_fVar eval_subst; simpl in *; try eauto. *)
(* - case_eq (n =? n'); intros case_n; rewrite case_n in *; eauto. *)
(* rewrite NatSet.singleton_spec in n_fVar. *)
(* exfalso. *)
(* rewrite Nat.eqb_neq in case_n. *)
(* apply case_n; auto. *)
(* - inversion n_fVar. *)
(* - inversion eval_subst; subst; *)
(* eapply IHe; eauto. *)
(* - inversion eval_subst; subst. *)
(* rewrite NatSet.union_spec in n_fVar. *)
(* destruct m1; destruct m2; inversion H2. *)
(* destruct n_fVar as [n_fVar_e1 | n_fVare2]; *)
(* [eapply IHe1; eauto | eapply IHe2; eauto]. *)
(* Qed. *)
(* Lemma bstep_subst_subexpr_any E e x f vR defVars: *)
(* NatSet.In x (liveVars f) -> *)
(* bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR REAL -> *)
(* exists E' v, eval_expr E' defVars (toREval (toRExp e)) v REAL. *)
(* Proof. *)
(* revert E e x vR defVars; *)
(* induction f; *)
(* intros E e' x vR defVars x_live eval_f. *)
(* - inversion eval_f; subst. *)
(* simpl in x_live. *)
(* rewrite NatSet.union_spec in x_live. *)
(* destruct x_live as [x_used | x_live]. *)
(* + exists E. eapply eval_subst_subexpr; eauto. *)
(* + eapply IHf; eauto. *)
(* Abort. *)
(* - simpl in *. *)
(* inversion eval_f; subst. *)
(* exists E. eapply eval_subst_subexpr; eauto. *)
(* Qed. *)
(* Lemma bstep_subst_subexpr_ret E e x e' vR defVars: *)
(* NatSet.In x (liveVars (Ret e')) -> *)
(* bstep (toREvalCmd (toRCmd (map_subst (Ret e') x e))) E defVars vR REAL -> *)
(* exists v, eval_expr E defVars (toREval (toRExp e)) v REAL. *)
(* Proof. *)
(* simpl; intros x_live bstep_ret. *)
(* inversion bstep_ret; subst. *)
(* eapply eval_subst_subexpr; eauto. *)
(* Qed. *)
(* Lemma no_forward_refs V (f:cmd V) inVars outVars: *)
(* ssa f inVars outVars -> *)
(* forall v, NatSet.In v (definedVars f) -> *)
(* NatSet.mem v inVars = false. *)
(* Proof. *)
(* intros ssa_f; induction ssa_f; simpl. *)
(* - intros v v_defVar. *)
(* rewrite NatSet.add_spec in v_defVar. *)
(* destruct v_defVar as [v_x | v_defVar]. *)
(* + subst; auto. *)
(* + specialize (IHssa_f v v_defVar). *)
(* case_eq (NatSet.mem v inVars); intros mem_inVars; try auto. *)
(* assert (NatSet.mem v (NatSet.add x inVars) = true) by (rewrite NatSet.mem_spec, NatSet.add_spec, <- NatSet.mem_spec; auto). *)
(* congruence. *)
(* - intros v v_in_empty; inversion v_in_empty. *)
(* Qed. *)
(* Lemma bstep_subst_subexpr_let E e x y e' g vR m defVars: *)
(* NatSet.In x (liveVars (Let m y e' g)) -> *)
(* (forall x, NatSet.In x (usedVars e) -> *)
(* exists v, E x = v) -> *)
(* bstep (toREvalCmd (toRCmd (map_subst (Let m y e' g) x e))) E defVars vR REAL -> *)
(* exists v, eval_expr E defVars (toREval (toRExp e)) v REAL. *)
(* Proof. *)
(* revert E e x y e' vR; *)
(* induction g; *)
(* intros E e0 x y e' vR x_live uedVars_def bstep_f. *)
(* - simpl in *. *)
(* inversion bstep_f; subst. *)
(* specialize (IHg (updEnv y m v E) e0 x n e). *)
(* rewrite NatSet.union_spec in x_live. *)
(* destruct x_live as [x_used | x_live]. *)
(* + eapply eval_subst_subexpr; eauto. *)
(* + edestruct IHg as [v0 eval_v0]; eauto. *)
(* Abort. *)
(* Theorem let_free_agree f E vR inVars outVars e defVars: *)
(* ssa f inVars outVars -> *)
(* (forall v, NatSet.In v (definedVars f) -> *)
(* NatSet.In v (liveVars f)) -> *)
(* let_subst f = e -> *)
(* bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR REAL -> *)
(* bstep (toREvalCmd (toRCmd f)) E defVars vR REAL. *)
(* Proof. *)
(* intros ssa_f. *)
(* revert E vR e; *)
(* induction ssa_f; *)
(* intros E vR e_subst dVars_live subst_step bstep_e; *)
(* simpl in *. *)
(* (* Let Case, prove that the value of the let binding must be used somewhere *) *)
(* - case_eq (let_subst s). *)
(* + intros e0 subst_s; rewrite subst_s in *. *)
(* Abort. *)
(* (*inversion subst_step; subst. *)
(* clear subst_s subst_step. *)
(* inversion bstep_e; subst. *)
(* specialize (dVars_live x). *)
(* rewrite NatSet.add_spec in dVars_live. *)
(* assert (NatSet.In x (NatSet.union (usedVars e) (liveVars s))) *)
(* as x_used_or_live *)
(* by (apply dVars_live; auto). *)
(* rewrite NatSet.union_spec in x_used_or_live. *)
(* destruct x_used_or_live as [x_used | x_live]. *)
(* * specialize (H x x_used). *)
(* rewrite <- NatSet.mem_spec in H; congruence. *)
(* * *)
(* eapply let_b. *)
(* Focus 2. *)
(* eapply IHssa_f; try auto. *) *)
(* Theorem let_free_form f E vR inVars outVars e defVars: *)
(* ssa f inVars outVars -> *)
(* bstep (toREvalCmd (toRCmd f)) E defVars vR REAL -> *)
(* let_subst f = e -> *)
(* bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR REAL. *)
(* Proof. *)
(* revert E vR inVars outVars e; *)
(* induction f; *)
(* intros E vR inVars outVars e_subst ssa_f bstep_f subst_step. *)
(* - simpl. *)
(* inversion bstep_f; subst. *)
(* inversion ssa_f; subst. *)
(* Abort. *)
(* (* case_eq (let_subst f). *)
(* + intros f_subst subst_f_eq. *)
(* specialize (IHf (updEnv n REAL v E) vR (NatSet.add n inVars) outVars f_subst H9 H7 subst_f_eq). *)
(* rewrite subst_f_eq in subst_step. *)
(* inversion IHf; subst. *)
(* constructor. *)
(* inversion subst_step. *)
(* subst. *)
(* rewrite <- expr_subst_correct; eauto. *)
(* + intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step. *)
(* - inversion bstep_f; subst. *)
(* constructor. *)
(* simpl in *. *)
(* inversion subst_step; subst. *)
(* assumption. *)
(* Qed. *)
(* *) *)
(* (* *)
(* Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env) *)
(* (ParamEnv:param_env) (P:precond) (eps:R): *)
(* ssa Q f inVars outVars -> *)
(* (forall v, NatSet.In v (freeVars e) -> *)
(* (Q2R (ivlo (P v)) <= ParamEnv v <= Q2R (ivhi (P v))))%R -> *)
(* (forall v, NatSet.In v inVars -> *)
(* exists r, VarEnv v = Some r) -> *)
(* exists vR, *)
(* bstep (toRCmd f) VarEnv ParamEnv P eps (Nop R) vR. *)
(* Proof. *)
(* intros ssa_f; revert VarEnv ParamEnv P eps. *)
(* induction ssa_f; *)
(* intros VarEnv ParamEnv P eps fVars_live. *)
(* - *)
(* *) *)
\ No newline at end of file
coq/ssaPrgs.v
View file @ 8b9d6c33
......@@ -462,398 +462,4 @@ Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_det_ignore_bind2; [eauto |].
edestruct ssa_inv_let; eauto.
Qed.
(*
Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
(forall n, E1 n = E2 n)->
eval_expr E1 defVars (toREval e) v REAL <->
eval_expr E2 defVars (toREval e) v REAL.
Proof.
revert v E1 E2.
induction e; intros v' E1 E2 agree_on_vars.
- split; intros eval_Var.
+ inversion eval_Var; subst.
rewrite agree_on_vars in H1.
constructor; auto.
+ inversion eval_Var; subst.
rewrite <- agree_on_vars in H1.
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.
+ erewrite IHe; eauto.
+ erewrite <- IHe; eauto.
+ erewrite <- IHe; eauto.
- split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto.
destruct m1; destruct m2; inversion H2.
try (erewrite IHe1; eauto);
try (erewrite IHe2; eauto); auto.
- split; intros eval_Downcast; simpl; simpl in eval_Downcast; erewrite IHe; eauto.
Qed.
Lemma shadowing_free_rewriting_cmd f E1 E2 vR defVars:
(forall n, E1 n = E2 n) ->
bstep (toREvalCmd f) E1 defVars vR REAL <->
bstep (toREvalCmd f) E2 defVars vR REAL.
Proof.
revert E1 E2 defVars vR.
induction f; intros E1 E2 vR agree_on_vars.
- split; intros bstep_Let; inversion bstep_Let; subst.
+ erewrite shadowing_free_rewriting_expr in H8; auto.
econstructor; eauto.
rewrite <- IHf.
apply H10.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
+ erewrite <- shadowing_free_rewriting_expr in H8; auto.
econstructor; eauto.
rewrite IHf.
apply H10.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
- split; intros bstep_Ret; inversion bstep_Ret; subst.
+ erewrite shadowing_free_rewriting_expr in H1; auto.
constructor; auto.
+ erewrite <- shadowing_free_rewriting_expr in H1; auto.
constructor; auto.
Qed.
Lemma dummy_bind_ok e v x v' inVars E defVars:
NatSet.Subset (usedVars e) inVars ->
NatSet.mem x inVars = false ->
eval_expr E defVars (toREval (toRExp e)) v REAL ->
eval_expr (updEnv x v' E) defVars (toREval (toRExp e)) v REAL.
Proof.
revert v x v' inVars E.
induction e; intros v1 x v2 inVars E valid_vars x_not_free eval_e.
- inversion eval_e; subst.
assert ((updEnv x v2 E) n = E n).
+ unfold updEnv.
case_eq (n =? x); try auto.
intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
subst; simpl in *.
hnf in valid_vars.
assert (NatSet.mem x (NatSet.singleton x) = true)
as in_singleton by (rewrite NatSet.mem_spec, NatSet.singleton_spec; auto).
rewrite NatSet.mem_spec in *.
specialize (valid_vars x in_singleton).
rewrite <- NatSet.mem_spec in valid_vars.
rewrite valid_vars in *; congruence.
+ econstructor; eauto.
rewrite H; auto.
- inversion eval_e; subst; constructor; auto.
- inversion eval_e; subst; econstructor; eauto.
- simpl in valid_vars.
inversion eval_e; subst; econstructor; eauto;
destruct m1; destruct m2; inversion H2;
subst.
+ eapply IHe1; eauto.
hnf; intros a in_e1.
apply valid_vars;
rewrite NatSet.union_spec; auto.
+ eapply IHe2; eauto.
hnf; intros a in_e2.
apply valid_vars;
rewrite NatSet.union_spec; auto.
- apply (IHe v1 x v2 inVars E); auto.
Qed.
Fixpoint expr_subst (e:expr Q) x e_new :=
match e with
|Var _ v => if v =? x then e_new else Var Q v
|Unop op e1 => Unop op (expr_subst e1 x e_new)
|Binop op e1 e2 => Binop op (expr_subst e1 x e_new) (expr_subst e2 x e_new)
|Downcast m e1 => Downcast m (expr_subst e1 x e_new)
| e => e
end.
*)
(* Lemma expr_subst_correct e e_sub E x v v_res defVars: *)
(* eval_expr E defVars (toREval (toRExp e_sub)) v REAL -> *)
(* eval_expr (updEnv x v E) defVars (toREval (toRExp e)) v_res REAL <-> *)
(* eval_expr E defVars (toREval (toRExp (expr_subst e x e_sub))) v_res REAL. *)
(* Proof. *)
(* intros eval_e. *)
(* revert v_res. *)
(* induction e. *)
(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(* + unfold updEnv in eval_upd. simpl in *. *)
(* inversion eval_upd; subst. *)
(* case_eq (n =? x); intros; try auto. *)
(* * rewrite H in H1. *)
(* inversion H1; subst; auto. *)
(* * rewrite H in H1. *)
(* eapply Var_load; eauto. *)
(* + simpl in eval_subst. *)
(* case_eq (n =? x); intros n_eq_case; *)
(* rewrite n_eq_case in eval_subst. *)
(* * simpl. *)
(* assert (updEnv x v E n = Some v_res). *)
(* { unfold updEnv; rewrite n_eq_case. *)
(* f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. } *)
(* { econstructor; eauto. *)
(* rewrite n_eq_case; auto. } *)
(* * simpl. inversion eval_subst; subst. *)