From 4309a5c53aa0125a9d29fbdfc17f5c71ea07a46d Mon Sep 17 00:00:00 2001
From: Jad Ghalayini <jad.ghalayini@protonmail.com>
Date: Mon, 29 Jul 2024 19:43:34 +0100
Subject: [PATCH] Fixpoint naturality

---
 .../Rewrite/Region/Compose/Elgot.lean         | 79 ++++++++++++++++++-
 .../BinSyntax/Rewrite/Region/Compose/Seq.lean | 57 +++++++++++++
 .../BinSyntax/Rewrite/Region/Compose/Sum.lean | 42 ++++++++++
 DeBruijnSSA/BinSyntax/Typing/LCtx.lean        |  7 ++
 4 files changed, 184 insertions(+), 1 deletion(-)

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean
index d4ebbd3..2c121f2 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean
@@ -53,6 +53,25 @@ theorem Eqv.vwk2_left_exit {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   = left_exit
   := rfl
 
+theorem Eqv.left_exit_eq_coprod {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  : left_exit (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) =
+    coprod (br 1 (var 0 (by simp)) ⟨by simp, le_refl _⟩) (ret (var 0 (by simp)))
+  := rfl
+
+theorem Eqv.lwk1_sum_seq_left_exit {A B A' B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) (A'::L)} {g : Eqv φ (⟨B, ⊥⟩::Γ) (B'::L)}
+  : (sum f g).lwk1 ;; left_exit
+  = coprod (f.lwk1 ;; (br 1 (var 0 (by simp)) ⟨by simp, le_refl _⟩)) g.lwk1
+  := by rw [left_exit_eq_coprod, lwk1_sum, sum_seq_coprod, ret_var_zero, seq_nil]
+
+theorem Eqv.lwk1_sum_seq_left_exit' {A B A' B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) (A'::L)} {g : Eqv φ (⟨B, ⊥⟩::Γ) (B'::L)}
+  : (sum f g).lwk1 ;; left_exit
+  = case (Term.Eqv.var 0 Ctx.Var.shead)
+    (f.vwk1.lwk1 ;; (br 1 (var 0 (by simp)) ⟨by simp, le_refl _⟩))
+    g.vwk1.lwk1 := by
+  rw [lwk1_sum_seq_left_exit, coprod, vwk1_seq, vwk1_lwk1, vwk1_br, Term.Eqv.wk1_var0, vwk1_lwk1]
+
 def Eqv.fixpoint {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
   : Eqv φ (⟨A, ⊥⟩::Γ) (B::L) := cfg [A] nil (Fin.elim1 (f.vwk1.lwk1 ;; left_exit))
 
@@ -82,6 +101,23 @@ theorem Eqv.vsubst_lift_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   induction σ using Quotient.inductionOn
   simp [InS.vsubst_lift_fixpoint]
 
+theorem Eqv.lsubst_fixpoint_seq_helper {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)} {σ : Subst.Eqv φ (⟨A, ⊥⟩::Γ) (B::L) K}
+  : f.fixpoint.lsubst σ
+  = cfg [A] nil (Fin.elim1 ((f.vwk1.lwk1 ;; left_exit).lsubst σ.slift.vlift)) := by
+  rw [fixpoint, lsubst_cfg]
+  congr
+  · simp
+  · funext i
+    cases i using Fin.elim1
+    simp
+
+theorem Eqv.lsubst_fixpoint {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)} {σ : Subst.Eqv φ (⟨A, ⊥⟩::Γ) (B::L) K}
+  : f.fixpoint.lsubst σ
+  = cfg [A] nil (Fin.elim1 ((f.vwk1.lwk1.lsubst σ.slift.vlift ;; left_exit.lsubst σ.slift.vlift)))
+  := by rw [lsubst_fixpoint_seq_helper, lsubst_vlift_slift_seq]
+
 theorem Eqv.fixpoint_iter_cfg {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
   : fixpoint f = cfg [A] (f.lwk1 ;; left_exit) (Fin.elim1 (f.vwk1.lwk1 ;; left_exit)) := by
@@ -132,10 +168,51 @@ theorem Eqv.fixpoint_iter {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   | zero => simp only [
       Fin.elim1_zero, vwk1_seq, vwk1_left_exit, vwk2_seq, vwk2_left_exit, lwk1_vwk1, vwk1_vwk2]
 
+theorem Eqv.fixpoint_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
+  (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::L))
+  : (fixpoint f) ;; g = fixpoint (f ;; sum g nil) := by
+  rw [seq, lsubst_fixpoint, fixpoint]
+  apply congrArg
+  apply congrArg
+  rw [vwk1_seq, lwk1_seq, seq_assoc]
+  congr 1
+  · simp only [lwk1, <-lsubst_toSubst, lsubst_lsubst]
+    induction f using Quotient.inductionOn
+    induction g using Quotient.inductionOn
+    apply Eqv.eq_of_reg_eq
+    simp only [
+      InS.coe_lsubst, Subst.InS.coe_comp, Subst.InS.coe_vlift, Subst.InS.coe_slift, InS.coe_alpha0,
+      InS.coe_vwk, Ctx.InS.coe_wk1, LCtx.InS.coe_toSubst, LCtx.InS.coe_wk1
+    ]
+    congr
+    funext k
+    cases k <;> rfl
+  · rw [
+      vwk1_sum, lwk1_sum_seq_left_exit, coprod, vwk1_seq, nil_vwk1, nil_lwk1, nil_vwk1, vwk1_br,
+      wk1_var0, left_exit, lsubst_case
+    ]
+    induction g using Quotient.inductionOn
+    congr 1
+    apply Eqv.eq_of_reg_eq
+    simp only [InS.lsubst_br, InS.coe_vsubst, Term.InS.coe_subst0, Term.InS.coe_var, InS.coe_vwk_id,
+      Subst.InS.coe_get, Subst.InS.coe_vlift, Subst.InS.coe_slift, InS.coe_alpha0, InS.coe_vwk,
+      Ctx.InS.coe_wk1, InS.vwk_br, Term.InS.wk_var, Nat.liftWk_zero, InS.coe_lsubst, InS.coe_br,
+      InS.coe_lwk, LCtx.InS.coe_wk1, Region.vwk_lwk, Region.vwk_vwk, Region.Subst.vlift,
+      Region.Subst.lift, Function.comp_apply, Region.vwk1_lwk, Region.vsubst_lwk, Region.alpha,
+      Function.update_same]
+    simp only [<-Region.lsubst_fromLwk, Region.vwk1, Region.vwk_vwk, Region.lsubst_lsubst]
+    simp only [<-Region.vsubst_fromWk, Region.vsubst_vsubst]
+    congr
+    funext k
+    cases k <;> rfl
+    funext k
+    cases k <;> rfl
+
 theorem Eqv.fixpoint_naturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
   (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::L))
