Work on final naturality

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Elgot.lean

@@ -136,17 +136,18 @@ theorem Eqv.vwk1_fixpoint {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : r.fixpoint.vwk1 (inserted := inserted) = (r.vwk1).fixpoint := by
   simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_lift_fixpoint]
 
-theorem Eqv.lwk_lift_fixpoint {A B : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
-  {r : Eqv φ (⟨A, ⊥⟩::Δ) ((B.coprod A)::L)}
+theorem Eqv.lwk_lift_fixpoint {A B : Ty α} {L K : LCtx α}
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)}
   {ρ : L.InS K}
   : r.fixpoint.lwk ρ.slift = (r.lwk ρ.slift).fixpoint := by
   induction r using Quotient.inductionOn
-  --simp [InS.lwk_lift_fixpoint]
-  sorry
+  simp only [fixpoint_quot, lwk_quot]
+  rw [InS.lwk_lift_fixpoint]
 
 theorem Eqv.lwk1_fixpoint {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {r : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)}
-  : r.fixpoint.lwk1 (inserted := inserted) = (r.lwk1).fixpoint := sorry
+  : r.fixpoint.lwk1 (inserted := inserted) = (r.lwk1).fixpoint := by
+  rw [lwk1, <-LCtx.InS.slift_wk0, lwk_lift_fixpoint]; rfl
 
 theorem Eqv.vsubst_lift_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   {r : Eqv φ (⟨A, ⊥⟩::Δ) ((B.coprod A)::L)}

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean

@@ -579,7 +579,30 @@ theorem Eqv.assoc_mid_nat {A B C B' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 
 theorem Eqv.assoc_right_nat {A B C C' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (r : Eqv φ (⟨C, ⊥⟩::Γ) (C'::L))
-  : (A.prod B) ⋊ r ;; assoc = assoc ;; A ⋊ (B ⋊ r) := sorry
+  : (A.prod B) ⋊ r ;; assoc = assoc ;; A ⋊ (B ⋊ r) := by
+  rw [rtimes, let2_seq]
+  simp only [vwk1_assoc]
+  rw [seq_assoc, assoc_eq_ret, <-ret_of_seq, seq_prod_assoc, Term.Eqv.reassoc]
+  simp only [Term.Eqv.let2_pair, wk0_var, zero_add, let1_beta_pure, subst_let2, var_succ_subst0,
+    subst_pair, subst_liftn₂_var_one, ge_iff_le, le_refl, subst_liftn₂_var_zero,
+    subst_liftn₂_var_add_2, var0_subst0, List.length_cons, Nat.reduceAdd, Fin.zero_eta,
+    List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk_res_self]
+  rw [assoc, let2_seq]
+  simp only [vwk1_rtimes, let2_seq, ret_seq_rtimes, let2_pair, let1_beta]
+  simp only [wk0_pair, wk0_var, zero_add, Nat.reduceAdd]
+  rw [rtimes, let2_seq, seq_assoc, vwk1_ret, vwk1_ret, <-ret_of_seq]
+  simp only [Term.Eqv.seq, wk1_pair, wk1_var_succ, zero_add, wk1_var0, List.length_cons,
+    Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, Nat.reduceAdd,
+    let1_beta_pure, subst_pair, var_succ_subst0, var0_subst0, wk_res_self, vsubst_let2,
+    vsubst_liftn₂_seq, vsubst_br, subst_liftn₂_var_add_2, wk0_var, subst_liftn₂_var_one, ge_iff_le,
+    le_refl, subst_liftn₂_var_zero, let2_pair, let1_beta]
+  rw [br_zero_eq_ret, wk_res_self]
+  apply congrArg
+  rw [<-let2_ret]
+  sorry
+  -- calc
+  --   _ = let1 (var 1 Ctx.Var.shead.step) (r.vwk0.vwk1 ;; sorry) := sorry
+  --   _ = _ := sorry
 
 theorem Eqv.triangle {X Y : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : assoc (φ := φ) (Γ := Γ) (L := L) (A := X) (B := Ty.unit) (C := Y) ;; X ⋊ pi_r = pi_l ⋉ Y

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean

@@ -197,6 +197,14 @@ theorem Eqv.let2_seq {Γ : Ctx α ε} {L : LCtx α}
   : (Eqv.let2 a r) ;; s = Eqv.let2 a (r ;; s.vwk1.vwk1) := by
   simp only [seq_def, lsubst_let2, Subst.Eqv.vliftn₂_eq_vlift_vlift, vlift_alpha0]
 
+-- theorem Eqv.seq_let2_wk0_vwk2 {Γ : Ctx α ε} {L : LCtx α}
+--   (r : Eqv φ (⟨X, ⊥⟩::Γ) (Y::L))
+--   (a : Term.Eqv φ Γ ⟨A.prod B, ⊥⟩)
+--   (s : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (D::L))
+--   : (r ;; let2 a.wk0 s.vwk2) = let2 a.wk0
+--     (let1 (Term.Eqv.var 2 Ctx.Var.shead.step.step) (r.vwk1.vwk1.vwk1 ;; s.vwk2.vwk0)) := by
+--   sorry
+
 theorem Eqv.case_seq {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨X.coprod Y, e⟩)
   (r : Eqv φ (⟨X, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨Y, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L))

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -528,10 +528,20 @@ theorem vsubst_lift_fixpoint (r : Region φ) {ρ : Term.Subst φ}
   simp only [fixpoint, vsubst]
   congr
   funext i
-  cases i using Fin.elim1 with
-  | zero =>
-    rw [Fin.elim1_zero, vsubst_lift_append, vsubst_lwk1, vsubst_lift₂_vwk1]
-    rfl
+  cases i using Fin.elim1
+  rw [Fin.elim1_zero, vsubst_lift_append, vsubst_lwk1, vsubst_lift₂_vwk1]
+  rfl
+
+theorem lwk_lift_fixpoint (r : Region φ)
+  : r.fixpoint.lwk (Nat.liftWk ρ) = (r.lwk $ Nat.liftWk ρ).fixpoint := by
+  simp only [fixpoint, lwk]
+  congr
+  funext i; cases i using Fin.elim1
+  simp only [Nat.liftnWk_one, Fin.elim1_zero, lwk_lift_append]
+  congr 1
+  simp only [lwk1, lwk_lwk, vwk1_lwk]
+  congr
+  funext k; cases k <;> rfl
 
 def ite (b : Term φ) (r r' : Region φ) : Region φ := case b (r.vwk Nat.succ) (r'.vwk Nat.succ)
 

DeBruijnSSA/BinSyntax/Typing/Region/Compose.lean

@@ -371,6 +371,13 @@ def InS.cfgSubst {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
       (Wf.br ⟨ℓ.prop, by simp⟩ (Term.Wf.var Ctx.Var.shead))
       (λi => (G i).prop.vwk1)⟩
 
+theorem InS.lwk_lift_fixpoint {A B : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
+  {r : InS φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)}
+  {ρ : L.InS K}
+  : r.fixpoint.lwk ρ.slift = (r.lwk ρ.slift).fixpoint := by
+  ext
+  simp only [coe_lwk, coe_fixpoint, LCtx.InS.coe_slift, Region.lwk_lift_fixpoint]
+
 @[simp]
 theorem InS.coe_cfgSubst {Γ : Ctx α ε} {L : LCtx α} (R : LCtx α)
   (G : ∀i : Fin R.length, InS φ ((R.get i, ⊥)::Γ) (R ++ L))