From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 theories/dynlang/operational_props.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 theories/dynlang/operational_props.v

(limited to 'theories/dynlang/operational_props.v')

diff --git a/theories/dynlang/operational_props.v b/theories/dynlang/operational_props.v
new file mode 100644
index 0000000..9e8028c
--- /dev/null
+++ b/theories/dynlang/operational_props.v
@@ -0,0 +1,33 @@
+From mininix Require Export dynlang.operational.
+From stdpp Require Import options.
+
+Module Import dynlang.
+Export dynlang.
+
+(** 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 SId_rtc ds e1 e1' : e1 -->* e1' → EId ds e1 -->* EId 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 dynlang.
-- 
cgit v1.2.3