-  : fixpoint (f ;; sum g nil) = (fixpoint f) ;; g := sorry
+  : fixpoint (f ;; sum g nil) = (fixpoint f) ;; g := by rw [fixpoint_seq]
 
 theorem Eqv.fixpoint_dinaturality {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod C)::L))
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean
index 2bd2002..b3808fc 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean
@@ -73,6 +73,11 @@ theorem Eqv.nil_vwk1 {Γ : Ctx α ε} {L : LCtx α}
   : (Eqv.nil (φ := φ) (ty := ty) (rest := Γ) (targets := L)).vwk1 (inserted := inserted)
   = Eqv.nil := rfl
 
+@[simp]
+theorem Eqv.nil_lwk1 {Γ : Ctx α ε} {L : LCtx α}
+  : (Eqv.nil (φ := φ) (ty := ty) (rest := Γ) (targets := L)).lwk1 (inserted := inserted)
+  = Eqv.nil := rfl
+
 theorem Eqv.let1_0_nil
   : Eqv.let1 (Term.Eqv.var 0 ⟨by simp, le_refl _⟩) Eqv.nil
   = Eqv.nil (φ := φ) (ty := ty) (rest := rest) (targets := targets)
@@ -321,6 +326,21 @@ theorem Eqv.ret_of_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 
 theorem Eqv.ret_nil : ret Term.Eqv.nil = nil (φ := φ) (ty := A) (rest := Γ) (targets := L)  := rfl
 
