Commit dd226fbe authored by Nikita Zyuzin's avatar Nikita Zyuzin

Remove old deterministic semantics files

parent c7fc112c
(**
Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Export Flover.Commands.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
(**
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep_det DeltaMap: cmd R -> env -> (expr R -> option mType) -> R -> mType -> Prop :=
| let_b_det m m' x e s E v res defVars:
eval_expr_det E defVars DeltaMap e v m ->
bstep_det DeltaMap s (updEnv x v E) defVars res m' ->
bstep_det DeltaMap (Let m x e s) E defVars res m'
| ret_b_det m e E v defVars:
eval_expr_det E defVars DeltaMap e v m ->
bstep_det DeltaMap (Ret e) E defVars v m.
Lemma bstep_eq_env_det f DeltaMap:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
bstep_det DeltaMap f E1 Gamma v m ->
bstep_det DeltaMap f E2 Gamma v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env_det in H7; eauto. eapply let_b_det; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
+ auto.
- apply ret_b_det. eapply eval_eq_env_det; eauto.
Qed.
Lemma swap_Gamma_bstep_det f DeltaMap E vR m Gamma1 Gamma2 :
(forall n, Gamma1 n = Gamma2 n) ->
bstep_det DeltaMap f E Gamma1 vR m ->
bstep_det DeltaMap f E Gamma2 vR m.
Proof.
revert E Gamma1 Gamma2;
induction f; intros * Gamma_eq eval_f.
all: inversion eval_f; subst.
all: econstructor; try eauto.
all: eapply swap_Gamma_eval_expr_det; eauto.
Qed.
Lemma bstep_Gamma_det_det f DeltaMap:
forall E1 E2 Gamma v1 v2 m1 m2,
bstep_det DeltaMap f E1 Gamma v1 m1 ->
bstep_det DeltaMap f E2 Gamma v2 m2 ->
m1 = m2.
Proof.
induction f; intros * eval_f1 eval_f2;
inversion eval_f1; subst;
inversion eval_f2; subst; try auto.
- eapply IHf; eauto.
- eapply Gamma_det_det; eauto.
Qed.
Lemma bstep_det_functional f DeltaMap:
forall E Gamma v1 v2 m,
bstep_det DeltaMap f E Gamma v1 m ->
bstep_det DeltaMap f E Gamma v2 m ->
v1 = v2.
Proof.
induction f; intros * eval_f1 eval_f2;
inversion eval_f1; subst;
inversion eval_f2; subst; try auto.
- erewrite eval_expr_det_functional with (v1 := v) (v2 := v0) in *; eauto.
- eapply eval_expr_det_functional; eauto.
Qed.
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