Skip to content

Commit

Permalink
Generalized unpack_out
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem committed Sep 28, 2024
1 parent 7784fc3 commit 3810d92
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 50 deletions.
10 changes: 5 additions & 5 deletions DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ namespace Region

theorem Eqv.packed_br_den {Γ : Ctx α ε} {L : LCtx α}
{ℓ} {a : Term.Eqv φ Γ (A, ⊥)} {hℓ}
: (br (L := L) ℓ a hℓ).packed (Δ := Δ)
: (br (L := L) ℓ a hℓ).packed (L := L) (Δ := Δ)
= ret ((a.packed.wk_res ⟨hℓ.get, by rfl⟩)) ;; ret (Term.Eqv.inj_n _ ⟨ℓ, hℓ.length⟩) := by
rw [<-ret_of_seq, Term.Eqv.seq_inj_n, packed_br]

theorem Eqv.packed_let1_den {Γ : Ctx α ε} {R : LCtx α}
{a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) R}
: (let1 a r).packed (Δ := Δ)
: (let1 a r).packed (L := L) (Δ := Δ)
= ret Term.Eqv.split ;; _ ⋊ lret a.packed ;; r.packed := by
rw [<-lret_rtimes, ret_seq, lret]
simp only [Term.Eqv.rtimes, Term.Eqv.tensor, Term.Eqv.wk1_nil, Term.Eqv.wk1_packed, let1_let2,
Expand Down Expand Up @@ -68,7 +68,7 @@ theorem Eqv.packed_let1_den {Γ : Ctx α ε} {R : LCtx α}

theorem Eqv.packed_let2_den {Γ : Ctx α ε} {R : LCtx α}
{a : Term.Eqv φ Γ (A.prod B, e)} {r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) R}
: (let2 a r).packed (Δ := Δ)
: (let2 a r).packed (L := L) (Δ := Δ)
= ret Term.Eqv.split ;; _ ⋊ lret a.packed ;; assoc_inv ;; r.packed := by
rw [ret_seq_rtimes]
simp only [
Expand Down Expand Up @@ -110,7 +110,7 @@ theorem Eqv.packed_let2_den {Γ : Ctx α ε} {R : LCtx α}

theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α}
{a : Term.Eqv φ Γ (A.coprod B, e)} {r : Eqv φ ((A, ⊥)::Γ) R} {s : Eqv φ ((B, ⊥)::Γ) R}
: (case a r s).packed (Δ := Δ)
: (case a r s).packed (L := L) (Δ := Δ)
= ret Term.Eqv.split ;; _ ⋊ lret a.packed ;; distl_inv ;; coprod r.packed s.packed := by
rw [ret_seq_rtimes, Term.Eqv.split, let2_pair]
simp only [Term.Eqv.nil, Term.Eqv.wk0_var, zero_add, lret, vwk1_let1, Term.Eqv.wk1_packed,
Expand Down Expand Up @@ -192,7 +192,7 @@ theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α}
rfl

theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
: (cfg R β G).packed (Δ := Δ)
: (cfg R β G).packed (L := []) (Δ := Δ)
= (ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv ;; sum pi_r nil)
;; coprod nil (
fixpoint (
Expand Down
30 changes: 16 additions & 14 deletions DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O

namespace Region

def Eqv.packed {Γ Δ : Ctx α ε} {R : LCtx α} (r : Eqv φ Γ R) : Eqv φ ((Γ.pack, ⊥)::Δ) [R.pack]
def Eqv.packed {Γ Δ : Ctx α ε} {R : LCtx α} (r : Eqv φ Γ R) : Eqv φ ((Γ.pack, ⊥)::Δ) (R.pack::L)
:= r.packed_out.packed_in

def Eqv.unpacked {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ [(Γ.pack, ⊥)] [R.pack]) (h : Γ.Pure)
Expand All @@ -33,13 +33,15 @@ theorem Eqv.unpacked_out_packed_in {Γ : Ctx α ε} {R : LCtx α}
Term.Subst.Eqv.unpack, Subst.Eqv.vsubst_quot]
congr; ext; simp

-- TODO: generalize these to arbitrary L

theorem Eqv.packed_out_unpacked_in {Γ : Ctx α ε} {R : LCtx α}
{r : Eqv φ [(Γ.pack, ⊥)] R} {h : Γ.Pure}
: (r.unpacked_in h).packed_out = r.packed_out.unpacked_in h := by
: (r.unpacked_in h).packed_out (L := []) = r.packed_out.unpacked_in h := by
apply unpacked_out_injective; simp [unpacked_out_unpacked_in]

theorem Eqv.packed_out_packed_in {Γ : Ctx α ε} {R : LCtx α}
{r : Eqv φ Γ R} : r.packed_in.packed_out = r.packed_out.packed_in (Δ := Δ) := by
{r : Eqv φ Γ R} : r.packed_in.packed_out (L := []) = r.packed_out.packed_in (Δ := Δ) := by
apply unpacked_out_injective; simp [unpacked_out_packed_in]

theorem Eqv.packed_in_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α}
Expand All @@ -48,7 +50,7 @@ theorem Eqv.packed_in_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α}
simp [unpacked_app_out, packed_in, vsubst_lsubst, unpacked_app_out]