+theorem Eqv.ret_var_zero {Γ : Ctx α ε} {L : LCtx α}
+  : ret (Term.Eqv.var 0 ⟨by simp, le_refl _⟩)
+  = nil (φ := φ) (ty := A) (rest := Γ) (targets := L) := rfl
+
+@[simp]
+theorem Eqv.ret_lsubst_slift
+   {σ : Subst.Eqv φ _ targets targets'} {a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩}
+  : (Eqv.ret a (targets := targets)).lsubst σ.slift = Eqv.ret a
+  := by induction a using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl
+
+@[simp]
+theorem Eqv.nil_lsubst_slift (σ : Subst.Eqv φ _ targets targets')
+  : (Eqv.nil (φ := φ) (ty := ty) (rest := rest) (targets := targets)).lsubst σ.slift = Eqv.nil
+  := by rw [<-ret_nil, ret_lsubst_slift]; rfl
+
 def Eqv.wseq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)
   := cfg [B] left.lwk1 (Fin.elim1 right.lwk0.vwk1)
@@ -458,6 +478,43 @@ theorem Eqv.wseq_eq_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : left.wseq right = left ;; right := by
   sorry
 
+theorem Eqv.lwk_lift_seq {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {ρ : LCtx.InS L K}
+  {left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)}
+  {right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (left ;; right).lwk (ρ.lift (le_refl _))
+  = (left.lwk (ρ.lift (le_refl _))) ;; (right.lwk (ρ.lift (le_refl _))) := by
+  simp only [<-wseq_eq_seq, lwk_lift_wseq]
+
+theorem Eqv.lwk_slift_seq {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {ρ : LCtx.InS L K}
+  {left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)}
+  {right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (left ;; right).lwk ρ.slift
+  = (left.lwk ρ.slift) ;; (right.lwk ρ.slift) := lwk_lift_seq
+
+theorem Eqv.lwk1_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)}
+  {right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (left ;; right).lwk1 (inserted := inserted) = left.lwk1 ;; right.lwk1 := by
+  simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_slift_seq]
+
+theorem Eqv.lsubst_vlift_slift_seq {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {σ : Subst.Eqv φ Γ L K}
+  {left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)}
+  {right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (left ;; right).lsubst σ.slift.vlift
+  = left.lsubst σ.slift.vlift ;; right.lsubst σ.slift.vlift
+  := sorry
+
+theorem Eqv.lsubst_slift_vlift_seq {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {σ : Subst.Eqv φ Γ L K}
+  {left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)}
+  {right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (left ;; right).lsubst σ.vlift.slift
+  = left.lsubst σ.vlift.slift ;; right.lsubst σ.vlift.slift
+  := sorry
+
 theorem Eqv.wrseq_assoc {B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (left : Eqv φ Γ (B::L)) (middle : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) (right : Eqv φ (⟨C, ⊥⟩::Γ) (D::L))
   : (left.wrseq middle).wrseq right = left.wrseq (middle ;; right) := by
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean
index 9df0401..aab0296 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean
@@ -15,6 +15,28 @@ def Eqv.coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) (C::L)
   := case (var 0 Ctx.Var.shead) l.vwk1 r.vwk1
 
+theorem Eqv.lwk_slift_coprod {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (l.coprod r).lwk ρ.slift = (l.lwk ρ.slift).coprod (r.lwk ρ.slift)
+  := by simp only [coprod, lwk_case, vwk1_lwk]
+
+theorem Eqv.lwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (l.coprod r).lwk1 (inserted := inserted) = (l.lwk1).coprod (r.lwk1)
+  := by simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_slift_coprod]
+
+theorem Eqv.vwk_slift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {ρ : Γ.InS Δ}
+  {l : Eqv φ (⟨A, ⊥⟩::Δ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Δ) (C::L)}
+  : (l.coprod r).vwk ρ.slift = (l.vwk ρ.slift).coprod (r.vwk ρ.slift) := by
+  simp only [coprod, vwk_case, vwk1, vwk_vwk]
+  congr 2 <;> ext k <;> cases k <;> rfl
+
+theorem Eqv.vwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+  : (l.coprod r).vwk1 (inserted := inserted) = l.vwk1.coprod r.vwk1 := by
+  simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_coprod]
+
 theorem Eqv.Pure.coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} (hl : l.Pure)
   {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)} (hr : r.Pure)
