Work on packed term theory

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

@@ -21,11 +21,18 @@ def Eqv.pl {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B, e⟩) : Eq
 theorem Eqv.pl_quot {A B : Ty α} {Γ : Ctx α ε} {a : InS φ Γ ⟨A.prod B, e⟩}
   : pl ⟦a⟧ = ⟦a.pl⟧ := rfl
 
+@[simp]
 theorem Eqv.wk_pl {A B : Ty α} {Γ : Ctx α ε} {ρ : Ctx.InS Γ Δ}
   {a : Eqv φ Δ ⟨A.prod B, e⟩}
   : (a.pl).wk ρ = (a.wk ρ).pl := by
   induction a using Quotient.inductionOn; rfl
 
+@[simp]
+theorem Eqv.subst_pl {A B : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
+  {a : Eqv φ Δ ⟨A.prod B, e⟩}
+  : (a.pl).subst σ = (a.subst σ).pl := by
+  induction a using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl
+
 theorem Eqv.wk0_pl {A B : Ty α} {Γ : Ctx α ε}
   {a : Eqv φ Γ ⟨A.prod B, e⟩}
   : (a.pl).wk0 (head := head) = a.wk0.pl := by rw [wk0, wk_pl]; rfl
@@ -49,11 +56,18 @@ def Eqv.pr {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B, e⟩) : Eq
 theorem Eqv.pr_quot {A B : Ty α} {Γ : Ctx α ε} {a : InS φ Γ ⟨A.prod B, e⟩}
   : pr ⟦a⟧ = ⟦a.pr⟧ := rfl
 
+@[simp]
 theorem Eqv.wk_pr {A B : Ty α} {Γ : Ctx α ε} {ρ : Ctx.InS Γ Δ}
   {a : Eqv φ Δ ⟨A.prod B, e⟩}
   : (a.pr).wk ρ = (a.wk ρ).pr := by
   induction a using Quotient.inductionOn; rfl
 
+@[simp]
+theorem Eqv.subst_pr {A B : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
+  {a : Eqv φ Δ ⟨A.prod B, e⟩}
+  : (a.pr).subst σ = (a.subst σ).pr := by
+  induction a using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl
+
 theorem Eqv.wk0_pr {A B : Ty α} {Γ : Ctx α ε}
   {a : Eqv φ Γ ⟨A.prod B, e⟩}
   : (a.pr).wk0 (head := head) = a.wk0.pr := by rw [wk0, wk_pr]; rfl

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

@@ -105,6 +105,17 @@ theorem Eqv.wk1_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length}
   : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk1 (inserted := inserted) = unpack0 i := by
   simp [unpack0]
 
+@[simp]
+theorem Eqv.wk_lift_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} {ρ : Γ.InS Δ}
+  : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk (ρ.lift (le_refl _)) = unpack0 i := by
+  simp [unpack0]
+
+@[simp]
+theorem Eqv.subst_lift_unpack0 {Γ Δ Δ' : Ctx α ε} {i : Fin Γ.length} {σ : Subst.Eqv φ Δ' Δ}
+  : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).subst (σ.lift (le_refl _)) = unpack0 i := by
+  induction σ using Quotient.inductionOn
+  simp [unpack0]
+
 @[simp]
 theorem Eqv.subst0_nil_pr_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length}
   : (Eqv.unpack0 (φ := φ) (Γ := Γ) (e := e) i).subst (nil.pr.subst0)
@@ -123,6 +134,9 @@ theorem Eqv.pl_pack_drop'  {Γ Δ : Ctx α ε} {i : Fin Γ.length}
 theorem Eqv.unpack0_def {Γ Δ : Ctx α ε} (i : Fin Γ.length) :
   Eqv.unpack0 (φ := φ) (Δ := Δ) (e := e) i = ⟦Term.InS.unpack0 i⟧ := rfl
 
+theorem Eqv.unpack0_zero {Γ Δ : Ctx α ε}
+  : Eqv.unpack0 (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) (0 : Fin (Γ.length + 1)) = pi_l := rfl
+
 theorem Eqv.unpack0_succ {Γ Δ : Ctx α ε} (i : Fin Γ.length)
   : unpack0 (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ = pi_r ;;' unpack0 i := by
   rw [seq, <-wk_eff_pi_r, let1_beta, wk1_unpack0, subst0_pi_r_unpack0]
@@ -224,20 +238,106 @@ theorem Eqv.unpack0_eq_unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) :
       unpack0', Fin.val_zero, List.getElem_cons_zero, Fin.cases_succ, <-I]
     rw [<-wk1_unpack0, <-wk1_unpack0, <-nil, <-pi_r_seq, unpack0_succ]
 