theorem Eqv.packed_def' {Γ : Ctx α ε} {R : LCtx α}
{r : Eqv φ Γ R} : r.packed (Δ := Δ) = r.packed_in.packed_out
{r : Eqv φ Γ R} : r.packed (Δ := Δ) = r.packed_in.packed_out (L := [])
:= by simp [packed, packed_out_packed_in]

theorem Eqv.unpacked_def' {Γ : Ctx α ε} {R : LCtx α}
Expand All @@ -65,62 +67,62 @@ theorem Eqv.unpacked_packed {Γ : Ctx α ε} {R : LCtx α}

@[simp]
theorem Eqv.vwk_slift_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R} {ρ : Δ'.InS Δ}
: r.packed.vwk ρ.slift = r.packed (Δ := Δ') := by simp [packed]
: r.packed.vwk ρ.slift = r.packed (L := L) (Δ := Δ') := by simp [packed]

@[simp]
theorem Eqv.vwk_liftn₂_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R} {ρ : Δ'.InS Δ}
: r.packed.vwk (ρ.liftn₂ (le_refl _) (le_refl V)) = r.packed (Δ := _::Δ') := by
: r.packed.vwk (ρ.liftn₂ (le_refl _) (le_refl V)) = r.packed (L := L) (Δ := _::Δ') := by
simp [<-Ctx.InS.lift_lift]

@[simp]
theorem Eqv.vwk1_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
: r.packed.vwk1 (inserted := inserted) = r.packed (Δ := _::Δ) := by
: r.packed.vwk1 (inserted := inserted) = r.packed (L := L) (Δ := _::Δ) := by
rw [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_packed]

@[simp]
theorem Eqv.vwk2_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
: r.packed.vwk2 (inserted := inserted) = r.packed (Δ := head::_::Δ) := by
: r.packed.vwk2 (inserted := inserted) = r.packed (L := L) (Δ := head::_::Δ) := by
rw [vwk2, <-Ctx.InS.lift_wk1, vwk_slift_packed]

@[simp]
theorem Eqv.vsubst_lift_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
{σ : Term.Subst.Eqv φ Δ' Δ}
: r.packed.vsubst (σ.lift (le_refl _)) = r.packed (Δ := Δ') := by
: r.packed.vsubst (σ.lift (le_refl _)) = r.packed (L := L) (Δ := Δ') := by
simp [packed]

@[simp]
theorem Eqv.vsubst_liftn₂_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
{σ : Term.Subst.Eqv φ Δ' Δ}
: r.packed.vsubst (σ.liftn₂ (le_refl _) (le_refl V)) = r.packed (Δ := _::Δ') := by
: r.packed.vsubst (σ.liftn₂ (le_refl _) (le_refl V)) = r.packed (L := L) (Δ := _::Δ') := by
simp [<-Term.Subst.Eqv.lift_lift]

open Term.Eqv

theorem Eqv.packed_br {Γ : Ctx α ε} {L : LCtx α}
{ℓ} {a : Term.Eqv φ Γ (A, ⊥)} {hℓ}
: (br (L := L) ℓ a hℓ).packed (Δ := Δ) = ret ((a.packed.wk_res ⟨hℓ.get, by rfl⟩).inj) := by
: (br (L := L) ℓ a hℓ).packed (L := L) (Δ := Δ) = ret ((a.packed.wk_res ⟨hℓ.get, by rfl⟩).inj) := by
rw [packed, packed_out_br, packed_in_br, Term.Eqv.packed_of_inj, ret]
congr
induction a using Quotient.inductionOn
apply Term.Eqv.eq_of_term_eq; rfl

theorem Eqv.packed_let1 {Γ : Ctx α ε} {R : LCtx α}
{a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) R}
: (let1 a r).packed (Δ := Δ)
: (let1 a r).packed (Δ := Δ) (L := L)
= let1 a.packed (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) r.packed) := by
rw [packed, packed_out_let1, packed_in_let1, <-packed]

theorem Eqv.packed_let2 {Γ : Ctx α ε} {R : LCtx α}
{a : Term.Eqv φ Γ (A.prod B, e)} {r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) R}
: (let2 a r).packed (Δ := Δ)
: (let2 a r).packed (Δ := Δ) (L := L)
= let2 a.packed (let1
(pair (pair (var 2 (by simp)) (var 1 (by simp))) (var 0 Ctx.Var.shead))
r.packed) := by
rw [packed, packed_out_let2, packed_in_let2, <-packed]

theorem Eqv.packed_case {Γ : Ctx α ε} {R : LCtx α}
{a : Term.Eqv φ Γ (A.coprod B, e)} {r : Eqv φ ((A, ⊥)::Γ) R} {s : Eqv φ ((B, ⊥)::Γ) R}
: (case a r s).packed (Δ := Δ)
: (case a r s).packed (Δ := Δ) (L := L)
= case a.packed
(let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) r.packed)
(let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) s.packed) := by
Expand Down
56 changes: 29 additions & 27 deletions DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,33 +182,33 @@ theorem Subst.Eqv.vsubst_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Sub
rw [unpack_def, vsubst_quot, unpack_def]
apply congrArg; ext; simp

def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R [R.pack] := ⟦Subst.InS.pack⟧
def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R (R.pack::L) := ⟦Subst.InS.pack⟧

@[simp]
theorem Subst.Eqv.pack_get {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
: (Subst.Eqv.pack (φ := φ) (Γ := Γ) (R := R)).get i
: (Subst.Eqv.pack (φ := φ) (Γ := Γ) (R := R) (L := L)).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
: (pack (φ := φ) (Γ := Γ) (R := R) (L := L)).vlift (head := head) = pack
:= by simp only [pack, vlift_quot, Subst.InS.vlift_pack]

@[simp]
theorem Subst.Eqv.vliftn₂_pack {Γ : Ctx α ε} {R : LCtx α}
: (Subst.Eqv.pack (φ := φ) (Γ := Γ) (R := R)).vliftn₂ (left := left) (right := right)
: (Subst.Eqv.pack (φ := φ) (Γ := Γ) (R := R) (L := L)).vliftn₂ (left := left) (right := right)
= pack := by simp [Subst.Eqv.vliftn₂_eq_vlift_vlift]

@[simp]
theorem Subst.Eqv.vwk_pack {Γ : Ctx α ε} {R : LCtx α} {ρ : Γ.InS Δ}
: (Subst.Eqv.pack (φ := φ) (R := R)).vwk ρ = pack := by
: (Subst.Eqv.pack (φ := φ) (R := R) (L := L)).vwk ρ = pack := by
rw [pack, vwk_quot, pack]
congr
ext; simp [Subst.pack]

@[simp]
theorem Subst.Eqv.vsubst_pack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Subst.Eqv φ Δ Γ)
: (Subst.Eqv.pack (φ := φ) (R := R)).vsubst σ = pack := by
: (Subst.Eqv.pack (φ := φ) (R := R) (L := L)).vsubst σ = pack := by
induction σ using Quotient.inductionOn
rw [pack, vsubst_quot, pack]
congr
Expand Down Expand Up @@ -264,7 +264,7 @@ theorem Eqv.unpacked_out_vsubst {Γ : Ctx α ε} {R : LCtx α} {σ : Term.Subst.
{r : Eqv φ Δ [R.pack]} : (r.vsubst σ).unpacked_out = r.unpacked_out.vsubst σ
:= vsubst_unpacked_out.symm

def Eqv.packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ [R.pack]
def Eqv.packed_out {Γ : Ctx α ε} {R L : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ (R.pack::L)
:= h.lsubst Subst.Eqv.pack

@[simp]
Expand All @@ -273,16 +273,16 @@ theorem Eqv.packed_out_quot {Γ : Ctx α ε} {R : LCtx α} (r : InS φ Γ R)

@[simp]
theorem Eqv.vwk_packed_out {Γ : Ctx α ε} {R : LCtx α} {ρ : Γ.InS Δ} {r : Eqv φ Δ R}
: r.packed_out.vwk ρ = (r.vwk ρ).packed_out := by simp [packed_out, vwk_lsubst]
: r.packed_out.vwk ρ = (r.vwk ρ).packed_out (L := L) := by simp [packed_out, vwk_lsubst]

@[simp]
theorem Eqv.vsubst_packed_out {Γ : Ctx α ε} {R : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ}
{r : Eqv φ Δ R} : r.packed_out.vsubst σ = (r.vsubst σ).packed_out := by
{r : Eqv φ Δ R} : r.packed_out.vsubst σ = (r.vsubst σ).packed_out (L := L) := by
simp [packed_out, vsubst_lsubst]

theorem Eqv.packed_out_br {Γ : Ctx α ε} {L : LCtx α}
{ℓ} {a : Term.Eqv φ Γ (A, ⊥)} {hℓ}
: (br (L := L) ℓ a hℓ).packed_out = br 0 (a.wk_res ⟨hℓ.get, by rfl⟩).inj (by simp) := by
: (br (L := L) ℓ a hℓ).packed_out (L := R) = br 0 (a.wk_res ⟨hℓ.get, by rfl⟩).inj (by simp) := by
simp [packed_out]
induction a using Quotient.inductionOn
simp only [Term.Eqv.subst0_quot, Term.Eqv.inj_n_def, List.get_eq_getElem, Term.Eqv.wk_id_quot,
Expand All @@ -293,21 +293,22 @@ theorem Eqv.packed_out_br {Γ : Ctx α ε} {L : LCtx α}

theorem Eqv.packed_out_let1 {Γ : Ctx α ε} {R : LCtx α}
(a : Term.Eqv φ Γ (A, e)) (r : Eqv φ ((A, ⊥)::Γ) R)
: (let1 a r).packed_out = let1 a r.packed_out := by simp [packed_out]
: (let1 a r).packed_out (L := L) = let1 a r.packed_out := by simp [packed_out]

theorem Eqv.packed_out_let2 {Γ : Ctx α ε} {R : LCtx α}
(a : Term.Eqv φ Γ (A.prod B, e)) (r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) R)
: (let2 a r).packed_out = let2 a r.packed_out := by simp [packed_out]
: (let2 a r).packed_out (L := L) = let2 a r.packed_out := by simp [packed_out]

theorem Eqv.packed_out_case {Γ : Ctx α ε} {R : LCtx α}
(a : Term.Eqv φ Γ (A.coprod B, e))
(l : Eqv φ ((A, ⊥)::Γ) R) (r : Eqv φ ((B, ⊥)::Γ) R)
: (case a l r).packed_out = case a l.packed_out r.packed_out := by simp [packed_out]
: (case a l r).packed_out (L := L) = case a l.packed_out r.packed_out := by simp [packed_out]

-- TODO: packing a cfg is half of Böhm–Jacopini, and I believe the best we can do sans dinaturality

theorem Eqv.packed_out_lwk0_arrow {Γ : Ctx α ε} {R : LCtx α}
(r : Eqv φ ((A, ⊥)::Γ) R) : (r.lwk0 (head := head)).packed_out = r.packed_out ;; inj_l := by
(r : Eqv φ ((A, ⊥)::Γ) R) : (r.lwk0 (head := head)).packed_out (L := L) = r.packed_out ;; inj_l
:= by
induction r using Quotient.inductionOn
apply Eqv.eq_of_reg_eq
simp only [LCtx.pack.eq_2, Set.mem_setOf_eq, Subst.InS.pack, InS.coe_lsubst, InS.coe_lwk,
Expand All @@ -329,7 +330,7 @@ theorem Eqv.unpacked_out_packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ

@[simp]
theorem Eqv.packed_out_unpack {Γ : Ctx α ε} {R : LCtx α}
: (unpack (φ := φ) (Γ := Γ) (R := R)).packed_out
: (unpack (φ := φ) (Γ := Γ) (R := R)).packed_out (L := L)
= nil := by
induction R generalizing Γ with
| nil =>
Expand All @@ -345,7 +346,7 @@ theorem Eqv.packed_out_unpack {Γ : Ctx α ε} {R : LCtx α}
rw [<-packed_out, packed_out_lwk0_arrow, I]

theorem Eqv.lsubst_pack_unpack {Γ : Ctx α ε} {R : LCtx α}
: lsubst Subst.Eqv.pack (unpack (φ := φ) (Γ := Γ) (R := R)) = nil := by
: lsubst (Subst.Eqv.pack (L := L)) (unpack (φ := φ) (Γ := Γ) (R := R)) = nil := by
rw [<-Eqv.packed_out, Eqv.packed_out_unpack]

theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
Expand All @@ -366,14 +367,15 @@ theorem Eqv.unpacked_out_injective {Γ : Ctx α ε} {R : LCtx α}
intros x y h; convert congrArg Eqv.packed_out h <;> simp

theorem Eqv.packed_out_injective {Γ : Ctx α ε} {R : LCtx α}
: Function.Injective (Eqv.packed_out (φ := φ) (Γ := Γ) (R := R)) := by
: Function.Injective (Eqv.packed_out (φ := φ) (Γ := Γ) (R := R) (L := [])) := by
intros x y h; convert congrArg Eqv.unpacked_out h <;> simp

theorem Eqv.unpacked_out_inj {Γ : Ctx α ε} {R : LCtx α} {r s : Eqv φ Γ [R.pack]}
: r.unpacked_out = s.unpacked_out ↔ r = s := ⟨λh => unpacked_out_injective h, λh => by simp [h]⟩

theorem Eqv.packed_out_inj {Γ : Ctx α ε} {R : LCtx α} {r s : Eqv φ Γ R}
: r.packed_out = s.packed_out ↔ r = s := ⟨λh => packed_out_injective h, λh => by simp [h]⟩
: r.packed_out (L := []) = s.packed_out ↔ r = s
:= ⟨λh => packed_out_injective h, λh => by simp [h]⟩

theorem Eqv.cfg_unpack_rec {Γ : Ctx α ε} {R L : LCtx α}
{β : Eqv φ Γ (R.pack::L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R.pack::L)}
Expand All @@ -385,7 +387,7 @@ theorem Eqv.cfg_unpack_rec {Γ : Ctx α ε} {R L : LCtx α}

theorem Eqv.packed_out_cfg_liftn {Γ : Ctx α ε} {R L : LCtx α}
{β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
: (cfg R β G).packed_out
: (cfg R β G).packed_out (L := K)
= cfg R (β.lsubst (Subst.Eqv.pack.liftn_append _))
(λi => (G i).lsubst (Subst.Eqv.pack.liftn_append _))
:= by simp only [packed_out, lsubst_cfg, Subst.Eqv.vlift_liftn_append, Subst.Eqv.vlift_pack]
Expand Down Expand Up @@ -571,15 +573,15 @@ theorem Eqv.vwk1_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ (
Subst.Eqv.vlift_unpack_app_out, Subst.Eqv.vlift_unpack_app_out, <-unpacked_app_out]

theorem Eqv.vwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
: r.packed_out.vwk1 (inserted := inserted) = r.vwk1.packed_out := by
: r.packed_out.vwk1 (inserted := inserted) = r.vwk1.packed_out (L := L) := by
rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, Subst.Eqv.vwk1_lsubst_vlift,
Subst.Eqv.vlift_pack, Subst.Eqv.vlift_pack, <-packed_out]

-- theorem Eqv.lwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
-- : r.packed_out.lwk1 (inserted := inserted) = r.packed_out := by
-- sorry
-- rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, Subst.Eqv.lwk1_lsubst_vlift,
-- Subst.Eqv.vlift_pack, Subst.Eqv.vlift_pack, <-packed_out]
theorem Eqv.lwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
: (r.packed_out (L := L)).lwk1 (inserted := inserted) = r.packed_out := by
rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, lwk1, <-lsubst_toSubstE, lsubst_lsubst,
Subst.Eqv.vlift_pack]
rfl

theorem Eqv.unpacked_app_out_let1 {Γ : Ctx α ε} {R L : LCtx α}
{a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]}
Expand Down Expand Up @@ -633,7 +635,7 @@ theorem Eqv.packed_out_cfg_letc {Γ : Ctx α ε} {R L : LCtx α}

theorem Eqv.packed_out_binary_ret_seq {Γ : Ctx α ε}
{r : Eqv φ ((X, ⊥)::Γ) [A, B]} {c : Term.Eqv φ ((A, ⊥)::Γ) (C, ⊥)}
: (r ;; ret c).packed_out = r.packed_out ;; sum nil (ret c) := by
: (r ;; ret c).packed_out (L := L) = r.packed_out ;; sum nil (ret c) := by
simp [packed_out, seq, lsubst_lsubst]
congr 1
ext k; cases k using Fin.cases with
Expand All @@ -657,7 +659,7 @@ theorem Eqv.packed_out_binary_ret_seq {Γ : Ctx α ε}

theorem Eqv.packed_out_ret_seq {Γ : Ctx α ε}
{c : Term.Eqv φ ((X, ⊥)::Γ) (Y, ⊥)} {r : Eqv φ ((Y, ⊥)::Γ) (A::L)}
: (ret c ;; r).packed_out = ret c ;; r.packed_out := by
: (ret c ;; r).packed_out (L := R) = ret c ;; r.packed_out := by
simp [ret_seq, vsubst_packed_out, vwk1_packed_out]

theorem Eqv.packed_out_unpacked_app_out_inner {Γ : Ctx α ε} {R L : LCtx α}
Expand Down
8 changes: 4 additions & 4 deletions DeBruijnSSA/BinSyntax/Typing/Region/Structural.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,23 +20,23 @@ def Subst.pack : Region.Subst φ := λℓ => br 0 (Term.inj_n ℓ)

@[simp]
theorem Subst.Wf.pack {Γ : Ctx α ε} {R : LCtx α}
: Subst.Wf Γ R [R.pack] (Subst.pack (φ := φ)) := λ_ => Wf.br LCtx.Trg.shead Term.Wf.inj_n
: Subst.Wf Γ R (R.pack::L) (Subst.pack (φ := φ)) := λ_ => Wf.br LCtx.Trg.shead Term.Wf.inj_n

@[simp]
def Subst.InS.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.InS φ Γ R [R.pack] :=
def Subst.InS.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.InS φ Γ R (R.pack::L) :=
⟨Subst.pack, Subst.Wf.pack⟩

@[simp]
theorem Subst.InS.coe_pack {Γ : Ctx α ε} {R : LCtx α}
: (Subst.InS.pack (φ := φ) (Γ := Γ) (R := R) : Region.Subst φ) = Subst.pack := rfl
: (Subst.InS.pack (φ := φ) (Γ := Γ) (R := R) (L := L) : Region.Subst φ) = Subst.pack := rfl

@[simp]
theorem Subst.vlift_pack
: pack.vlift = pack (φ := φ) := by funext ℓ; simp [pack, Subst.vlift, vwk1]

@[simp]
theorem Subst.InS.vlift_pack {Γ : Ctx α ε} {R : LCtx α}
: (pack (φ := φ) (Γ := Γ) (R := R)).vlift (head := head) = pack := by ext; simp
: (pack (φ := φ) (Γ := Γ) (R := R) (L := L)).vlift (head := head) = pack := by ext; simp

def unpack : ℕ → Region φ
| 0 => loop
Expand Down

0 comments on commit 3810d92

Please sign in to comment.