Commit ea902e6d authored by Heiko Becker's avatar Heiko Becker

Finish proving correctness of new type computation

parent 36a22bbb
......@@ -51,7 +51,7 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_expr E defVars e v m ->
bstep s (updEnv x v E) (updDefVars (Var R x) m defVars) res m' ->
bstep s (updEnv x v E) defVars res m' -> (* (updDefVars (Var R x) m defVars) res m' -> *)
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_expr E defVars e v m ->
......@@ -100,4 +100,19 @@ Proof.
destruct (x=? n); auto.
+ auto.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
\ No newline at end of file
Qed.
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
(forall n, Gamma1 n = Gamma2 n) ->
bstep f E Gamma1 vR m ->
bstep f E Gamma2 vR m.
Proof.
revert E Gamma1 Gamma2;
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
- inversion eval_f; subst.
econstructor; try eauto.
eapply swap_Gamma_eval_expr; eauto.
Qed.
......@@ -333,6 +333,24 @@ Proof.
set_tac. *)
Admitted.
Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2:
(forall n, Gamma1 n = Gamma2 n) ->
eval_expr E Gamma1 e vR m ->
eval_expr E Gamma2 e vR m.
Proof.
revert E vR Gamma1 Gamma2 m;
induction e; intros * Gamma_eq eval_e;
inversion eval_e; subst; simpl in *;
[ eapply Var_load
| eapply Const_dist'
| eapply Unop_neg'
| eapply Unop_inv'
| eapply Binop_dist'
| eapply Fma_dist'
| eapply Downcast_dist' ]; try eauto;
rewrite <- Gamma_eq; auto.
Qed.
Lemma Rmap_updVars_comm Gamma n m:
forall x,
updDefVars n REAL (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
......
......@@ -60,38 +60,6 @@ Proof.
destruct e; intros [_ valid_e]; simpl in *; try auto.
Qed.
(* Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2: *)
(* (forall n, Gamma1 n = Gamma2 n) -> *)
(* eval_expr E Gamma1 e vR m -> *)
(* eval_expr E Gamma2 e vR m. *)
(* Proof. *)
(* revert E vR Gamma1 Gamma2 m; *)
(* induction e; intros * Gamma_eq eval_e; *)
(* inversion eval_e; subst; simpl in *; *)
(* try eauto. *)
(* apply Var_load; try auto. *)
(* rewrite <- Gamma_eq; auto. *)
(* Qed. *)
(* Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 fBits : *)
(* (forall n, Gamma1 n = Gamma2 n) -> *)
(* bstep f E Gamma1 fBits vR m -> *)
(* bstep f E Gamma2 fBits vR m. *)
(* Proof. *)
(* revert E Gamma1 Gamma2; *)
(* induction f; intros * Gamma_eq eval_f. *)
(* - inversion eval_f; subst. *)
(* econstructor; try eauto. *)
(* + eapply swap_Gamma_eval_expr; eauto. *)
(* + apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto. *)
(* intros n1. *)
(* unfold updDefVars. *)
(* case (n1 =? n); auto. *)
(* - inversion eval_f; subst. *)
(* econstructor; try eauto. *)
(* eapply swap_Gamma_eval_expr; eauto. *)
(* Qed. *)
(* Lemma validRanges_swap Gamma1 Gamma2: *)
(* forall e A E fBits, *)
(* (forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) -> *)
......
This diff is collapsed.
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