Reduction to sequence lore

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

@@ -598,11 +598,23 @@ theorem Eqv.assoc_right_nat {A B C C' : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     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
+  rw [<-let2_ret, seq_let2_wk0_pure' (a' := var 0 Ctx.Var.shead) (ha := by rfl)]
+  apply congrArg
+  induction r using Quotient.inductionOn
+  apply Eqv.eq_of_reg_eq
+  simp only [Set.mem_setOf_eq, InS.vwk_br, Term.InS.wk_pair, Term.InS.wk_var, Ctx.InS.coe_swap02,
+    Nat.ofNat_pos, Nat.swap0_lt, Nat.swap0_0, Nat.one_lt_ofNat, Ctx.InS.coe_wk1, Nat.liftWk_succ,
+    Nat.succ_eq_add_one, Nat.reduceAdd, zero_add, Nat.liftWk_zero, InS.coe_vwk, InS.coe_lsubst,
+    InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair, Term.InS.coe_var, vwk_lsubst, InS.coe_vsubst,
+    Term.InS.coe_subst0, Term.Subst.InS.coe_liftn₂, Region.vsubst_lsubst]
+  congr
+  · funext k; cases k with
+    | zero => simp
+    | succ => rfl
+  · simp only [Region.vwk_vwk]
+    simp only [Region.vsubst_vsubst, <-Region.vsubst_fromWk]
+    congr
+    funext k; cases k <;> rfl
 
 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,13 +197,94 @@ 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.seq_let1_wk0_pure {Γ : Ctx α ε} {L : LCtx α}
+  (a : Term.Eqv φ Γ ⟨X, ⊥⟩)
+  (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L))
+  : r ;; (let1 a.wk0 s) = let1 a.wk0 (r.vwk1 ;; s.vswap01).vswap01 := by
+  simp only [seq_def, let1_beta]
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  induction s using Quotient.inductionOn
+  apply Eqv.eq_of_reg_eq
+  simp only [Set.mem_setOf_eq, InS.coe_lsubst, InS.coe_alpha0, InS.coe_vwk, Ctx.InS.coe_wk1,
+    InS.coe_vsubst, Term.InS.coe_subst0, Term.InS.coe_wk, Ctx.InS.coe_wk0, Ctx.InS.coe_swap01,
+    vwk_lsubst, Region.vsubst_lsubst]
+  congr
+  · funext k; cases k with
+    | zero =>
+      simp only [alpha, Function.update_same, Region.vwk_vwk, Function.comp_apply]
+      simp only [<-Region.vsubst_fromWk, Region.vsubst_vsubst]
+      congr
+      funext k; cases k using Nat.cases2 with
+      | zero => simp only [Term.Subst.comp, Term.subst0_zero, Term.subst_fromWk, Term.wk_wk,
+        Nat.liftWk_succ_comp_succ, Term.subst, Function.comp_apply, Nat.swap0_0, Nat.liftWk_succ,
+        Nat.succ_eq_add_one, zero_add, Nat.reduceAdd, zero_lt_one, Nat.swap0_lt,
+        Term.Subst.lift_succ]; rfl
+      | _ => rfl
+    | succ => rfl
+  · rw [Region.vwk_vwk, <-Region.vsubst_fromWk, Region.vsubst_vsubst, Region.vsubst_id']
+    funext k; cases k <;> rfl
+
+-- theorem Eqv.lsubst_let2_alpha0 {Γ : Ctx α ε} {L : LCtx α}
+--   (p : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩)
+--   (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (C::L))
+--   : lsubst (let2 p.wk0.wk0 s).alpha0 r
+--   = let2 p.wk0 (lsubst (alpha0 s.vswap02.vswap02) r.vwk0.vwk0)
+--   := by induction r using Eqv.arrow_induction with
+--   | br ℓ a hℓ =>
+--     cases ℓ with
+--     | zero =>
+--       induction p using Quotient.inductionOn
+--       induction s using Quotient.inductionOn
+--       induction a using Quotient.inductionOn
+--       apply Eqv.eq_of_reg_eq
+--       simp only [Set.mem_setOf_eq, InS.lsubst_br, List.length_cons, List.get_eq_getElem,
+--         InS.coe_vsubst, Term.InS.coe_subst0, InS.coe_vwk_id, Subst.InS.coe_get, InS.coe_alpha0,
+--         InS.coe_let2, Term.InS.coe_wk, Ctx.InS.coe_wk0, InS.vwk_br, InS.coe_vwk, Ctx.InS.coe_swap02]
+--       simp only [Region.vsubst, Term.wk_succ_subst_subst0, alpha, ← vsubst_fromWk,
+--         Region.vsubst_vsubst, Function.update_same, let2.injEq, true_and]
+--       congr
+--       funext k; cases k using Nat.cases3 with
+--       | two => simp only [Term.Subst.liftn, lt_self_iff_false, ↓reduceIte, le_refl,
+--         tsub_eq_zero_of_le, Term.subst0_zero, Term.Subst.comp, Term.subst, Term.wk_wk,
+--         Nat.one_lt_ofNat, Nat.swap0_lt, Nat.ofNat_pos]; rfl
+--       | _ => rfl
+--     | succ ℓ => simp [get_alpha0, let2_br, Term.Eqv.nil, Term.Eqv.let2_wk0_wk0_pure]
+--   | let1 a r => sorry
+--   | let2 a r => sorry
+--   | case a l r => sorry
+--   | cfg R β G => sorry
+
+theorem Eqv.seq_let2_wk0_pure {Γ : Ctx α ε} {L : LCtx α}
+  {a : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩}
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)}
+  : r ;; (let2 a.wk0 s) = let2 a.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by
+  sorry
+  -- rw [seq, vwk1_let2, Term.Eqv.wk0_wk1, lsubst_let2_alpha0]
+  -- congr
+  -- rw [seq]
+  -- induction r using Quotient.inductionOn
+  -- induction s using Quotient.inductionOn
+  -- induction a using Quotient.inductionOn
+  -- apply Eqv.eq_of_reg_eq
+  -- simp only [Set.mem_setOf_eq, InS.coe_lsubst, InS.coe_alpha0, InS.coe_vwk, Ctx.InS.coe_swap02,
+  --   Ctx.InS.coe_wk3, Ctx.InS.coe_wk0, Ctx.InS.coe_wk1, vwk_lsubst]
+  -- congr 1
+  -- · funext k; cases k with
+  --   | zero =>
+  --     simp only [alpha, Region.vwk_vwk, Function.update_same, Function.comp_apply]
+  --     congr
+  --     funext k; cases k using Nat.cases3 <;> rfl
+  --   | succ => rfl
+  -- · simp only [Region.vwk_vwk]; congr; funext k; cases k <;> rfl
+
+theorem Eqv.seq_let2_wk0_pure' {Γ : Ctx α ε} {L : LCtx α}
+  {a : Term.Eqv φ (_::Γ) ⟨X.prod Y, ⊥⟩} {a' : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩}
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)}
+  (ha : a = a'.wk0)
+  : r ;; (let2 a s) = let2 a'.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by
+  cases ha; rw [seq_let2_wk0_pure]
+
 
 theorem Eqv.case_seq {Γ : Ctx α ε} {L : LCtx α}
   (a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨X.coprod Y, e⟩)

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -721,6 +721,18 @@ theorem Eqv.vwk1_shf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α}
   : d.shf.vwk1 (inserted := inserted) = (d.vwk1).shf := by
   induction d using Quotient.inductionOn; rfl
 
