blob: 31724c05bc5549a1bea00f231f8ceca5085f7aa2 (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
From mininix Require Export evallang.operational.
From stdpp Require Import options.
Module Import evallang.
Export evallang.
(** Properties of operational semantics *)
Lemma step_not_final e1 e2 : e1 --> e2 → ¬final e1.
Proof. induction 1; simpl; repeat case_match; naive_solver. Qed.
Lemma final_nf e : final e → nf step e.
Proof. by intros ? [??%step_not_final]. Qed.
Lemma SAbsL_rtc ex1 ex1' e : ex1 -->* ex1' → EAbs ex1 e -->* EAbs ex1' e.
Proof. induction 1; econstructor; eauto using step. Qed.
Lemma SAppL_rtc e1 e1' e2 : e1 -->* e1' → EApp e1 e2 -->* EApp e1' e2.
Proof. induction 1; econstructor; eauto using step. Qed.
Lemma SEval_rtc ds e1 e1' : e1 -->* e1' → EEval ds e1 -->* EEval ds e1'.
Proof. induction 1; econstructor; eauto using step. Qed.
Ltac inv_step := repeat
match goal with H : ?e --> _ |- _ => assert_fails (is_var e); inv H end.
Lemma step_det e d1 d2 :
e --> d1 →
e --> d2 →
d1 = d2.
Proof.
intros Hred1. revert d2.
induction Hred1; intros d2 Hred2; inv Hred2; try by inv_step;
f_equal; by apply IHHred1.
Qed.
End evallang.
|
