Packwork

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

@@ -28,32 +28,53 @@ theorem Eqv.pack_sum_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
       ext
       simp [Term.pack0, Term.Wf.pack0, -Function.iterate_succ, Function.iterate_succ']
 
-def Eqv.pack' {Γ : Ctx α ε} : Eqv φ Γ (Γ.pack, Γ.sup_effect) := match Γ with
-  | [] => unit ⊥
-  | V::Γ => pair (var 0 (by cases V; simp)) ((pack' (Γ := Γ)).wk0.wk_eff (by simp))
-
-theorem Eqv.pack_def' {Γ : Ctx α ε} : Eqv.pack' (φ := φ) (Γ := Γ) = ⟦Term.InS.pack'⟧ := by
+def Eqv.pack {Γ : Ctx α ε} (h : ∀i, Γ.effect i ≤ e) : Eqv φ Γ (Γ.pack, e) := match Γ with
+  | [] => unit e
+  | V::Γ => pair
+    (var 0 (Ctx.Var.head (by constructor; rfl; convert (h 0); simp) _))
+    ((pack (Γ := Γ) (λi => by convert h (i + 1) using 1; simp)).wk0)
+
+theorem Eqv.pack_def {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ e}
+  : Eqv.pack (φ := φ) (Γ := Γ) h = ⟦Term.InS.pack h⟧ := by
   induction Γ with
   | nil => rfl
-  | cons _ _ I => simp only [pack', I]; rfl
+  | cons _ _ I => simp only [pack, I]; rfl
 
-def _root_.BinSyntax.Ctx.Pure.packE' {Γ : Ctx α ε} (h : Γ.Pure) : Eqv φ Γ (Γ.pack, ⊥) := match Γ with
-  | [] => Eqv.unit ⊥
-  | V::Γ => Eqv.pair (Eqv.var 0 (by cases V; convert h.head; simp)) h.tail.packE'.wk0
+abbrev _root_.BinSyntax.Ctx.Pure.packE {Γ : Ctx α ε} (h : Γ.Pure) : Eqv φ Γ (Γ.pack, ⊥)
+  := Eqv.pack (e := ⊥) (h := λi => by simp [h.effect i])
 
-theorem Eqv.packE_def' {Γ : Ctx α ε} {h : Γ.Pure} : h.packE' (φ := φ) = ⟦h.pack'⟧ := by
-  induction Γ with
-  | nil => rfl
-  | cons _ _ I => simp only [Ctx.Pure.packE', I]; rfl
+theorem Eqv.packE_def' {Γ : Ctx α ε} {h : Γ.Pure} : h.packE (φ := φ) = ⟦h.pack⟧ := by
+  simp only [Ctx.Pure.packE, pack_def]
+
+@[simp]
+theorem Eqv.wk_eff_pack {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ lo} {h' : lo ≤ hi}
+  : (pack (φ := φ) h).wk_eff h' = pack (λi => (h i).trans h') := by
+  simp [pack_def]
+
+theorem Eqv.wk_eff_packE {Γ : Ctx α ε} {h : Γ.Pure}
+  : h.packE.wk_eff bot_le = pack (φ := φ) (e := hi) (λi => by simp [h.effect]) := by simp
+
+@[simp]
+theorem  _root_.BinSyntax.Ctx.Pure.packP {Γ : Ctx α ε} (h : Γ.Pure) (h')
+  : Eqv.Pure (Eqv.pack (φ := φ) (Γ := Γ) (e := e) h')
+  := ⟨h.packE, by simp⟩
 
 def Eqv.pack_drop {Γ Δ : Ctx α ε} (i : Fin Γ.length)
   : Eqv φ ((Γ.pack, ⊥)::Δ) (Ctx.pack (Γ.drop i), e)
   := ⟦InS.pack_drop i⟧
 
+theorem Eqv.Pure.pack_drop {Γ Δ : Ctx α ε} {i : Fin Γ.length}
+  : Pure (pack_drop (φ := φ) (Δ := Δ) (e := e) i)
+  := ⟨Eqv.pack_drop i, rfl⟩
+
 def Eqv.pack_drop' {Γ Δ : Ctx α ε} (i : Fin Γ.length)
   : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1.prod (Ctx.pack (Γ.drop (i + 1))), e)
   := ⟦InS.pack_drop' i⟧
 
+theorem Eqv.Pure.pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length}
+  : Pure (pack_drop' (φ := φ) (Δ := Δ) (e := e) i)
+  := ⟨Eqv.pack_drop' i, rfl⟩
+
 theorem Eqv.cast_pack_drop {Γ Δ : Ctx α ε} {i : Fin Γ.length}
   : (Eqv.pack_drop (φ := φ) (Δ := Δ) (e := e) i).cast rfl (by rw [Ctx.pack_drop_fin]) = pack_drop' i
   := rfl
@@ -71,6 +92,10 @@ def Eqv.pack_drop_succ {Γ Δ : Ctx α ε} (i : Fin Γ.length)
 def Eqv.unpack0 {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e)
   := ⟦InS.unpack0 i⟧
 
+theorem Eqv.Pure.unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length}
+  : Pure (unpack0 (φ := φ) (Δ := Δ) (e := e) i)
+  := ⟨Eqv.unpack0 i, rfl⟩
+
 theorem Eqv.pl_pack_drop'  {Γ Δ : Ctx α ε} {i : Fin Γ.length}
   : (Eqv.pack_drop' (φ := φ) (Δ := Δ) (e := e) i).pl = unpack0 i := rfl
 
@@ -95,6 +120,34 @@ theorem Eqv.unpack0_def' {Γ Δ : Ctx α ε} (i : Fin Γ.length) :
     ]
     cases i using Fin.cases <;> rfl
 
+def Subst.Eqv.unpack {Γ Δ : Ctx α ε} : Subst.Eqv φ ((Γ.pack, ⊥)::Δ) Γ := ⟦Subst.InS.unpack⟧
+
+def Eqv.packed {Γ Δ : Ctx α ε} (a : Eqv φ Γ V) : Eqv φ ((Γ.pack, ⊥)::Δ) V
+  := a.subst Subst.Eqv.unpack
+
+def Eqv.unpacked {Γ : Ctx α ε} (a : Eqv φ [(Γ.pack, ⊥)] (A, e)) (h : ∀i, Γ.effect i ≤ e)
+  : Eqv φ Γ (A, e) := let1 (pack h) (a.wk_id (by simp [Ctx.Wkn.drop]))
+
+-- theorem Eqv.packed_unpacked {Γ : Ctx α ε} {a : Eqv φ [(Γ.pack, ⊥)] (A, e)} (h : Γ.Pure)
+--   : (a.unpacked (λi => by simp [h.effect])).packed = a := by
+--   rw [
+--     unpacked, <-wk_eff_packE (h := h), let1_beta, packed, subst_subst, <-wk_eq_wk_id,
+--     <-subst_fromWk, subst_subst, subst_id'
+--   ]
+--   ext k; cases k using Fin.elim1
+--   simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero,
+--     List.getElem_cons_zero, Set.mem_setOf_eq, Subst.Eqv.get_comp, Subst.Eqv.get_fromWk,
+--     Fin.zero_eta, Fin.coe_fin_one, id_eq, subst_var, List.length_cons, subst0_get_zero,
+--      wk_res_self,
+--     Subst.Eqv.get_id, Ctx.Pure.packE]
+--   induction Γ with
+--   | nil => apply Eqv.terminal
+--   | cons V Γ I =>
+--     simp [Eqv.pack, subst_var]
+--     convert Eqv.Pure.pair_eta ⟨var 0 Ctx.Var.shead, rfl⟩
+--     simp only [wk_eff_self]
+--     sorry
+
 -- theorem Eqv.unpack0_eq_unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) :
 --   Eqv.unpack0 (φ := φ) (Δ := Δ) (e := e) i = Eqv.unpack0' i := by
 --   cases Γ with

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -713,6 +713,14 @@ theorem Subst.Eqv.get_comp {σ : Subst.Eqv φ Γ Δ} {τ : Subst.Eqv φ Δ Ξ} {
   induction τ using Quotient.inductionOn
   rfl
 
+@[simp]
+theorem Subst.Eqv.get_id {i : Fin Δ.length}
+  : (Subst.Eqv.id : Subst.Eqv φ Δ Δ).get i = Eqv.var i (by simp) := rfl
+
+@[simp]
+theorem Subst.Eqv.get_fromWk {ρ : Γ.InS Δ} {i : Fin Δ.length}
+  : (Subst.Eqv.fromWk ρ).get i = Eqv.var (φ := φ) (ρ.val i) (ρ.prop i i.prop) := rfl
+
 @[simp]
 theorem Eqv.subst_op {σ : Subst.Eqv φ Γ Δ} {a : Eqv φ Δ ⟨A, e⟩} {f : φ} {hf : Φ.EFn f A B e}
   : subst σ (op f hf a) = op f hf (subst σ a) := by
@@ -794,6 +802,12 @@ def Eqv.subst0 (a : Eqv φ Δ V) : Subst.Eqv φ Δ (V::Δ)
 @[simp]
 theorem Eqv.subst0_quot {a : InS φ Δ V} : subst0 ⟦a⟧ = ⟦a.subst0⟧ := rfl
 
+@[simp]
+theorem Eqv.subst0_get_zero {a : Eqv φ Δ V}
+  : (subst0 a).get (0 : Fin (Δ.length + 1)) = (a : Eqv φ Δ V) := by
+  induction a using Quotient.inductionOn
+  rfl
+
 @[simp]
 theorem Eqv.subst0_wk0 {a : Eqv φ Γ V} {b : Eqv φ Γ V'} : a.wk0.subst b.subst0 = a := by
   induction a using Quotient.inductionOn;

DeBruijnSSA/BinSyntax/Typing/Ctx.lean

@@ -49,6 +49,7 @@ theorem Var.head (h : V ≤ V') (Γ : Ctx α ε) : Var (V::Γ) 0 V' where
   length := by simp
   getElem := h
 
+@[simp]
 theorem Var.refl {Γ : Ctx α ε} {n} (h : n < Γ.length) : Var Γ n Γ[n] := ⟨h, le_refl _⟩
 
 @[simp]
@@ -849,6 +850,8 @@ theorem Pure.sup_effect {Γ : Ctx α ε} : Pure Γ → Γ.sup_effect = ⊥ := Pu
 
 theorem Pure.of_sup_effect {Γ : Ctx α ε} : Γ.sup_effect = ⊥ → Pure Γ := Pure.sup_effect_iff.mpr
 
+theorem Pure.sup_le {Γ : Ctx α ε} (h : Pure Γ) : Γ.sup_effect ≤ e := by simp [h.sup_effect]
+
 end SemilatticeSup
 
 end Ctx

DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean

@@ -16,7 +16,7 @@ def pack : ℕ → Term φ
   | 0 => unit
   | n + 1 => pair (var 0) (pack n).wk0
 
-theorem Wf.pack {Γ Δ : Ctx α ε}
+theorem Wf.pack_append_sup {Γ Δ : Ctx α ε}
   : Wf (φ := φ) (Γ ++ Δ) (pack Γ.length) (Γ.pack, Γ.sup_effect) := by
   induction Γ with
   | nil => exact Wf.unit _
@@ -31,32 +31,30 @@ theorem Wf.pack {Γ Δ : Ctx α ε}
     apply Wf.wk_eff _ I
     simp
 
-theorem Wf.pack' {Γ : Ctx α ε}
+theorem Wf.pack_sup {Γ : Ctx α ε}
   : Wf (φ := φ) Γ (Term.pack Γ.length) (Γ.pack, Γ.sup_effect) :=
-  by convert Wf.pack (Δ := []); simp
+  by convert Wf.pack_append_sup (Δ := []); simp
 
-def InS.pack' {Γ : Ctx α ε} : InS φ Γ (Γ.pack, Γ.sup_effect) := match Γ with
-  | [] => unit ⊥
-  | V::Γ => pair (var 0 (by cases V; simp)) ((pack' (Γ := Γ)).wk0.wk_eff (by simp))
+def InS.pack {Γ : Ctx α ε} (h : ∀i, Γ.effect i ≤ e) : InS φ Γ (Γ.pack, e) := match Γ with
+  | [] => unit e
+  | V::Γ => pair
+    (var 0 (Ctx.Var.head (by constructor; rfl; convert (h 0); simp) _))
+    ((pack (Γ := Γ) (λi => by convert h (i + 1) using 1; simp)).wk0)
 
 @[simp]
-theorem InS.coe_pack' {Γ : Ctx α ε} : (InS.pack' (φ := φ) (Γ := Γ) : Term φ) = Term.pack Γ.length
+theorem InS.coe_pack {Γ : Ctx α ε} {h}
+  : (InS.pack (φ := φ) (Γ := Γ) (e := e) h : Term φ) = Term.pack Γ.length
   := by induction Γ with
   | nil => rfl
-  | cons => simp [pack', Term.pack, *]
+  | cons => simp [pack, Term.pack, *]
 
-def _root_.BinSyntax.Ctx.Pure.pack' {Γ : Ctx α ε} (h : Γ.Pure) : InS φ Γ (Γ.pack, ⊥) := match Γ with
-  | [] => InS.unit ⊥
-  | V::Γ => InS.pair (InS.var 0 (by cases V; convert h.head; simp)) h.tail.pack'.wk0
+abbrev _root_.BinSyntax.Ctx.Pure.pack {Γ : Ctx α ε} (h : Γ.Pure) : InS φ Γ (Γ.pack, ⊥)
+  := InS.pack (e := ⊥) (h := λi => by simp [h.effect i])
 
 @[simp]
-theorem InS.coe_pure_pack {Γ : Ctx α ε} {h : Γ.Pure}
-  : (h.pack' (φ := φ) : Term φ) = Term.pack Γ.length := by induction Γ with
-  | nil => rfl
-  | cons => simp [Term.pack, Ctx.Pure.pack', *]
-
-theorem InS.wk_eff_coe_pure' {Γ : Ctx α ε} {h : Γ.Pure}
-  : (h.pack' (φ := φ)).wk_eff bot_le = pack' := by ext; simp
+theorem InS.wk_eff_pack {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ lo} {h' : lo ≤ hi}
+  : (pack (φ := φ) h).wk_eff h' = pack (λi => (h i).trans h') := by
+  ext; simp
 
 def unpack0 (x : ℕ) : Term φ := pl (pr^[x] (var 0))
 
@@ -141,12 +139,67 @@ theorem InS.pl_pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length}
 theorem InS.coe_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length}
   : (InS.unpack0 (φ := φ) (Δ := Δ) (e := e) i : Term φ) = Term.unpack0 i := rfl
 
+def unpack0' (n : ℕ) (i : ℕ) : Term φ := match n with
+| 0 => unit
+| n + 1 => let2 (var 0) (match i with | 0 => var 1 | i + 1 => unpack0' n i)
+
+theorem Wf.unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length)
+  : Wf (φ := φ) ((Γ.pack, ⊥)::Δ) (unpack0' Γ.length i) ((Γ.get i).1, e)
+  := by induction Γ generalizing Δ with
+  | nil => exact i.elim0
+  | cons V Γ I =>
+    apply Wf.let2
+    apply Wf.var (V := (V.1.prod (Ctx.pack Γ), e)); simp [Ctx.pack]
+    cases i using Fin.cases with
+    | zero => simp
+    | succ i =>
+      simp only [List.length_cons, Fin.val_succ, List.get_eq_getElem, List.getElem_cons_succ]
+      exact I i
+
 def InS.unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : InS φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e)
   := match Γ with
   | [] => i.elim0
   | V::Γ => let2
     (var (V := (V.1.prod (Ctx.pack Γ), e)) 0 (by simp [Ctx.pack]))
-    (i.cases (var 1 (by simp)) (λi => unpack0' i))
+    (i.cases (var 1 (by simp)) (λi => unpack0' (Γ := Γ) i))
+
+@[simp]
+theorem InS.coe_unpack0' {Γ Δ : Ctx α ε} {i : Fin Γ.length}
+  : (InS.unpack0' (φ := φ) (Δ := Δ) (e := e) i : Term φ) = Term.unpack0' Γ.length i := by
+  induction Γ generalizing Δ with
+  | nil => exact i.elim0
+  | cons V Γ I =>
+    simp only [List.get_eq_getElem, List.length_cons, Set.mem_setOf_eq, unpack0', Fin.val_zero,
+      List.getElem_cons_zero, InS.coe_let2, coe_var, Term.unpack0', let2.injEq, true_and]
+    cases i using Fin.cases with
+    | zero => rfl
+    | succ i => exact I
+
+theorem InS.unpack0_zero' {Γ Δ : Ctx α ε}
+  : InS.unpack0' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) (by simp only [List.length_cons]; exact 0)
+  = (by simp only [Ctx.pack]; apply InS.pi_l) := rfl
+
+theorem InS.unpack0_succ' {Γ Δ : Ctx α ε} {i : Fin Γ.length}
+  : InS.unpack0' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ
+  = let2
+    (var (V := (V.1.prod (Ctx.pack Γ), e)) 0 (by simp [Ctx.pack]))
+    (unpack0' (Γ := Γ) i) := rfl
+
+def Subst.unpack0 : Subst φ := λi => Term.unpack0 i
+
+theorem Subst.Wf.unpack0 {Γ Δ : Ctx α ε}
+  : Subst.Wf (φ := φ) ((Γ.pack, ⊥)::Δ) Γ Subst.unpack0 := λ_ => Term.Wf.unpack0
+
+def Subst.InS.unpack {Γ Δ : Ctx α ε} : Subst.InS φ ((Γ.pack, ⊥)::Δ) Γ := ⟨Subst.unpack0, Wf.unpack0⟩
+
+def InS.packed {Γ Δ : Ctx α ε} (a : InS φ Γ V) : InS φ ((Γ.pack, ⊥)::Δ) V
+  := a.subst Subst.InS.unpack
+
+def InS.unpacked {Γ : Ctx α ε} (a : InS φ [(Γ.pack, ⊥)] (A, e)) (h : ∀i, Γ.effect i ≤ e)
+  : InS φ Γ (A, e)
+  := let1 (pack h) (a.wk_id (by simp [Ctx.Wkn.drop]))
+
+-- TODO: version with appends? or nah?
 
 end Product