Structural stuff is nary stuff

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

@@ -1,126 +1 @@
-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.Structural
-import DeBruijnSSA.BinSyntax.Typing.Region.Structural
-
-namespace BinSyntax
-
-variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
-
-namespace Region
-
-def Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Eqv φ ((R.pack, ⊥)::Γ) R :=
-  match R with
-  | [] => loop
-  | _::_ => coprod nil unpack.lwk0
-
-theorem Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
-  : Eqv.unpack (φ := φ) (Γ := Γ) (R := R) = ⟦InS.unpack (Γ := Γ) (R := R)⟧ := by induction R with
-  | nil => rw [unpack, loop_def]; rfl
-  | cons _ _ I =>
-    rw [unpack, nil, I, lwk0_quot]
-    apply Eqv.eq_of_reg_eq
-    simp [
-      Region.unpack, Region.nil, Region.ret, Region.lwk0, Region.vwk_lwk, Region.vwk_lift_unpack]
-
-@[simp]
-theorem Eqv.vwk_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (ρ : Γ.InS Δ)
-  : Eqv.vwk (ρ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = unpack := by
-  rw [unpack_def, vwk_quot, unpack_def]
-  apply Eqv.eq_of_reg_eq
-  simp
-
-@[simp]
-theorem Eqv.vwk1_unpack {Γ : Ctx α ε} {R : LCtx α}
-  : (Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).vwk1 (inserted := inserted) = unpack := by
-  rw [vwk1, <-Ctx.InS.lift_wk0, vwk_lift_unpack]
-
-@[simp]
-theorem Eqv.vsubst_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Subst.Eqv φ Γ Δ)
-  : Eqv.vsubst (σ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = Eqv.unpack := by
-  induction σ using Quotient.inductionOn
-  rw [unpack_def, Term.Subst.Eqv.lift_quot, vsubst_quot, unpack_def]
-  apply Eqv.eq_of_reg_eq
-  simp
-
-def Subst.Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ [R.pack] R
-  := Region.Eqv.unpack.csubst
-
-theorem Subst.Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
-  : Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R) = ⟦InS.unpack (Γ := Γ) (R := R)⟧
-  := by rw [unpack, Region.Eqv.unpack_def]; rfl
-
-def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R [R.pack] := ⟦Subst.InS.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_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_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_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, 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
-
-theorem Subst.Eqv.unpack_comp_pack {Γ : Ctx α ε} {R : LCtx α}
-  : Subst.Eqv.unpack.comp Subst.Eqv.pack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := R)
-  := by ext ℓ; simp [get_comp, pack_get, get_id, unpack, Eqv.csubst_get, Eqv.vsubst0_pack_unpack]
-
--- theorem Eqv.lsubst_pack_unpack {Γ : Ctx α ε} {R : LCtx α}
---   : (unpack (φ := φ) (Γ := Γ) (R := R)).lsubst Subst.Eqv.pack
---   = nil := by
---   induction R with
---   | nil =>
---     apply Eqv.initial
---     sorry -- TODO: context containing empty is trivially initial, add simp lemmas...
---   | cons A R I =>
---     simp only [LCtx.pack.eq_2, unpack, coprod, vwk1_quot, InS.nil_vwk1, vwk1_lwk0, vwk1_unpack,
---       lsubst_case, Subst.Eqv.vlift_pack]
---     apply Eq.trans _ Eqv.sum_nil
---     simp only [sum, coprod]
---     congr
---     -- TODO: lsubst pack lwk0 is lsubst pack ;; inj_r; then follows by induction
---     sorry
-
--- theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
---   : Subst.Eqv.pack.comp Subst.Eqv.unpack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := [R.pack]) := by
---   ext ℓ
---   induction ℓ using Fin.elim1
---   simp only [unpack, get_comp, vlift_pack, Eqv.csubst_get, Eqv.cast_rfl, Eqv.lsubst_pack_unpack,
---     get_id, Fin.coe_fin_one]
---   rfl
-
-def Eqv.unpacked {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ [R.pack]) : Eqv φ Γ R
-  := h.lsubst Subst.Eqv.unpack
-
-def Eqv.packed {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ [R.pack]
-  := h.lsubst Subst.Eqv.pack
-
--- theorem Eqv.unpacked_packed {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R)
---   : h.packed.unpacked = h := by
---   rw [Eqv.unpacked, packed, lsubst_lsubst, Subst.Eqv.unpack_comp_pack]
---   sorry
-
-end Region
-
-end BinSyntax
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Basic

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

@@ -0,0 +1,24 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Product
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+def Eqv.packed {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ Γ R) : Eqv φ [(Γ.pack, ⊥)] [R.pack]
+  := r.packed_out.packed_in
+
+def Eqv.unpacked {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ [(Γ.pack, ⊥)] [R.pack]) (h : Γ.Pure)
+  : Eqv φ Γ R := r.unpacked_out.unpacked_in h
+
+-- TODO: (un)packed_in commutes with (un)packed_out
+
+-- TODO: packed_unpacked, unpacked_packed
+
+-- TODO: {br, let1, let2, case, cfg}
+
+end Region
+
+end BinSyntax

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

@@ -0,0 +1,39 @@
+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.Structural.Product
+import DeBruijnSSA.BinSyntax.Typing.Region.Structural
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+def Eqv.unpacked_in {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ [(Γ.pack, ⊥)] R) (h : Γ.Pure) : Eqv φ Γ R
+  := let1 h.packE (r.vwk_id (by simp [Ctx.Wkn.drop]))
+
+theorem Eqv.unpacked_in_def' {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ [(Γ.pack, ⊥)] R} {h : Γ.Pure}
+  : r.unpacked_in (φ := φ) (Γ := Γ) h = r.vsubst h.packSE := by
+  rw [unpacked_in, let1_beta, vwk_id_eq_vwk, <-vsubst_fromWk, vsubst_vsubst]
+  congr
+  ext k; cases k using Fin.elim1
+  simp [Term.Subst.Eqv.get_comp]
+
+def Eqv.packed_in {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ Γ R) : Eqv φ [(Γ.pack, ⊥)] R
+  := r.vsubst Term.Subst.Eqv.unpack
+
+theorem Eqv.unpacked_in_packed_in {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R} {h : Γ.Pure}
+  : r.packed_in.unpacked_in h = r := by
+  rw [unpacked_in_def', packed_in, vsubst_vsubst, Term.Subst.Eqv.packSE_comp_unpack, vsubst_id]
+
+theorem Eqv.packed_in_unpacked_in
+  {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ [(Γ.pack, ⊥)] R} {h : Γ.Pure}
+  : (r.unpacked_in h).packed_in = r := by
+  rw [unpacked_in_def', packed_in, vsubst_vsubst, Term.Subst.Eqv.unpack_comp_packSE, vsubst_id]
+
+-- TODO: {br, let1, let2, case, cfg}
+
+end Region
+
+end BinSyntax

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

@@ -0,0 +1,130 @@
+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.Structural.Sum
+import DeBruijnSSA.BinSyntax.Typing.Region.Structural
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+def Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Eqv φ ((R.pack, ⊥)::Γ) R :=
+  match R with
+  | [] => loop
+  | _::_ => coprod nil unpack.lwk0
+
+theorem Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
+  : Eqv.unpack (φ := φ) (Γ := Γ) (R := R) = ⟦InS.unpack (Γ := Γ) (R := R)⟧ := by induction R with
+  | nil => rw [unpack, loop_def]; rfl
+  | cons _ _ I =>
+    rw [unpack, nil, I, lwk0_quot]
+    apply Eqv.eq_of_reg_eq
+    simp [
+      Region.unpack, Region.nil, Region.ret, Region.lwk0, Region.vwk_lwk, Region.vwk_lift_unpack]
+
+@[simp]
+theorem Eqv.vwk_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (ρ : Γ.InS Δ)
+  : Eqv.vwk (ρ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = unpack := by
+  rw [unpack_def, vwk_quot, unpack_def]
+  apply Eqv.eq_of_reg_eq
+  simp
+
+@[simp]
+theorem Eqv.vwk1_unpack {Γ : Ctx α ε} {R : LCtx α}
+  : (Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).vwk1 (inserted := inserted) = unpack := by
+  rw [vwk1, <-Ctx.InS.lift_wk0, vwk_lift_unpack]
+
+@[simp]
+theorem Eqv.vsubst_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Subst.Eqv φ Γ Δ)
+  : Eqv.vsubst (σ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = Eqv.unpack := by
+  induction σ using Quotient.inductionOn
+  rw [unpack_def, Term.Subst.Eqv.lift_quot, vsubst_quot, unpack_def]
+  apply Eqv.eq_of_reg_eq
+  simp
+
+def Subst.Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ [R.pack] R
+  := Region.Eqv.unpack.csubst
+
+theorem Subst.Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
+  : Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R) = ⟦InS.unpack (Γ := Γ) (R := R)⟧
+  := by rw [unpack, Region.Eqv.unpack_def]; rfl
+
+def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R [R.pack] := ⟦Subst.InS.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.inj_n R i) LCtx.Trg.shead := by rw [pack, Term.Eqv.inj_n_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.inj_n 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.inj_n, 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, unpack,
+        LCtx.pack.eq_2, Term.Eqv.inj_n, 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
+
+theorem Subst.Eqv.unpack_comp_pack {Γ : Ctx α ε} {R : LCtx α}
+  : Subst.Eqv.unpack.comp Subst.Eqv.pack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := R)
+  := by ext ℓ; simp [get_comp, pack_get, get_id, unpack, Eqv.csubst_get, Eqv.vsubst0_pack_unpack]
+
+-- theorem Eqv.lsubst_pack_unpack {Γ : Ctx α ε} {R : LCtx α}
+--   : (unpack (φ := φ) (Γ := Γ) (R := R)).lsubst Subst.Eqv.pack
+--   = nil := by
+--   induction R with
+--   | nil =>
+--     apply Eqv.initial
+--     sorry -- TODO: context containing empty is trivially initial, add simp lemmas...
+--   | cons A R I =>
+--     simp only [LCtx.pack.eq_2, unpack, coprod, vwk1_quot, InS.nil_vwk1, vwk1_lwk0, vwk1_unpack,
+--       lsubst_case, Subst.Eqv.vlift_pack]
+--     apply Eq.trans _ Eqv.sum_nil
+--     simp only [sum, coprod]
+--     congr
+--     -- TODO: lsubst pack lwk0 is lsubst pack ;; inj_r; then follows by induction
+--     sorry
+
+-- theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
+--   : Subst.Eqv.pack.comp Subst.Eqv.unpack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := [R.pack]) := by
+--   ext ℓ
+--   induction ℓ using Fin.elim1
+--   simp only [unpack, get_comp, vlift_pack, Eqv.csubst_get, Eqv.cast_rfl, Eqv.lsubst_pack_unpack,
+--     get_id, Fin.coe_fin_one]
+--   rfl
+
+def Eqv.unpacked_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ [R.pack]) : Eqv φ Γ R
+  := h.lsubst Subst.Eqv.unpack
+
+def Eqv.packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ [R.pack]
+  := h.lsubst Subst.Eqv.pack
+
+-- theorem Eqv.unpacked_out_packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R)
+--   : h.packed_out.unpacked_out = h := by
+--   rw [Eqv.unpacked, packed, lsubst_lsubst, Subst.Eqv.unpack_comp_pack]
+--   sorry
+
+-- TODO: packed_out_unpacked_out
+
+-- TODO: {br, let1, let2, case, cfg}
+
+end Region
+
+end BinSyntax

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -429,7 +429,9 @@ theorem InS.vwk_id_q {Γ Δ : Ctx α ε} {L : LCtx α} {r : InS φ Δ L}
 theorem Eqv.vwk_id_quot {Γ Δ : Ctx α ε} {L : LCtx α} {r : InS φ Δ L}
   (hρ : Γ.Wkn Δ id) : Eqv.vwk_id hρ ⟦r⟧ = ⟦r.vwk_id hρ⟧ := rfl
 
