From 86dab7438480b3506631088fa4426e4d6be2c36b Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Mon, 23 Dec 2024 01:13:55 -0500
Subject: [PATCH] Add outermost expansion and some related lemmas

---
 theories/diagram.txt |  7 +++++++
 theories/fp_red.v    | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+)

diff --git a/theories/diagram.txt b/theories/diagram.txt
index 2eaec80..2cf16e8 100644
--- a/theories/diagram.txt
+++ b/theories/diagram.txt
@@ -11,3 +11,10 @@ Abs a0 ----> (Abs a3) >>* a2
   |             |
   |             |
 Abs a1 ----> (Abs a4) >>*
+
+
+a0 >> a1
+|     |
+|     |
+v     v
+b0 >> b1
diff --git a/theories/fp_red.v b/theories/fp_red.v
index cf66d29..4d944e1 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -242,6 +242,45 @@ Module EPar.
 End EPar.
 
 
+Module OExp.
+  Inductive R {n} : Tm n -> Tm n ->  Prop :=
+  (****************** Eta ***********************)
+  | AppEta a :
+    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
+  | PairEta a :
+    R a (Pair (Proj PL a) (Proj PR a)).
+
+  Lemma merge n (t a b : Tm n) :
+    rtc R a b ->
+    EPar.R t a ->
+    EPar.R t b.
+  Proof.
+    move => h. move : t. elim : a b /h.
+    - eauto using EPar.refl.
+    - hauto q:on ctrs:EPar.R inv:R.
+  Qed.
+
+  Lemma commutativity n (a b c : Tm n) :
+    EPar.R a b -> R a c -> exists d, R b d /\ EPar.R c d.
+  Proof.
+    move => h.
+    inversion 1; subst.
+    - hauto q:on ctrs:EPar.R, R use:EPar.renaming, EPar.refl.
+    - hauto lq:on ctrs:EPar.R, R.
+  Qed.
+
+  Lemma commutativity0 n (a b c : Tm n) :
+    EPar.R a b -> rtc R a c -> exists d, rtc R b d /\ EPar.R c d.
+  Proof.
+    move => + h. move : b.
+    elim : a c / h.
+    - sfirstorder.
+    - hauto lq:on rew:off ctrs:rtc use:commutativity.
+  Qed.
+
+End OExp.
+
+
 Local Ltac com_helper :=
   split; [hauto lq:on ctrs:RPar.R use: RPar.refl, RPar.renaming
          |hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming].