From 00f581bcc7f45516f0f1345122577491120cfc15 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Tue, 8 Apr 2025 01:04:18 -0400
Subject: [PATCH] Work on diamond

---
 theories/confluence.v | 179 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 179 insertions(+)
 create mode 100644 theories/confluence.v

diff --git a/theories/confluence.v b/theories/confluence.v
new file mode 100644
index 0000000..4fabdb6
--- /dev/null
+++ b/theories/confluence.v
@@ -0,0 +1,179 @@
+From Ltac2 Require Ltac2.
+Import Ltac2.Notations.
+
+Import Ltac2.Control.
+Require Import ssreflect ssrbool.
+Require Import FunInd.
+Require Import Psatz.
+From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn).
+From Hammer Require Import Tactics.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax.
+
+Module βηPar.
+  Inductive R : Tm -> Tm -> Prop :=
+  | VarCong i :
+    R (VarTm i) (VarTm i)
+  | AppCong b0 b1 a0 a1 :
+    R b0 b1 ->
+    R a0 a1 ->
+    R (App b0 a0) (App b1 a1)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (Abs a0) (Abs a1)
+  | AppAbs b0 b1 a0 a1 :
+    R b0 b1 ->
+    R a0 a1 ->
+    R (App (Abs b0) a0) (subst_Tm (scons a1 VarTm) b1)
+  | AbsEta b0 b1 :
+    R b0 b1 ->
+    R b0 (Abs (App (ren_Tm shift b1) (VarTm var_zero))).
+
+  #[export]Hint Constructors R : βηPar.
+
+  Derive Inversion inv with (forall a b, R a b).
+
+  Lemma AppAbs' b0 b1 a0 a1 u :
+    u = (subst_Tm (scons a1 VarTm) b1) ->
+    R b0 b1 ->
+    R a0 a1 ->
+    R (App (Abs b0) a0) u.
+  Proof. move => ->. apply AppAbs. Qed.
+
+  Lemma AbsEta' b0 b1 u :
+    u = (Abs (App (ren_Tm shift b1) (VarTm var_zero))) ->
+    R b0 b1 ->
+    R b0 u.
+  Proof. move => ->. apply AbsEta. Qed.
+
+  Lemma refl a : R a a.
+  Proof. elim : a => //=; eauto with βηPar. Qed.
+
+  Lemma morphing a b ρ :
+    R a b ->
+    R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof.
+    move => h. move : ρ. elim : a b /h => /=; eauto with βηPar.
+    - eauto using refl.
+    - move => *; apply : AppAbs'; eauto. by asimpl.
+    - move => *; apply : AbsEta'; eauto. by asimpl.
+  Qed.
+
+  Lemma renaming a b ξ :
+    R a b ->
+    R (ren_Tm ξ a) (ren_Tm ξ b).
+  Proof. substify. apply morphing. Qed.
+
+  Definition morphing2_ok ρ0 ρ1 := forall (i : nat), R (ρ0 i) (ρ1 i).
+
+  Lemma morphing2_ren (ξ : nat -> nat) ρ0 ρ1 :
+    morphing2_ok ρ0 ρ1 ->
+    morphing2_ok (funcomp (ren_Tm ξ) ρ0) (funcomp (ren_Tm ξ) ρ1).
+  Proof. rewrite /morphing2_ok; eauto using renaming. Qed.
+
+  Lemma morphing2_ext a b ρ0 ρ1 :
+    R a b ->
+    morphing2_ok ρ0 ρ1 ->
+    morphing2_ok (scons a ρ0) (scons b ρ1).
+  Proof.
+    move => * [|i] //=.
+  Qed.
+
+  Lemma morphing_up ρ0 ρ1 :
+    morphing2_ok ρ0 ρ1 ->
+    morphing2_ok (up_Tm_Tm ρ0) (up_Tm_Tm ρ1).
+  Proof.
+    move => h.
+    apply morphing2_ext. apply VarCong.
+    by apply morphing2_ren.
+  Qed.
+
+  Lemma morphing2 a b ρ0 ρ1 :
+    R a b ->
+    morphing2_ok ρ0 ρ1 ->
+    R (subst_Tm ρ0 a) (subst_Tm ρ1 b).
+  Proof.
+    move => h. move : ρ0 ρ1.
+    elim : a b /h => //=; eauto using morphing_up with βηPar.
+    - move => * /=.
+      apply : AppAbs'; eauto using morphing_up. by asimpl.
+    - move => * /=.
+      apply : AbsEta'; eauto using morphing_up. by asimpl.
+  Qed.
+
+End βηPar.
+
+Module IPar.
+  Inductive R : Tm -> Tm -> Prop :=
+  | VarCong i :
+    R (VarTm i) (VarTm i)
+  | AppCong b0 b1 a0 a1 :
+    βηPar.R b0 b1 ->
+    βηPar.R a0 a1 ->
+    R (App b0 a0) (App b1 a1)
+  | AbsCong a0 a1 :
+    βηPar.R a0 a1 ->
+    R (Abs a0) (Abs a1)
+  | AppAbs b0 b1 a0 a1 :
+    βηPar.R b0 b1 ->
+    βηPar.R a0 a1 ->
+    R (App (Abs b0) a0) (subst_Tm (scons a1 VarTm) b1).
+  Derive Inversion inv with (forall a b, R a b).
+End IPar.
+
+Module OExp.
+  Inductive R : Tm -> Tm -> Prop :=
+  | AbsEta b :
+    R b (Abs (App (ren_Tm shift b) (VarTm var_zero))).
+
+End OExp.
+
+Lemma IO_factorization a c :
+  βηPar.R a c -> exists b, IPar.R a b /\ rtc OExp.R b c.
+Proof.
+  move => h. elim : a c /h.
+  - move => i. exists (VarTm i).
+    split. constructor.
+    apply rtc_refl.
+  - move => b0 b1 a0 a1 hb [b' [ihb0 ihb1]] ha [a' [iha0 iha1]].
+    exists (App b1 a1).
+    split. apply IPar.AppCong; eauto.
+    apply rtc_refl.
+  - move => a0 a1 ha [a' [iha0 iha1]].
+    exists (Abs a1). split. by apply IPar.AbsCong.
+    apply rtc_refl.
+  - move => b0 b1 a0 a1 hb [b' [ihb0 ihb1]] ha [a' [iha0 iha1]].
+    eexists. split. apply IPar.AppAbs; eauto.
+    apply rtc_refl.
+  - move => b0 b1 hb [b' [ihb0 ihb1]].
+    exists b'. split => //.
+    apply : rtc_r; eauto.
+    constructor.
+Qed.
+
+Lemma IO_merge a b c :
+  βηPar.R a b -> OExp.R b c -> βηPar.R a c.
+Proof. hauto lq:on inv:OExp.R ctrs:βηPar.R. Qed.
+
+Lemma IO_merge' a b c :
+  βηPar.R a b -> rtc OExp.R b c -> βηPar.R a c.
+Proof. induction 2; hauto l:on use:IO_merge. Qed.
+
+Lemma diamond a b0 b1 :
+  βηPar.R a b0 -> βηPar.R a b1 -> exists c, βηPar.R b0 c /\ βηPar.R b1 c.
+Proof.
+  move => h. move : b1.
+  elim : a b0 / h.
+  - move => i b1 /IO_factorization.
+    move => [b [h0 h1]].
+    inversion h0; subst. exists b1.
+    split => //=.
+    apply : IO_merge'; eauto.
+    constructor.
+    apply βηPar.refl.
+  - move => b0 b1 a0 a1 hb ihb ha iha b2 /IO_factorization.
+    move => [u [h0 h1]].
+    elim /IPar.inv : h0=>//_.
+    + move => b3 b4 a2 a3 hb' ha' [*]. subst.
+      have {}/ihb [b14 [ihb0 ihb1]] := hb'.
+      have {}/iha [a13 [iha0 iha1]] := ha'.
+      exists (App b14 a13). split. by constructor.