-
+theorem Eqv.vwk_id_eq_vwk {Γ Δ : Ctx α ε} {L : LCtx α} {r : Eqv φ Δ L}
+  (hρ : Γ.Wkn Δ id) : Eqv.vwk_id hρ r = r.vwk ⟨id, hρ⟩ := by
+  induction r using Quotient.inductionOn; simp [InS.vwk_id_eq_vwk]
 
 @[simp]
 theorem Eqv.vwk_id_eq
@@ -581,6 +583,14 @@ theorem InS.vsubst_q {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.InS φ 
 theorem Eqv.vsubst_quot {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.InS φ Γ Δ} {r : InS φ Δ L}
    : Eqv.vsubst ⟦σ⟧ ⟦r⟧ = ⟦r.vsubst σ⟧ := rfl
 
+@[simp]
+theorem Eqv.vsubst_id {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ Γ L}
+  : Eqv.vsubst Term.Subst.Eqv.id r = r := by
+  induction r using Quotient.inductionOn; simp [Term.Subst.Eqv.id]
+
+theorem Eqv.vsubst_id' {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ Γ L} {σ : Term.Subst.Eqv φ Γ Γ}
+  (h : σ = Term.Subst.Eqv.id) : Eqv.vsubst σ r = r := by simp [h]
+
 theorem Eqv.vsubst_vsubst {Γ Δ Ξ : Ctx α ε} {L : LCtx α} {r : Eqv φ Ξ L}
   {σ : Term.Subst.Eqv φ Γ Δ} {τ : Term.Subst.Eqv φ Δ Ξ}
   : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by
@@ -593,6 +603,9 @@ theorem Eqv.vsubst_toSubst {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {L} {r : Eqv φ
   : r.vsubst ⟦ρ.toSubst⟧ = r.vwk ρ
   := by induction r using Quotient.inductionOn; simp [InS.vsubst_toSubst]
 
+theorem Eqv.vsubst_fromWk {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {r : Eqv φ Δ L}
+  : r.vsubst (Term.Subst.Eqv.fromWk ρ) = r.vwk ρ := vsubst_toSubst
+
 @[simp]
 theorem Eqv.vsubst_br {Γ : Ctx α ε} {L : LCtx α}
   {σ : Term.Subst.Eqv φ Γ Δ} {ℓ} {a : Term.Eqv φ Δ ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A}