Term associator naturality

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

@@ -768,15 +768,15 @@ theorem Eqv.assoc_inv_assoc {A B C : Ty α} {Γ : Ctx α ε}
   : assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) ;;' assoc = nil := by
   rw [seq_prod_assoc, assoc_inv, reassoc_reassoc_inv]
 
-theorem Eqv.reassoc_left {A B C A' : Ty α} {Γ : Ctx α ε}
-  (l : Eqv φ (⟨A, ⊥⟩::Γ) (A', e))
-  : ((l ⋉' B) ⋉' C).reassoc = assoc ;;' l ⋉' (B.prod C) := by
-  conv => rhs; rw [assoc, reassoc, seq_let2, seq_let2]
-  simp only [wk1_ltimes]
+
+theorem Eqv.reassoc_tensor {A B C A' B' C' : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) (A', e)} {m : Eqv φ (⟨B, ⊥⟩::Γ) (B', e)} {r : Eqv φ (⟨C, ⊥⟩::Γ) (C', e)}
+  : (tensor (tensor l m) r).reassoc = assoc ;;' tensor l (tensor m r) := by
+  conv => rhs; rw [assoc, reassoc, seq_let2, seq_let2]; simp only [wk1_tensor]
   conv =>
     lhs
     simp only [
-      reassoc, ltimes, tensor, wk1_nil, wk1_let2, wk_pair, wk_liftn₂_nil, wk0_let2, wk0_nil,
+      reassoc, tensor, wk1_nil, wk1_let2, wk_pair, wk_liftn₂_nil, wk0_let2, wk0_nil,
       wk2_pair, wk2_nil, let2_let2, wk2_let2, wk2_var1, List.length_cons, Fin.mk_one,
       List.get_eq_getElem, Fin.val_one, List.getElem_cons_succ, List.getElem_cons_zero, wk_var,
       Set.mem_setOf_eq, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, le_refl,
@@ -788,20 +788,69 @@ theorem Eqv.reassoc_left {A B C A' : Ty α} {Γ : Ctx α ε}
       Nat.liftWk_succ
     ]
   congr 2
-  simp only [seq_ltimes, let2_pair, wk0_pair, let1_beta_var1]
+  simp only [seq_tensor, let2_pair, let1_beta_var1]
+  apply Eq.symm
+  rw [let1_beta' (a' := (pair (var 1 (by simp)) (var 3 (by simp))))]
+  simp only [subst_pair, subst0_wk0, wk1_tensor]
+  rw [Eqv.Pure.let1_let2_of_right' (b := var 0 (by simp))]
+  simp only [tensor, subst_let2, nil_subst0, wk_eff_pair, wk_eff_var, subst_pair, let2_pair,
+    wk0_var, Nat.reduceAdd, subst_let1, var_succ_subst0, subst_lift_var_succ, let1_beta_var0,
+    let1_beta_var2]
+  conv => rhs; simp only [wk1_let2, wk1_var0]
+  rw [let2_bind' (r := let1 r.wk1.wk1.wk0.wk0.wk0.wk1
+    (pair (var 2 (by simp)) (pair (var 1 (by simp)) (var 0 (by simp)))))]
+  rw [let1_pair_var_succ]
+  rw [let1_pair_var_1_left, let1_eta, let2_pair, let1_pair_var_1_left]
+  conv =>
+    rhs
+    rhs
+    rhs
+    tactic =>
+      rw [<-wk1_var0, <-wk1_pair, <-wk0_let1]
+      simp
+  rw [let1_pair_right, let1_eta, let1_pair_right, let1_eta]
+  congr
+  simp only [wk1, wk0, wk2, wk_wk]
+  simp only [<-subst_fromWk, subst_subst]
+  congr
+  apply Subst.Eqv.eq_of_subst_eq
+  intro k
+  cases k using Fin.cases <;> rfl
+  simp only [wk1, wk0, wk2, wk_wk]
+  simp only [<-subst_fromWk, subst_subst]
+  congr
+  apply Subst.Eqv.eq_of_subst_eq
+  intro k
+  cases k using Fin.cases <;> rfl
+  simp only [wk1, wk0, wk2, wk_wk]
+  simp only [<-subst_fromWk, subst_subst]
+  congr
+  apply Subst.Eqv.eq_of_subst_eq
+  intro k
+  cases k using Fin.cases <;> rfl
+  simp
+  simp
+  simp only [wk_let1, swap02, wk_pair, wk1, wk0, wk2, wk_wk]
+  rfl
+  exact ⟨var 0 (by simp), rfl⟩
+  rfl
+  rfl
 
 theorem Eqv.assoc_left_nat {A B C A' : Ty α} {Γ : Ctx α ε}
   (l : Eqv φ (⟨A, ⊥⟩::Γ) (A', e))
   : (l ⋉' B) ⋉' C ;;' assoc = assoc ;;' l ⋉' (B.prod C) := by
-  rw [seq_prod_assoc, reassoc_left]
+  simp only [seq_prod_assoc, ltimes, reassoc_tensor, tensor_nil_nil]
 
 theorem Eqv.assoc_mid_nat {A B C B' : Ty α} {Γ : Ctx α ε}
   (m : Eqv φ (⟨B, ⊥⟩::Γ) (B', e))
-  : (A ⋊' m) ⋉' C ;;' assoc = assoc ;;' A ⋊' (m ⋉' C) := sorry
+  : (A ⋊' m) ⋉' C ;;' assoc = assoc ;;' A ⋊' (m ⋉' C) := by
+  simp only [seq_prod_assoc, ltimes, rtimes, reassoc_tensor]
 
 theorem Eqv.assoc_right_nat {A B C C' : Ty α} {Γ : Ctx α ε}
   (r : Eqv φ (⟨C, ⊥⟩::Γ) (C', e))
-  : (A.prod B) ⋊' r ;;' assoc = assoc ;;' A ⋊' (B ⋊' r) := sorry
+  : (A.prod B) ⋊' r ;;' assoc = assoc ;;' A ⋊' (B ⋊' r) := by
+  rw [rtimes, <-tensor_nil_nil, seq_prod_assoc, reassoc_tensor]
+  rfl
 
 theorem Eqv.triangle {X Y : Ty α} {Γ : Ctx α ε}
   : assoc (φ := φ) (Γ := Γ) (A := X) (B := Ty.unit) (C := Y) (e := e) ;;' X ⋊' pi_r

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -1217,6 +1217,10 @@ theorem Eqv.let1_beta {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ (⟨A, ⊥⟩::Γ
   induction b using Quotient.inductionOn
   apply sound $ InS.let1_beta
 
+theorem Eqv.let1_beta' {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩} {a' : Eqv φ Γ ⟨A, ⊥⟩}
+  (h : a = a'.wk_eff (by simp))
+  : let1 a b = b.subst a'.subst0 := by cases h; rw [let1_beta]
+
 theorem Eqv.let1_beta_pure {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩}
   : let1 a b = b.subst a.subst0 := by rw [<-a.wk_eff_self, let1_beta, wk_eff_self]
 
@@ -1278,13 +1282,24 @@ theorem Eqv.pair_bind_left
   : pair a b = let1 a (pair (var 0 (by simp)) b.wk0)
   := by rw [pair_bind, pair_bind (a := (var 0 _)), let1_beta_var0, subst_let1, subst0_wk0]; rfl
 
+theorem Eqv.pair_bind_left'
+  {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {b'} (h :  b' = b.wk0)
+  : let1 a (pair (var 0 (by simp)) b') = pair a b
+  := by cases h; rw [<-pair_bind_left]
+
 theorem Eqv.let1_pair_right
   {Γ : Ctx α ε} {r : Eqv φ Γ ⟨X, e⟩} {a : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩}
   : let1 r (pair a b.wk0) = pair (let1 r a) b := by rw [
     pair_bind (b := b), let1_let1, let1_pair_var_1_left, let1_eta, wk1_pair, wk1_var0, wk0_wk1,
     <-pair_bind_left
   ]
 
+theorem Eqv.let1_pair_right'
+  {Γ : Ctx α ε} {r : Eqv φ Γ ⟨X, e⟩} {a : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {b'}
+  (h : b' = b.wk0)
+  : let1 r (pair a b') = pair (let1 r a) b
+  := by cases h; rw [<-let1_pair_right]
+
 theorem Eqv.let2_pair_right
   {Γ : Ctx α ε} {r : Eqv φ Γ ⟨X.prod Y, e⟩}
   {a : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::Γ) ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩}
@@ -1417,6 +1432,86 @@ theorem Eqv.pair_bind_swap
   : pair a b = (let1 b $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp)))
   := pair_bind_swap_left ⟨a, by simp⟩
 
+theorem Eqv.Pure.pair_left_let1
+  {Γ : Ctx α ε} {r : Eqv φ Γ ⟨X, e⟩} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ (⟨X, ⊥⟩::Γ) ⟨B, e⟩}
+  (h : a.Pure)
+  : pair a (let1 r b) = let1 r (pair a.wk0 b) := by
+  apply Eq.symm
+  have ⟨p, hp⟩ := h;
+  cases hp
+  convert let1_pair_wk_eff_left
+  induction p using Quotient.inductionOn
+  rfl
+
+theorem Eqv.Pure.pair_left_let1'
+  {Γ : Ctx α ε} {r : Eqv φ Γ ⟨X, e⟩} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ (⟨X, ⊥⟩::Γ) ⟨B, e⟩} {a'}
+  (h : a.Pure) (h' : a' = a.wk0)
+  : let1 r (pair a' b) = pair a (let1 r b) := by cases h'; rw [h.pair_left_let1]
+
+theorem Eqv.Pure.let1_let2_of_left {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B.prod C, e⟩} {c : Eqv φ (⟨C, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨D, e⟩}
+  : a.Pure → let1 a (let2 b.wk0 c) = let2 b (let1 a.wk0.wk0 c.swap02.swap02)
+  | ⟨a, ha⟩ => by
+    cases ha
+    simp only [let1_beta, wk0_wk_eff, subst_let2, subst0_wk0, swap02, wk_wk]
+    simp only [<-subst_fromWk, subst_subst]
+    congr 2
+    induction a using Quotient.inductionOn
+    apply Subst.Eqv.eq_of_subst_eq
+    intro i
+    cases i using Fin.cases with
+    | zero => rfl
+    | succ i => cases i using Fin.cases with
+      | zero => rfl
+      | succ i => cases i using Fin.cases with
+        | zero =>
+          ext
+          simp only [List.length_cons, Fin.succ_zero_eq_one, Fin.succ_one_eq_two, Fin.getElem_fin,
+            Nat.succ_eq_add_one, Fin.val_two, List.getElem_cons_succ, List.getElem_cons_zero,
+            Set.mem_setOf_eq, Subst.InS.get, Subst.InS.liftn₂, InS.coe_subst0, Subst.liftn,
+            lt_self_iff_false, ↓reduceIte, le_refl, tsub_eq_zero_of_le, subst0_zero,
+            Subst.InS.coe_comp, Subst.comp, Term.subst, Ctx.InS.coe_comp, Ctx.InS.coe_swap02,
+            Function.comp_apply, Nat.one_lt_ofNat, Nat.swap0_lt, Nat.ofNat_pos, InS.coe_wk,
+            Ctx.InS.coe_wk0, Term.wk_wk]
+          rfl
+        | succ i => rfl
+
+theorem Eqv.Pure.let1_let2_of_left' {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B.prod C, e⟩} {c : Eqv φ (⟨C, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨D, e⟩}
+  {b'} (ha : a.Pure) (hb : b' = b.wk0)
+  : let1 a (let2 b' c) = let2 b (let1 a.wk0.wk0 c.swap02.swap02)
+  := by cases hb; rw [ha.let1_let2_of_left]
+
+theorem Eqv.Pure.let2_let1_of_right {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B.prod C, e⟩} {c : Eqv φ (⟨C, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨D, e⟩}
+  {a' c'} (ha : a.Pure) (ha' : a' = a.wk0.wk0) (hc' : c' = c.swap02.swap02)
+  : let2 b (let1 a' c') = let1 a (let2 b.wk0 c) := by
+    rw [ha.let1_let2_of_left, ha', hc']
+
+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⟩}
+  : b.Pure → let1 a (let2 b.wk0 c) = let2 b (let1 a.wk0.wk0 c.swap02.swap02)
+  | ⟨b, hb⟩ => by
+    cases hb
+    rw [let2_bind, let1_let1]
+    apply Eq.symm
+    rw [let2_bind]
+    congr
+    sorry
+    sorry
+
+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⟩}
+  {b'} (hb : b.Pure) (hb' : b' = b.wk0)
+  : let1 a (let2 b' c) = let2 b (let1 a.wk0.wk0 c.swap02.swap02)
+  := by cases hb'; rw [hb.let1_let2_of_right]
+
+theorem Eqv.Pure.let2_let1_of_left {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B.prod C, e⟩} {c : Eqv φ (⟨C, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨D, e⟩}
+  {a' c'} (ha : b.Pure) (ha' : a' = a.wk0.wk0) (hc' : c' = c.swap02.swap02)
+  : let2 b (let1 a' c') = let1 a (let2 b.wk0 c) := by
+    rw [ha.let1_let2_of_right, ha', hc']
+
 end Basic
 
 end Term

DeBruijnSSA/BinSyntax/Typing/Ctx.lean

@@ -310,6 +310,12 @@ theorem InS.coe_swap02 {first second third : Ty α × ε} {Γ : Ctx α ε}
   : (InS.swap02 (Γ := Γ) (first := first) (second := second) (third := third) : ℕ → ℕ) = Nat.swap0 2
   := rfl
 
+def Nat.swap20 : ℕ → ℕ
+  | 0 => 2
+  | 1 => 0
+  | 2 => 1
+  | n + 3 => n + 3
+
 @[simp]
 theorem Wkn.add2 {first second} {Γ : Ctx α ε}
   : Wkn (first::second::Γ) Γ (· + 2)