+@[simp]
+theorem Eqv.vwk_br {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Γ.InS Δ}
+  {ℓ} {a : Term.Eqv φ Δ ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A}
+  : Eqv.vwk ρ (Eqv.br ℓ a hℓ) = Eqv.br ℓ (a.wk ρ) hℓ := by
+  induction a using Quotient.inductionOn; rfl
+
+@[simp]
+theorem Eqv.vwk0_br {Γ : Ctx α ε} {L : LCtx α}
+  {ℓ} {a : Term.Eqv φ Γ ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A}
+  : Eqv.vwk0 (Eqv.br ℓ a hℓ) = Eqv.br ℓ (a.wk0 (head := head)) hℓ := by
+  induction a using Quotient.inductionOn; rfl
+
 @[simp]
 theorem Eqv.vwk1_br {Γ : Ctx α ε} {L : LCtx α}
   {ℓ} {a : Term.Eqv φ (head::Γ) ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A}
@@ -775,6 +787,21 @@ theorem Eqv.vwk1_vwk2 {Γ : Ctx α ε} {L : LCtx α}
   congr 1
   ext k; cases k <;> rfl
 
+def Eqv.vwk3 {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (left::middle::right::Γ) L)
+  : Eqv φ (left::middle::right::inserted::Γ) L := Eqv.vwk Ctx.InS.wk3 r
+
+@[simp]
+theorem Eqv.vwk3_quot {Γ : Ctx α ε} {L : LCtx α} {r : InS φ (left::middle::right::Γ) L}
+  : Eqv.vwk3 (inserted := inserted) ⟦r⟧ = ⟦r.vwk3⟧ := rfl
+
+theorem Eqv.vwk1_let2 {L : LCtx α}
+  {a : Term.Eqv φ (⟨X, ⊥⟩::Γ) ⟨Ty.prod A B, e⟩} {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) L}
+  : vwk1 (inserted := inserted) (let2 a r)
+  = let2 a.wk1 r.vwk3 := by
+  induction a using Quotient.inductionOn; induction r using Quotient.inductionOn;
+  apply Eqv.eq_of_reg_eq
+  simp [Nat.liftnWk_succ]
+
 def Eqv.vswap01
   {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (left::right::Γ) L)
   : Eqv φ (right::left::Γ) L := Eqv.vwk Ctx.InS.swap01 r