@@ -78,6 +100,26 @@ def Eqv.sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) ((C.coprod D)::L)
   := coprod (l ;; inj_l) (r ;; inj_r)
 
+theorem Eqv.lwk_slift_sum {A B C D : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)}
+  : (l.sum r).lwk ρ.slift = (l.lwk ρ.slift).sum (r.lwk ρ.slift)
+  := by simp only [sum, lwk_slift_coprod, lwk_slift_seq]; rfl
+
+theorem Eqv.lwk1_sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)}
+  : (l.sum r).lwk1 (inserted := inserted) = (l.lwk1).sum (r.lwk1)
+  := by simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_slift_sum]
+
+theorem Eqv.vwk_slift_sum {A B C D : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {ρ : Γ.InS Δ} {l : Eqv φ (⟨A, ⊥⟩::Δ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Δ) (D::L)}
+  : (l.sum r).vwk ρ.slift = (l.vwk ρ.slift).sum (r.vwk ρ.slift)
+  := by simp only [sum, vwk_slift_coprod, vwk_lift_seq]; rfl
+
+theorem Eqv.vwk1_sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)}
+  : (l.sum r).vwk1 (inserted := inserted) = l.vwk1.sum r.vwk1
+  := by simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_sum]
+
 theorem Eqv.Pure.sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} (hl : l.Pure)
   {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)} (hr : r.Pure)
diff --git a/DeBruijnSSA/BinSyntax/Typing/LCtx.lean b/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
index 208c239..e20e296 100644
--- a/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
@@ -52,6 +52,9 @@ def InS (L K : LCtx α) : Type _ := {ρ : ℕ → ℕ | L.Wkn K ρ}
 instance inSCoe : CoeOut (InS L K) (ℕ → ℕ)
   := ⟨λt => t.val⟩
 
+@[ext]
+theorem InS.ext (ρ σ : InS L K) (h : ∀n, ρ.val n = σ.val n) : ρ = σ := Subtype.eq $ funext h
+
 instance InS.instSetoid : Setoid (InS L K) where
   r ρ σ := ∀i, i < L.length → (ρ : ℕ → ℕ) i = (σ : ℕ → ℕ) i
   iseqv := {
@@ -146,6 +149,10 @@ def InS.wk1 {head inserted : Ty α} {L : LCtx α} : InS (head::L) (head::inserte
 theorem InS.coe_wk1 {head inserted : Ty α} {L : LCtx α}
   : (InS.wk1 (head := head) (inserted := inserted) (L := L) : ℕ → ℕ) = Nat.liftWk Nat.succ := rfl
 
+theorem InS.slift_wk0 {head : Ty α} {L : LCtx α}
+  : (InS.wk0 (head := inserted) (L := L)).slift (head := head) = InS.wk1
+  := rfl
+
 def InS.comp {L K J : LCtx α} (ρ : InS K J) (σ : InS L K) : InS L J
   := ⟨(ρ : ℕ → ℕ) ∘ (σ : ℕ → ℕ), ρ.2.comp σ.2⟩