pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

OperationalSemantics: automated equivalence of big and small

Browse source
This commit is contained in:
Adam Chlipala 2016-02-21 13:23:09 -05:00
parent 918fcaa29b
commit f67d9b5e32
1 changed files with 49 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
OperationalSemantics.v
View file

@ -448,3 +448,52 @@ Proof.
eassumption.
constructor.
Qed.
(* Bonus material: here's how to make these proofs much more automatic. We
* won't explain the features being used here. *)
Hint Constructors trc step eval.
Lemma step_star_Seq_snazzy : forall v c1 c2 v' c1',
step^* (v, c1) (v', c1')
-> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).
Proof.
induct 1; eauto.
cases y; eauto.
Qed.
Hint Resolve step_star_Seq_snazzy.
Theorem big_small_snazzy : forall v c v', eval v c v'
-> step^* (v, c) (v', Skip).
Proof.
induct 1; eauto 6 using trc_trans.
Qed.
Lemma small_big''_snazzy : forall v c v' c', step (v, c) (v', c')
-> forall v'', eval v' c' v''
-> eval v c v''.
Proof.
induct 1; simplify;
repeat match goal with
| [ H : eval _ _ _ |- _ ] => invert1 H
end; eauto.
Qed.
Hint Resolve small_big''_snazzy.
Lemma small_big'_snazzy : forall v c v' c', step^* (v, c) (v', c')
-> forall v'', eval v' c' v''
-> eval v c v''.
Proof.
induct 1; eauto.
cases y; eauto.
Qed.
Hint Resolve small_big'_snazzy.
Theorem small_big_snazzy : forall v c v', step^* (v, c) (v', Skip)
-> eval v c v'.
Proof.
eauto.
Qed.