--- theorem Eqv.unpacked_unpack0 {Γ : Ctx α ε} {h : Γ.Pure} {i}
---   : (Eqv.unpack0 (φ := φ) (e := e) i).unpacked h = var i (h.any_effect_refl i.prop)
---   := sorry
+theorem Eqv.unpacked_unpack0 {Γ : Ctx α ε} {h : Γ.Pure} {i}
+  : (Eqv.unpack0 (φ := φ) (e := e) i).unpacked h = var i (h.any_effect_refl i.prop)
+  := by induction Γ with
+  | nil => exact i.elim0
+  | cons V Γ I => cases i using Fin.cases with
+  | zero =>
+    simp [unpack0_zero, unpacked_def', pi_l, nil, subst_var, pl, Subst.Eqv.get_liftn₂_one]
+    rw [<-pl, pack, Pure.pl_pair]
+    exact Pure.wk0 ⟨h.tail.packE, by simp⟩
+  | succ i =>
+    rw [unpacked_def', unpack0_succ, seq]
+    simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ,
+      wk1_unpack0, subst_let1, subst_lift_unpack0]
+    simp [pi_r, pr, nil, subst_var]
+    rw [<-pr, pack, Pure.pr_pair, <-wk1_unpack0, <-wk0_let1, <-wk0_var]
+    apply congrArg
+    exact I (h := h.tail)
+    exact ⟨var 0 (h.any_effect_refl (by simp)), rfl⟩
 
--- @[simp]
--- theorem Subst.Eqv.packSE_comp_unpack {Γ : Ctx α ε} (h : Γ.Pure)
---   : h.packSE.comp unpack = Subst.Eqv.id (φ := φ) := by
---   ext k; simp only [List.get_eq_getElem, get_comp, get_unpack, get_id]
---   rw [<-Eqv.unpacked_unpack0, Eqv.unpacked_def']
+@[simp]
+theorem Subst.Eqv.packSE_comp_unpack {Γ : Ctx α ε} (h : Γ.Pure)
+  : h.packSE.comp unpack = Subst.Eqv.id (φ := φ) := by
+  ext k; simp only [List.get_eq_getElem, get_comp, get_unpack, get_id]
+  rw [<-Eqv.unpacked_unpack0, Eqv.unpacked_def']
 
 theorem Eqv.packed_unpacked {Γ : Ctx α ε} {a : Eqv φ [(Γ.pack, ⊥)] (A, e)} {h : Γ.Pure}
   : (a.unpacked h).packed = a := by simp [unpacked_def', packed, subst_subst]
 
--- theorem Eqv.unpacked_packed {Γ : Ctx α ε} {a : Eqv φ Γ (A, e)} {h : Γ.Pure}
---   : a.packed.unpacked h = a := by simp [unpacked_def', packed, subst_subst]
+theorem Eqv.unpacked_packed {Γ : Ctx α ε} {a : Eqv φ Γ (A, e)} {h : Γ.Pure}
+  : a.packed.unpacked h = a := by simp [unpacked_def', packed, subst_subst]
+
+theorem Eqv.packed_injective {Γ : Ctx α ε} {a b : Eqv φ Γ V} (hΓ : Γ.Pure)
+  (h : a.packed (Δ := []) = b.packed) : a = b := by
+  rw [<-unpacked_packed (a := a), <-unpacked_packed (a := b), h]; exact hΓ
+
+theorem Eqv.unpacked_injective {Γ : Ctx α ε} {a b : Eqv φ [(Γ.pack, ⊥)] (A, e)} {hΓ : Γ.Pure}
+  (h : a.unpacked hΓ = b.unpacked hΓ) : a = b := by
+  rw [<-packed_unpacked (a := a), <-packed_unpacked (a := b), h]
+
+@[simp]
+theorem Eqv.packed_var {Γ : Ctx α ε} {i} {hv}
+  : (var (V := V) i hv).packed (Δ := Δ)
+  = (unpack0 (φ := φ) (Γ := Γ) ⟨i, hv.length⟩).wk_res hv.get := by simp [packed, subst_var]
+
+theorem Eqv.packed_let1 {Γ : Ctx α ε} {A B : Ty α}
+  {a : Eqv φ Γ (A, e)} {b : Eqv φ ((A, ⊥)::Γ) (B, e)}
+  : (let1 a b).packed (Δ := Δ)
+  = let1 a.packed (let1 (pair (var 0 (by simp)) (var 1 (by simp))) b.packed) := by
+  rw [packed, subst_let1]; apply congrArg
+  rw [
+    packed, let1_beta' (a' := pair (var 0 (by simp)) (var 1 (by simp))) (h := by simp),
+    subst_subst
+  ]; congr
+  ext k
+  cases k using Fin.cases with
+  | zero =>
+    simp [Subst.Eqv.get_comp, unpack0_zero, pi_l, nil, pl, let2_pair, let1_beta_var0, let1_beta_var1]
+  | succ k =>
+    simp [
+      Subst.Eqv.get_comp, unpack0_succ, seq, pi_r, nil, pr, let2_pair, let1_beta_var0,
+      let1_beta_var1
+    ]
+    rw [wk0, <-subst_fromWk]
+    apply eq_of_term_eq
+    apply subst_eqOn_fvi
+    intro i
+    simp only [InS.coe_unpack0, fvi_unpack0]
+    simp only [Set.mem_Iio, Nat.lt_one_iff, Set.mem_setOf_eq, Ctx.InS.coe_toSubst, Ctx.InS.coe_wk0,
+      Subst.fromWk_apply, Nat.succ_eq_add_one, InS.coe_subst0, InS.coe_var]
+    intro i; cases i; rfl
+
+-- theorem Eqv.packed_let2 {Γ : Ctx α ε} {A B C : Ty α}
+--   {a : Eqv φ Γ (A.prod B, e)} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) (C, e)}
+--   : (let2 a b).packed (Δ := Δ)
+--   = let2 a.packed (
+--       let1 (pair (var 0 (by simp)) (pair (var 1 (by simp)) (var 2 (by simp)))) b.packed) := by
+--   sorry
+
+-- theorem Eqv.packed_case {Γ : Ctx α ε} {A B : Ty α}
+--   {a : Eqv φ Γ (A.coprod B, e)} {l : Eqv φ ((A, ⊥)::Γ) (C, e)} {r : Eqv φ ((B, ⊥)::Γ) (C, e)}
+--   : (case a l r).packed (Δ := Δ)
+--   = case a.packed
+--     (let1 (pair (var 0 (by simp)) (var 1 (by simp))) l.packed)
+--     (let1 (pair (var 0 (by simp)) (var 1 (by simp))) r.packed) := by
+--   sorry
+
+@[simp]
+theorem Eqv.packed_inl {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (A, e)}
+  : (inl (B := B) a).packed (Δ := Δ) = inl a.packed := by simp [packed]
+
+@[simp]
+theorem Eqv.packed_inr {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (B, e)}
+  : (inr (A := A) a).packed (Δ := Δ) = inr a.packed := by simp [packed]
+
+@[simp]
+theorem Eqv.packed_abort {Γ : Ctx α ε} {A : Ty α} {a : Eqv φ Γ (Ty.empty, e)}
+  : (abort a A).packed (Δ := Δ) = abort a.packed A := by simp [packed]
+
+@[simp]
+theorem Eqv.packed_unit {Γ : Ctx α ε} : (unit (φ := φ) (Γ := Γ) (e := e)).packed (Δ := Δ) = unit _
+  := rfl
 
 end Term

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -668,6 +668,51 @@ def Subst.Eqv.get (σ : Subst.Eqv φ Γ Δ) (i : Fin Δ.length) : Term.Eqv φ Γ
 theorem Subst.Eqv.get_quot {σ : Subst.InS φ Γ Δ} {i : Fin Δ.length}
   : get ⟦σ⟧ i = ⟦σ.get i⟧ := rfl
 
+@[simp]
+theorem Subst.Eqv.get_lift_zero {h : lo ≤ hi} {σ : Eqv φ Γ Δ}
+  : (σ.lift h).get (0 : Fin (Δ.length + 1)) = Eqv.var 0 (by simp [h]) := by
+  induction σ using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  rfl
+
+@[simp]
+theorem Subst.Eqv.get_lift_succ {h : lo ≤ hi} {σ : Eqv φ Γ Δ} {i : Fin Δ.length}
+  : (σ.lift h).get i.succ = (σ.get i).wk0 := by
+  induction σ using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  rfl
+
+@[simp]
+theorem Subst.Eqv.get_liftn₂_zero {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ}
+  : (σ.liftn₂ h₁ h₂).get (0 : Fin (Δ.length + 2)) = Eqv.var 0 (by simp [h₁]) := by
+  induction σ using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  rfl
+
+theorem Subst.Eqv.get_liftn₂_one {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ}
+  : (σ.liftn₂ h₁ h₂).get (1 : Fin (Δ.length + 2)) = Eqv.var 1 (by simp [h₂]) := by
+  induction σ using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  rfl
+
+theorem Subst.Eqv.get_liftn₂_succ_succ
+  {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ} {i : Fin Δ.length}
+  : (σ.liftn₂ h₁ h₂).get i.succ.succ = (σ.get i).wk0.wk0 := by
+  induction σ using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  simp only [Nat.succ_eq_add_one, List.get_eq_getElem, List.length_cons, Fin.val_succ,
+    List.getElem_cons_succ, Set.mem_setOf_eq, InS.coe_get, InS.coe_liftn₂, liftn, Nat.reduceSubDiff,
+    InS.coe_wk, Ctx.InS.coe_wk0, wk_wk]
+  rfl
+
+@[simp]
+theorem Subst.Eqv.get_liftn₂_succ {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ}
+  {i : Fin (Δ.length + 1)}
+  : (σ.liftn₂ h₁ h₂).get i.succ = ((σ.lift h₂).get i).wk0 := by
+  cases i using Fin.cases with
+  | zero => convert get_liftn₂_one; simp
+  | succ i => convert get_liftn₂_succ_succ using 1; simp
+
 theorem Subst.Eqv.ext_quot {σ τ : Subst.InS φ Γ Δ}
   (h : ∀i, (⟦σ.get i⟧ : Term.Eqv φ _ _) = ⟦τ.get i⟧) : (⟦σ⟧ : Subst.Eqv φ Γ Δ) = ⟦τ⟧
   := Quotient.sound (λi => Quotient.exact $ h i)

DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean

@@ -66,6 +66,13 @@ theorem wk_lift_unpack0 {x : ℕ} : (unpack0 (φ := φ) x).wk (Nat.liftWk ρ) =
   | zero => rfl
   | succ x ih => simp only [wk_pr, Function.iterate_succ_apply', ih]
 
+@[simp]
+theorem fvi_unpack0 {x : ℕ} : fvi (unpack0 (φ := φ) x) = 1 := by
+  simp only [fvi, Nat.reduceAdd, le_refl, tsub_eq_zero_of_le, zero_le, max_eq_left]
+  induction x with
+  | zero => rfl
+  | succ x ih => simp [Function.iterate_succ_apply', ih]
+
 @[simp]
 theorem subst_lift_unpack0 {x : ℕ} {σ : Subst φ} : (unpack0 x).subst σ.lift = unpack0 x := by
   simp only [unpack0, subst_pl]
@@ -176,6 +183,16 @@ theorem InS.wk1_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length}
   : (InS.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk1 (inserted := inserted) = unpack0 i := by
   ext; rw [coe_unpack0, coe_wk1, coe_unpack0, Term.wk1_unpack0]
 
+@[simp]
+theorem InS.wk_lift_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} {ρ : Γ.InS Δ}
+  : (InS.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk (ρ.lift (le_refl _)) = unpack0 i := by
+  ext; rw [coe_unpack0, coe_wk, coe_unpack0, Ctx.InS.coe_lift, Term.wk_lift_unpack0]
+
+@[simp]
+theorem InS.subst_lift_unpack0 {Γ Δ Δ' : Ctx α ε} {i : Fin Γ.length} {σ : Subst.InS φ Δ' Δ}
+  : (InS.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).subst (σ.lift (le_refl _)) = unpack0 i := by
+  ext; rw [coe_unpack0, coe_subst, coe_unpack0, Subst.InS.coe_lift, Term.subst_lift_unpack0]
+
 @[simp]
 theorem InS.subst0_nil_pr_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length}
   : (InS.unpack0 (φ := φ) (Γ := Γ) (e := e) i).subst (nil.pr.subst0)