@@ -793,6 +820,15 @@ theorem Eqv.vswap02_quot
   {Γ : Ctx α ε} {L : LCtx α} {r : InS φ (left::mid::right::Γ) L}
   : Eqv.vswap02 ⟦r⟧ = ⟦r.vswap02⟧ := rfl
 
+def Eqv.vswap03
+  {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (first::second::third::fourth::Γ) L)
+  : Eqv φ (second::third::fourth::first::Γ) L := Eqv.vwk Ctx.InS.swap03 r
+
+@[simp]
+theorem Eqv.vswap03_quot
+  {Γ : Ctx α ε} {L : LCtx α} {r : InS φ (first::second::third::fourth::Γ) L}
+  : Eqv.vswap03 ⟦r⟧ = ⟦r.vswap03⟧ := rfl
+
 def Eqv.lwk0
   {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ Γ L)
   : Eqv φ Γ (head::L) := Eqv.lwk LCtx.InS.wk0 r

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

@@ -17,6 +17,10 @@ def Eqv.nil {A : Ty α} {Γ : Ctx α ε} : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A, e⟩
 theorem Eqv.wk0_nil {A : Ty α} {Γ : Ctx α ε}
   : (nil : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A, e⟩).wk0 (head := ⟨head, ⊥⟩) = (var 1 (by simp)) := rfl
 
+@[simp]
+theorem Eqv.wk_id_nil {A : Ty α} {Γ Δ : Ctx α ε} {hΓ : Ctx.Wkn (⟨A, ⊥⟩::Γ) ((A, ⊥)::Δ) id}
+  : (nil : Eqv φ (⟨A, ⊥⟩::Δ) ⟨A, e⟩).wk_id hΓ = nil := rfl
+
 @[simp]
 theorem Eqv.wk1_nil {A : Ty α} {Γ : Ctx α ε}
   : (nil (φ := φ) (A := A) (Γ := Γ) (e := e)).wk1 (inserted := inserted) = nil

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -1643,6 +1643,9 @@ theorem Eqv.Pure.let2_wk0_wk0 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A.prod B, e⟩}
     apply Pure.wk0
     exact ⟨a.let2 (var 0 (by simp)), by simp⟩
 
