parent
72267ebe23
commit
adaf2a7e81
@ -0,0 +1,177 @@
|
||||
From stdpp Require Import base relations tactics.
|
||||
From iris Require Import prelude.
|
||||
From semantics.lib Require Import sets maps.
|
||||
From semantics.ts.stlc Require Import lang notation.
|
||||
|
||||
Fixpoint eval_step (e: expr): option expr :=
|
||||
match e with
|
||||
| Var _ => None
|
||||
| Lam x body => None
|
||||
| LitInt n => None
|
||||
| App lhs rhs => match to_val rhs, to_val lhs with
|
||||
| None, _ => fmap (λ (rhs': expr), App lhs rhs') (eval_step rhs)
|
||||
| Some _, None => fmap (λ (lhs': expr), App lhs' rhs) (eval_step lhs)
|
||||
| Some rhs', Some (LamV name body) => Some (subst' name rhs' body)
|
||||
| _, _ => None
|
||||
end
|
||||
| Plus lhs rhs => match to_val rhs, to_val lhs with
|
||||
| None, _ => fmap (λ (rhs': expr), Plus lhs rhs') (eval_step rhs)
|
||||
| Some _, None => fmap (λ (lhs': expr), Plus lhs' rhs) (eval_step lhs)
|
||||
| Some (LitIntV rhs'), Some (LitIntV lhs') => Some (LitInt (lhs' + rhs'))
|
||||
| _, _ => None
|
||||
end
|
||||
end.
|
||||
|
||||
Theorem step_eval_step (e e': expr): step e e' → eval_step e = Some e'.
|
||||
Proof.
|
||||
intro H_step.
|
||||
induction H_step; unfold eval_step; fold eval_step.
|
||||
- unfold to_val.
|
||||
destruct e'; try (unfold is_val in H; exfalso; exact H).
|
||||
reflexivity.
|
||||
reflexivity.
|
||||
- destruct e1; try (unfold eval_step in IHH_step; discriminate IHH_step).
|
||||
+ unfold to_val.
|
||||
destruct e2; try (unfold is_val in H; exfalso; exact H).
|
||||
all: rewrite IHH_step; reflexivity.
|
||||
+ unfold to_val.
|
||||
destruct e2; try (unfold is_val in H; exfalso; exact H).
|
||||
all: rewrite IHH_step; reflexivity.
|
||||
- destruct (to_val e2) eqn:H_to_val.
|
||||
{
|
||||
apply of_to_val in H_to_val.
|
||||
assert (is_val (of_val v)); try exact (is_val_of_val v).
|
||||
apply val_no_step in H_step.
|
||||
exfalso; exact H_step.
|
||||
rewrite <-H_to_val.
|
||||
assumption.
|
||||
}
|
||||
rewrite IHH_step.
|
||||
reflexivity.
|
||||
- unfold to_val.
|
||||
rewrite H.
|
||||
reflexivity.
|
||||
- destruct e2; try (unfold is_val in H; exfalso; exact H).
|
||||
unfold to_val.
|
||||
|
||||
destruct H_step; try (rewrite IHH_step; reflexivity).
|
||||
unfold to_val.
|
||||
rewrite IHH_step; simpl.
|
||||
destruct e1.
|
||||
+ inversion H_step.
|
||||
+ val_no_step.
|
||||
+ reflexivity.
|
||||
+ val_no_step.
|
||||
+ reflexivity.
|
||||
- destruct (to_val e2) eqn:H_to_val.
|
||||
{
|
||||
apply of_to_val in H_to_val.
|
||||
assert (is_val (of_val v)); try exact (is_val_of_val v).
|
||||
apply val_no_step in H_step.
|
||||
exfalso; exact H_step.
|
||||
rewrite <-H_to_val.
|
||||
assumption.
|
||||
}
|
||||
rewrite IHH_step.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem eval_step_step (e e': expr): eval_step e = Some e' → step e e'.
|
||||
Proof.
|
||||
revert e'.
|
||||
induction e; intros e' H_eq.
|
||||
all: try (unfold eval_step in H_eq; discriminate H_eq).
|
||||
- unfold eval_step in H_eq; fold eval_step in H_eq.
|
||||
|
||||
induction (eval_step e2).
|
||||
+ remember (IHe2 a (eq_refl _)) as H_appr.
|
||||
unfold eval_step in H_eq; fold eval_step in H_eq.
|
||||
destruct (to_val e2) eqn:H_to_val.
|
||||
clear HeqH_appr.
|
||||
{
|
||||
apply of_to_val in H_to_val.
|
||||
assert (is_val (of_val v)); try exact (is_val_of_val v).
|
||||
apply val_no_step in H_appr.
|
||||
exfalso; exact H_appr.
|
||||
rewrite <-H_to_val.
|
||||
assumption.
|
||||
}
|
||||
simpl in H_eq.
|
||||
injection H_eq; intro H_eq'.
|
||||
rewrite <-H_eq'.
|
||||
apply StepAppR.
|
||||
assumption.
|
||||
+ destruct (to_val e2) eqn:H_e2_to_val.
|
||||
all: destruct (to_val e1) eqn:H_e1_to_val.
|
||||
all: try (simpl in H_eq; discriminate H_eq).
|
||||
all: try remember (of_to_val _ _ H_e1_to_val) as H_e1_val.
|
||||
all: try remember (of_to_val _ _ H_e2_to_val) as H_e2_val.
|
||||
{
|
||||
subst.
|
||||
induction v0.
|
||||
discriminate H_eq.
|
||||
injection H_eq; intro H_eq'; subst.
|
||||
apply StepBeta.
|
||||
eauto.
|
||||
}
|
||||
induction (eval_step e1).
|
||||
{
|
||||
simpl in H_eq.
|
||||
injection H_eq; intro H_eq'.
|
||||
rewrite <-H_eq'.
|
||||
eapply StepAppL.
|
||||
rewrite <-H_e2_val.
|
||||
apply is_val_of_val.
|
||||
apply (IHe1 a (eq_refl _)).
|
||||
}
|
||||
simpl in H_eq; discriminate H_eq.
|
||||
- unfold eval_step in H_eq; fold eval_step in H_eq.
|
||||
destruct (to_val e2) eqn:H_e2_to_val.
|
||||
all: destruct (to_val e1) eqn:H_e1_to_val.
|
||||
all: try remember (of_to_val _ _ H_e1_to_val) as H_e1_val.
|
||||
all: try remember (of_to_val _ _ H_e2_to_val) as H_e2_val.
|
||||
+ induction v; induction v0; try discriminate H_eq.
|
||||
rewrite <-H_e2_val.
|
||||
rewrite <-H_e1_val.
|
||||
unfold of_val.
|
||||
injection H_eq; intro H_eq'.
|
||||
rewrite <-H_eq'.
|
||||
eauto.
|
||||
+ induction v; try discriminate H_eq.
|
||||
all: (
|
||||
unfold of_val in H_e2_val;
|
||||
rewrite <-H_e2_val;
|
||||
induction (eval_step e1); try (simpl in H_eq; discriminate H_eq);
|
||||
simpl in H_eq;
|
||||
injection H_eq; intro H_eq';
|
||||
subst;
|
||||
eapply StepPlusL;
|
||||
unfold is_val; intuition;
|
||||
exact (IHe1 a (eq_refl _))
|
||||
).
|
||||
+ induction (eval_step e2); try (simpl in H_eq; discriminate H_eq).
|
||||
simpl in H_eq; injection H_eq; intro H_eq'.
|
||||
subst.
|
||||
eapply StepPlusR.
|
||||
exact (IHe2 a (eq_refl _)).
|
||||
+ induction (eval_step e2); try (simpl in H_eq; discriminate H_eq).
|
||||
simpl in H_eq; injection H_eq; intro H_eq'.
|
||||
subst.
|
||||
eapply StepPlusR.
|
||||
exact (IHe2 a (eq_refl _)).
|
||||
Qed.
|
||||
|
||||
|
||||
Ltac auto_subst :=
|
||||
(rewrite subst_closed_nil; last assumption) ||
|
||||
(unfold subst'; unfold subst; simpl; fold subst).
|
||||
|
||||
Ltac auto_step := (simpl;
|
||||
repeat (eapply rtc_l;
|
||||
first apply eval_step_step;
|
||||
first simpl;
|
||||
first reflexivity;
|
||||
try (reflexivity; done)
|
||||
);
|
||||
reflexivity
|
||||
).
|
||||
Loading…
Reference in new issue