Began experimenting with term completeness

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

@@ -1,34 +1,13 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Completeness
 import DeBruijnSSA.BinSyntax.Typing.Region.Structural
 
 namespace BinSyntax
 
 variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
 
-namespace Term
-
-def Eqv.pack {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) : Eqv φ ((R.get i, ⊥)::Γ) (R.pack, ⊥) :=
-  match R with
-  | [] => i.elim0
-  | _::R => i.cases (inl nil) (λi => inr (pack R i))
-
-theorem Eqv.pack_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
-  : Eqv.pack (φ := φ) (Γ := Γ) R i = ⟦Term.InS.pack0 R i⟧ := by
-  induction R generalizing Γ with
-  | nil => exact i.elim0
-  | cons _ _ I =>
-    cases i using Fin.cases with
-    | zero => rfl
-    | succ i =>
-      simp only [pack, I, inr_quot, Fin.cases_succ]
-      apply congrArg
-      ext
-      simp [Term.pack0, Term.Wf.pack0, -Function.iterate_succ, Function.iterate_succ']
-
-end Term
-
 namespace Region
 
 def Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Eqv φ ((R.pack, ⊥)::Γ) R :=
@@ -77,27 +56,28 @@ def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R [R.pack] :
 @[simp]
 theorem Subst.Eqv.pack_get {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
   : (Subst.Eqv.pack (φ := φ) (Γ := Γ) (R := R)).get i
-  = Eqv.br 0 (Term.Eqv.pack R i) LCtx.Trg.shead := by rw [pack, Term.Eqv.pack_def]; rfl
+  = Eqv.br 0 (Term.Eqv.pack_sum R i) LCtx.Trg.shead := by rw [pack, Term.Eqv.pack_sum_def]; rfl
 
 @[simp]
 theorem Subst.Eqv.vlift_pack {Γ : Ctx α ε} {R : LCtx α}
   : (pack (φ := φ) (Γ := Γ) (R := R)).vlift (head := head) = pack
   := by simp only [pack, vlift_quot, Subst.InS.vlift_pack]
 
 theorem Eqv.vsubst0_pack_unpack {Γ : Ctx α ε} {R : LCtx α} {ℓ : Fin R.length}
-  : (unpack (φ := φ) (Γ := _::Γ) (R := R)).vsubst (Term.Eqv.pack R ℓ).subst0
+  : (unpack (φ := φ) (Γ := _::Γ) (R := R)).vsubst (Term.Eqv.pack_sum R ℓ).subst0
   = br ℓ (Term.Eqv.var 0 Ctx.Var.shead) (by simp) := by
   induction R with
   | nil => exact ℓ.elim0
   | cons _ _ I =>
     cases ℓ using Fin.cases with
     | zero =>
-      simp only [Term.Eqv.pack, Fin.val_succ, Fin.cases_zero, unpack, coprod, vsubst_case,
+      simp only [Term.Eqv.pack_sum, Fin.val_succ, Fin.cases_zero, unpack, coprod, vsubst_case,
         Term.Eqv.var0_subst0, Term.Eqv.wk_res_self, case_inl, let1_beta]
       rfl
     | succ ℓ =>
-      simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ,
-        LCtx.pack.eq_2, Term.Eqv.pack, Fin.val_zero, List.getElem_cons_zero, Fin.cases_succ, unpack,
+      simp only [
+        List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, unpack,
+        LCtx.pack.eq_2, Term.Eqv.pack_sum, Fin.val_zero, List.getElem_cons_zero, Fin.cases_succ,
         coprod, vwk1_quot, InS.nil_vwk1, vwk1_lwk0, vwk1_unpack, vsubst_case, Term.Eqv.var0_subst0,
         Fin.zero_eta, Term.Eqv.wk_res_self, vsubst_lwk0, vsubst_lift_unpack, case_inr, let1_beta, I]
       rfl

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

@@ -0,0 +1,54 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Seq
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum
+import DeBruijnSSA.BinSyntax.Typing.Region.Structural
+
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Term
+
+def Eqv.pack_sum {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) : Eqv φ ((R.get i, ⊥)::Γ) (R.pack, ⊥)
+  := match R with
+  | [] => i.elim0
+  | _::R => i.cases (inl nil) (λi => inr (pack_sum R i))
+
+theorem Eqv.pack_sum_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  : Eqv.pack_sum (φ := φ) (Γ := Γ) R i = ⟦Term.InS.pack0 R i⟧ := by
+  induction R generalizing Γ with
+  | nil => exact i.elim0
+  | cons _ _ I =>
+    cases i using Fin.cases with
+    | zero => rfl
+    | succ i =>
+      simp only [pack_sum, I, inr_quot, Fin.cases_succ]
+      apply congrArg
+      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))
+
+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
+
+def Eqv.unpack {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Eqv φ ((Γ.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 => unpack i))
+
+-- TODO: wk lift unpack
+
+-- TODO: let1 pack (unpack i) = var i
+
+-- TODO: need InS version for this... :(
+
+-- def Subst.Eqv.unpacked {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Subst.Eqv φ ((Γ.pack, ⊥)::Δ) Γ
+--   := sorry
+
+end Term

DeBruijnSSA/BinSyntax/Typing/Ctx.lean

@@ -718,6 +718,58 @@ theorem effect_append_bot₂ {left right : Ty α} {tail : Ctx α ε}
   : effect (⟨left, ⊥⟩::⟨right, ⊥⟩::tail) = Nat.liftnBot 2 tail.effect
   := by simp only [effect_append_bot, Nat.liftnBot_two_apply]
 
+theorem effect_tail {Γ : Ctx α ε} (i : ℕ)
+  : effect (Γ.tail) i = Γ.effect (i + 1) := by cases Γ <;> simp [effect]
+
+theorem effect_cons_match {head} {Γ : Ctx α ε} (i : ℕ)
+  : effect (head::Γ) i = match i with | 0 => head.2 | i + 1 => Γ.effect i := by
+  cases i <;> simp [effect]
+
+@[simp]
+theorem effect_cons_zero {head} {Γ : Ctx α ε}
+  : effect (head::Γ) 0 = head.2 := by simp [effect_cons_match]
+
+@[simp]
+theorem effect_cons_succ {head} {Γ : Ctx α ε} (i : ℕ)
+  : effect (head::Γ) (i + 1) = Γ.effect i := by simp [effect_cons_match]
+
+@[simp]
+theorem effect_empty : effect (α := α) (ε := ε) [] = ⊥ := by funext i; simp [effect]
+
+def pack : Ctx α ε → Ty α
+  | [] => Ty.unit
+  | V::Γ => V.1.prod (pack Γ)
+
+def Pure (Γ : Ctx α ε) : Prop := Γ.effect = ⊥
+
+theorem pure_def {Γ : Ctx α ε} : Pure Γ ↔ Γ.effect = ⊥ := Iff.rfl
+
+theorem Pure.effect {Γ : Ctx α ε} (h : Pure Γ) (i : ℕ) : Γ.effect i = ⊥
+  := by rw [h]; rfl
+
+theorem Pure.of_effect' {Γ : Ctx α ε} (h : Γ.effect = ⊥) : Pure Γ := h
+
+theorem Pure.of_effect {Γ : Ctx α ε} (h : ∀i, Γ.effect i = ⊥) : Pure Γ := funext h
+
+theorem Pure.effect' {Γ : Ctx α ε} (h : Pure Γ) : Γ.effect = ⊥ := h
+
+theorem Pure.nil : Pure (α := α) (ε := ε) [] := by simp [Pure]
+
+theorem Pure.cons {head} {Γ : Ctx α ε} (h : Pure Γ) : Pure ((head, ⊥)::Γ) := by
+  funext k; cases k <;> simp [Pure, effect_append_bot, h.effect', Nat.liftBot]
+
+theorem Pure.cons' {head} {Γ : Ctx α ε} (h : head.2 = ⊥) (h' : Pure Γ) : Pure (head::Γ) := by
+  cases head; cases h; exact h'.cons
+
+theorem Pure.head {head} {Γ : Ctx α ε} (h : Pure (head::Γ)): head.2 = ⊥ := by
+  convert h.effect 0; simp [Ctx.effect]
+
+theorem Pure.tail {Γ : Ctx α ε} (h : Pure Γ) : Pure Γ.tail
+  := of_effect (λi => by simp [effect_tail, h.effect (i + 1)])
+
+theorem Pure.cons_iff {head} {Γ : Ctx α ε} : Pure (head::Γ) ↔ head.2 = ⊥ ∧ Pure Γ
+  := ⟨λh => ⟨h.head, h.tail⟩, λ⟨h, h'⟩ => h'.cons' h⟩
+
 variable [PartialOrder α] [PartialOrder ε]
 
 theorem Wkn.effect {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ ρ) (i : ℕ) (hi : i < Δ.length)
@@ -733,7 +785,6 @@ theorem Var.toEffect {Γ : Ctx α ε} {n : ℕ} {V} (h : Γ.Var n V)
     exact h.get.1
     simp [effect, h.length]
   ⟩
-
 -- def WknTy (Γ Δ : Ctx α ε) (ρ : ℕ → ℕ) : Prop := Γ.Types.NWkn Δ.Types ρ
 
 -- theorem WknTy.id_types_len_le {Γ Δ : Ctx α ε}
@@ -761,4 +812,28 @@ theorem IsInitial.wk {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ ρ) :
 
 end OrderBot
 
+section SemilatticeSup
+
+variable [Φ: EffInstSet φ (Ty α) ε] [SemilatticeSup ε] [OrderBot ε]
+
+@[simp]
+def sup_effect : Ctx α ε → ε
+  | [] => ⊥
+  | V::Γ => V.2 ⊔ sup_effect Γ
+
+theorem effect_le_sup_effect {Γ : Ctx α ε} (i : ℕ) : Γ.effect i ≤ sup_effect Γ
+  := by induction Γ generalizing i with
+    | nil => simp [effect, sup_effect]
+    | cons V Γ ih =>
+      cases i with | zero => simp | succ i => exact le_sup_of_le_right (by simp [ih i])
+
+theorem Pure.sup_effect_iff {Γ : Ctx α ε} : Pure Γ ↔ Γ.sup_effect = ⊥
+  := by induction Γ <;> simp [nil, cons_iff, *]
+
+theorem Pure.sup_effect {Γ : Ctx α ε} : Pure Γ → Γ.sup_effect = ⊥ := Pure.sup_effect_iff.mp
+
+theorem Pure.of_sup_effect {Γ : Ctx α ε} : Γ.sup_effect = ⊥ → Pure Γ := Pure.sup_effect_iff.mpr
+
+end SemilatticeSup
+
 end Ctx