+theorem Eqv.let2_wk0_wk0_pure {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A.prod B, ⊥⟩} {b : Eqv φ Γ ⟨C, ⊥⟩}
+  : let2 a b.wk0.wk0 = b := Eqv.Pure.let2_wk0_wk0 (by simp)
+
 theorem Eqv.Pure.let1_let2_of_right {Γ : Ctx α ε}
   {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B.prod C, e⟩} {c : Eqv φ (⟨C, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨D, e⟩}
   (hb : b.Pure) : let1 a (let2 b.wk0 c) = let2 b (let1 a.wk0.wk0 c.swap02.swap02) := by

DeBruijnSSA/BinSyntax/Syntax/Definitions.lean

@@ -851,6 +851,8 @@ def Region.vswap01 : Region φ → Region φ := vwk (Nat.swap0 1)
 
 def Region.vswap02 : Region φ → Region φ := vwk (Nat.swap0 2)
 
+def Region.vswap03 : Region φ → Region φ := vwk (Nat.swap0 3)
+
 theorem Region.vwk_vwk1 (r : Region φ) : r.vwk1.vwk ρ = r.vwk (ρ ∘ Nat.liftWk Nat.succ)
   := by simp only [vwk1, vwk_vwk, <-Nat.liftWk_comp]
 

DeBruijnSSA/BinSyntax/Typing/Ctx.lean

@@ -259,9 +259,17 @@ theorem InS.coe_swap02 {first second third : Ty α × ε} {Γ : Ctx α ε}
   : (InS.swap02 (Γ := Γ) (first := first) (second := second) (third := third) : ℕ → ℕ) = Nat.swap0 2
   := rfl
 
--- def InS.swap03 {first second third fourth : Ty α × ε} {Γ : Ctx α ε}
---   : InS (first::second::third::fourth::Γ) (fourth::first::second::third::Γ)
---   := ⟨Nat.swap0 3, λi hi => sorry⟩
+theorem Wkn.swap03 {first second third fourth : Ty α × ε} {Γ : Ctx α ε}
+  : Wkn (first::second::third::fourth::Γ) (fourth::first::second::third::Γ) (Nat.swap0 3)
+  | 0, _ => by simp
+  | 1, _ => by simp
+  | 2, _ => by simp
+  | 3, _ => by simp
+  | n + 4, hn => ⟨hn, by simp⟩
+
+def InS.swap03 {first second third fourth : Ty α × ε} {Γ : Ctx α ε}
+  : InS (first::second::third::fourth::Γ) (fourth::first::second::third::Γ)
+  := ⟨Nat.swap0 3, Wkn.swap03⟩
 
 def Nat.swap20 : ℕ → ℕ
   | 0 => 2
@@ -339,6 +347,27 @@ theorem InS.coe_wk2 {left right inserted} {Γ : Ctx α ε}
   = Nat.liftnWk 2 Nat.succ
   := rfl
 
+theorem Wkn.wk3 {left middle right inserted} {Γ : Ctx α ε}
+  : Wkn (left::middle::right::inserted::Γ) (left::middle::right::Γ) (Nat.liftnWk 3 Nat.succ)
+  := by intro i hi; cases i using Nat.cases3 with
+  | rest =>
+      simp only [Nat.liftnWk, add_lt_iff_neg_right, not_lt_zero', ↓reduceIte,
+        add_tsub_cancel_right, Nat.succ_eq_add_one, List.length_cons, List.get_eq_getElem,
+        List.getElem_cons_succ, Var.step_iff];
+      simp only [List.length_cons, add_lt_add_iff_right] at hi
+      exact ⟨hi, by simp⟩
+  | _ => simp [Nat.liftnWk]
+
+def InS.wk3 {left middle right inserted} {Γ : Ctx α ε}
+  : InS (left::middle::right::inserted::Γ) (left::middle::right::Γ)
+  := ⟨Nat.liftnWk 3 Nat.succ, Wkn.wk3⟩
+
+@[simp]
+theorem InS.coe_wk3 {left middle right inserted} {Γ : Ctx α ε}
+  : (InS.wk3 (Γ := Γ) (left := left) (middle := middle) (right := right) (inserted := inserted) : ℕ → ℕ)
+  = Nat.liftnWk 3 Nat.succ
+  := rfl
+
 @[simp]
 theorem InS.coe_liftn₂ {V₁ V₁' V₂ V₂' : Ty α × ε} (hV₁ : V₁ ≤ V₁') (hV₂ : V₂ ≤ V₂') (ρ : InS Γ Δ)
   : (InS.liftn₂ hV₁ hV₂ ρ : ℕ → ℕ) = Nat.liftnWk 2 ρ

DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean

@@ -625,6 +625,14 @@ theorem InS.vwk1_let1 {Γ : Ctx α ε} {L : LCtx α} {A e}
   : (t.let1 a).vwk1 (inserted := inserted) = let1 a.wk1 t.vwk2
   := by ext; simp [Region.vwk1, Nat.liftnWk_two, Region.vwk2, Term.wk1]
 
+def InS.vwk3 {Γ : Ctx α ε} {L} (r : InS φ (left::middle::right::Γ) L)
+  : InS φ (left::middle::right::inserted::Γ) L
+  := r.vwk Ctx.InS.wk3
+
+@[simp]
+theorem InS.coe_vwk3 {Γ : Ctx α ε} {L} {r : InS φ (left::middle::right::Γ) L}
+  : (r.vwk3 (inserted := inserted) : Region φ) = (r : Region φ).vwk3 := rfl
+
 def InS.vswap01 {Γ : Ctx α ε} {L} (r : InS φ (left::right::Γ) L) : InS φ (right::left::Γ) L
   := r.vwk Ctx.InS.swap01
 
@@ -640,6 +648,14 @@ def InS.vswap02 {Γ : Ctx α ε} {L} (r : InS φ (left::mid::right::Γ) L)
 theorem InS.coe_vswap02 {Γ : Ctx α ε} {L} {r : InS φ (left::mid::right::Γ) L}
   : (r.vswap02 : Region φ) = r.vswap02 := rfl
 
+def InS.vswap03 {Γ : Ctx α ε} {L} (r : InS φ (first::second::third::fourth::Γ) L)
+  : InS φ (second::third::fourth::first::Γ) L
+  := r.vwk Ctx.InS.swap03
+
+@[simp]
+theorem InS.coe_vswap03 {Γ : Ctx α ε} {L} {r : InS φ (first::second::third::fourth::Γ) L}
+  : (r.vswap03 : Region φ) = r.vswap03 := rfl
+
 def InS.lwk {Γ : Ctx α ε} (ρ : L.InS K) (r : InS φ Γ L) : InS φ Γ K
   := ⟨(r : Region φ).lwk ρ, r.2.lwk ρ.prop⟩