From 471c275865391f330dd4d7fc8da8d5d34cb07fe3 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Tue, 24 Sep 2024 14:11:47 +0100 Subject: [PATCH] packed_cfg_den statement --- .../Rewrite/Region/Compose/Cast.lean | 51 ++++++++ .../Rewrite/Region/Compose/Completeness.lean | 18 ++- .../BinSyntax/Rewrite/Region/Compose/Sum.lean | 23 ++-- DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean | 7 ++ .../BinSyntax/Rewrite/Region/LSubst.lean | 17 +++ .../BinSyntax/Rewrite/Region/Structural.lean | 18 ++- .../Rewrite/Region/Structural/Sum.lean | 114 ++++++++++++++++-- .../BinSyntax/Typing/Region/LSubst.lean | 5 + 8 files changed, 220 insertions(+), 33 deletions(-) create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean new file mode 100644 index 0000000..264d4f1 --- /dev/null +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean @@ -0,0 +1,51 @@ +import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum +import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Product + +namespace BinSyntax + +variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε] + +namespace Region + +def Eqv.acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} (h : X = Y) + : Eqv φ ((X, ⊥)::Γ) (Y::L) := (Eqv.nil (targets := L)).cast rfl (by rw [h]) + +@[simp] +theorem Eqv.acast_rfl {Γ : Ctx α ε} {L : LCtx α} {X : Ty α} + : Eqv.acast (φ := φ) (Γ := Γ) (L := L) (X := X) rfl = Eqv.nil := rfl + +theorem Eqv.acast_acast {Γ : Ctx α ε} {L : LCtx α} {X Y Z : Ty α} {h : X = Y} {h' : Y = Z} + : (Eqv.acast (φ := φ) (Γ := Γ) (L := L) h) ;; acast h' = Eqv.acast (by rw [h, h']) + := by cases h; cases h'; simp + +theorem Eqv.rtimes_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y} + : Z ⋊ (acast (φ := φ) (Γ := Γ) (L := L) h) = acast (by rw [h]) + := by cases h; simp [rtimes_nil] + +theorem Eqv.ltimes_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y} + : (acast (φ := φ) (Γ := Γ) (L := L) h) ⋉ Z = acast (by rw [h]) + := by cases h; simp [ltimes_nil] + +theorem Eqv.sum_acast {Γ : Ctx α ε} {L : LCtx α} + {X Y X' Y' : Ty α} {h : X = Y} {h' : X' = Y'} + : sum (acast (φ := φ) (Γ := Γ) (L := L) h) (acast h') = acast (by rw [h, h']) + := by cases h; cases h'; simp [sum_nil] + +theorem Eqv.sum_acast_nil {Γ : Ctx α ε} {L : LCtx α} + {X Y : Ty α} {h : X = Y} + : sum (acast (φ := φ) (Γ := Γ) (L := L) h) (nil (ty := X')) = acast (by rw [h]) + := by cases h; simp [sum_nil] + +theorem Eqv.sum_nil_acast {Γ : Ctx α ε} {L : LCtx α} + {X Y : Ty α} {h : X = Y} + : sum (nil (ty := X')) (acast (φ := φ) (Γ := Γ) (L := L) h) = acast (by rw [h]) + := by cases h; simp [sum_nil] + +theorem Eqv.sum_acast_inv {Γ : Ctx α ε} {L : LCtx α} + {X Y X' Y' : Ty α} {h : X.coprod Y = X'.coprod Y'} + : (acast (φ := φ) (Γ := Γ) (L := L) h) = sum (acast (by cases h; rfl)) (acast (by cases h; rfl)) + := by cases h; simp [sum_nil] + +end Region + +end BinSyntax diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean index b7c4ce1..ab3d1ed 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean @@ -1,6 +1,7 @@ import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Functor import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot +import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Cast import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Distrib namespace BinSyntax @@ -148,14 +149,11 @@ theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α} theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} : (cfg R β G).packed (Δ := Δ) - = ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv - ;; coprod pi_r (fixpoint (ret Term.Eqv.distl_pack ;; unpack.lsubst (Subst.Eqv.fromFCFG (λi => - ret (Term.Eqv.nil.cast - (V := ((R.dist Γ.pack).get i, ⊥)) - (V' := (Γ.pack.prod (R.get (i.cast R.length_dist)), ⊥)) rfl (by simp [R.getElem_dist])) - ;; ret Term.Eqv.split ⋉ _ - ;; assoc - ;; _ ⋊ ((G (i.cast R.length_dist)).packed ;; ret Term.Eqv.pack_app) - ;; sorry - )))) + = ret Term.Eqv.split ;; _ ⋊ β.packed ;; fixpoint ( + _ ⋊ ret Term.Eqv.pack_app ;; distl_inv ;; sum pi_r ( + ret Term.Eqv.distl_pack ;; pack_coprod + (λi => acast (R.get_dist (i := i)) ;; ret Term.Eqv.split ⋉ _ ;; assoc + ;; _ ⋊ (G (i.cast R.length_dist)).packed + ) + )) := sorry diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean index a6febb4..b040a75 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean @@ -11,20 +11,20 @@ namespace Region open Term.Eqv -def Eqv.coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} - (l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)) (r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) - : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) (C::L) +def Eqv.coprod {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} + (l : Eqv φ (⟨A, ⊥⟩::Γ) L) (r : Eqv φ (⟨B, ⊥⟩::Γ) L) + : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L := case (var 0 Ctx.Var.shead) l.vwk1 r.vwk1 -theorem Eqv.lwk_slift_coprod {A B C : Ty α} {Γ : Ctx α ε} {L K : LCtx α} - {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)} - : (l.coprod r).lwk ρ.slift = (l.lwk ρ.slift).coprod (r.lwk ρ.slift) +theorem Eqv.lwk_coprod {A B : Ty α} {Γ : Ctx α ε} {L K : LCtx α} + {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L} + : (l.coprod r).lwk ρ = (l.lwk ρ).coprod (r.lwk ρ) := by simp only [coprod, lwk_case, vwk1_lwk] theorem Eqv.lwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)} : (l.coprod r).lwk1 (inserted := inserted) = (l.lwk1).coprod (r.lwk1) - := by simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_slift_coprod] + := by simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_coprod] theorem Eqv.vwk_slift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Γ.InS Δ} @@ -38,6 +38,13 @@ theorem Eqv.vwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} : (l.coprod r).vwk1 (inserted := inserted) = l.vwk1.coprod r.vwk1 := by simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_coprod] +theorem Eqv.lsubst_vlift_coprod {A B : Ty α} {Γ : Ctx α ε} {L K : LCtx α} + {σ : Subst.Eqv φ Γ L K} {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L} + : (l.coprod r).lsubst σ.vlift = (l.lsubst σ.vlift).coprod (r.lsubst σ.vlift) + := by + simp only [coprod, lsubst_case, vwk1, vwk_lsubst, <-Subst.Eqv.vwk_wk0, Subst.Eqv.vwk_vwk] + rfl + theorem Eqv.ret_of_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} {l : Term.Eqv φ (⟨A, ⊥⟩::Γ) (C, ⊥)} {r : Term.Eqv φ (⟨B, ⊥⟩::Γ) (C, ⊥)} : ret (targets := L) (l.coprod r) = (ret l).coprod (ret r) := by @@ -146,7 +153,7 @@ def Eqv.sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α} theorem Eqv.lwk_slift_sum {A B C D : Ty α} {Γ : Ctx α ε} {L K : LCtx α} {ρ : L.InS K} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)} : (l.sum r).lwk ρ.slift = (l.lwk ρ.slift).sum (r.lwk ρ.slift) - := by simp only [sum, lwk_slift_coprod, lwk_slift_seq]; rfl + := by simp only [sum, lwk_coprod, lwk_slift_seq]; rfl theorem Eqv.lwk1_sum {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α} {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (D::L)} diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean index 2f6d849..02a5bf2 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean @@ -819,6 +819,13 @@ theorem Eqv.vwk1_let2 {L : LCtx α} apply Eqv.eq_of_reg_eq simp [Nat.liftnWk_succ] +theorem Eqv.vsubst0_var0_vwk1 {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ (head::Γ) L} + : (r.vwk1 (inserted := _)).vsubst (Term.Eqv.var 0 Ctx.Var.shead).subst0 = r := by + induction r using Quotient.inductionOn + apply eq_of_reg_eq + simp + exact Region.vsubst0_var0_vwk1 _ + def Eqv.vswap01 {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (left::right::Γ) L) : Eqv φ (right::left::Γ) L := Eqv.vwk Ctx.InS.swap01 r diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean index 53878df..9cae0cb 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean @@ -459,6 +459,16 @@ theorem Subst.Eqv.vwk_quot {Γ Δ : Ctx α ε} {L K : LCtx α} {ρ : Γ.InS Δ} {σ : Subst.InS φ Δ L K} : vwk ρ ⟦σ⟧ = ⟦σ.vwk ρ⟧ := rfl +theorem Subst.Eqv.vwk_wk0 {Γ : Ctx α ε} {σ : Subst.Eqv φ Γ L K} + : (σ.vwk <| Ctx.InS.wk0 (head := head)) = σ.vlift := by + induction σ using Quotient.inductionOn; rfl + +theorem Subst.Eqv.vwk_vwk {Γ Δ Ξ : Ctx α ε} {L K : LCtx α} + {ρ : Γ.InS Δ} {τ : Δ.InS Ξ} {σ : Subst.Eqv φ Ξ L K} + : (σ.vwk τ).vwk ρ = σ.vwk (ρ.comp τ) := by + induction σ using Quotient.inductionOn + simp [Subst.InS.vwk_vwk] + theorem Eqv.vwk_lsubst {Γ Δ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Δ L K} {ρ : Γ.InS Δ} {r : Eqv φ Δ L} @@ -717,6 +727,13 @@ theorem Subst.Eqv.get_fromFCFG {Γ : Ctx α ε} {L K : LCtx α} : (fromFCFG G).get i = G i := by induction G using Eqv.choiceInduction; rw [Subst.Eqv.fromFCFG_quot]; simp +theorem Subst.Eqv.fromFCFG_get {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L K} + : (fromFCFG σ.get) = σ := by ext k; simp [Subst.Eqv.get_fromFCFG] + +theorem Subst.Eqv.get_fromFCFG' {Γ : Ctx α ε} {L K : LCtx α} + {G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) K} + : (fromFCFG G).get = G := funext (λ_ => get_fromFCFG) + def Subst.Eqv.fromFCFG_append {Γ : Ctx α ε} {L K R : LCtx α} (G : ∀i : Fin L.length, Region.Eqv φ ((L.get i, ⊥)::Γ) (K ++ R)) : Subst.Eqv φ Γ (L ++ R) (K ++ R) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean index 7e48cc3..440104c 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean @@ -119,16 +119,28 @@ theorem Eqv.packed_case {Γ : Ctx α ε} {R : LCtx α} (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) s.packed) := by simp only [packed, packed_out_case, packed_in_case] -theorem Eqv.packed_cfg {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} +theorem Eqv.packed_cfg_unpack {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} : (cfg R β G).packed (Δ := Δ) - = gloop R.pack β.packed.unpacked_app_out + = gloop R.pack + β.packed.unpacked_app_out (unpack.lsubst (Subst.Eqv.fromFCFG (λi => (let1 (pair (var 2 (by simp)) (var 0 Ctx.Var.shead)) (G i).packed.unpacked_app_out)))) := by - rw [packed_def', packed_in_cfg, packed_out_cfg_gloop, <-packed_def'] + rw [packed_def', packed_in_cfg, packed_out_cfg_gloop_unpack, <-packed_def'] congr; funext i rw [vwk1_unpacked_app_out, packed_out_let1, <-packed_def', <-unpacked_app_out_let1] simp +theorem Eqv.packed_cfg {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} + : (cfg R β G).packed (Δ := Δ) + = gloop R.pack + β.packed.unpacked_app_out + (pack_coprod + (λi => (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) (G i).packed.unpacked_app_out))) + := by + rw [packed_def', packed_in_cfg, packed_out_cfg_gloop, <-packed_def'] + congr; funext i + rw [packed_out_let1, <-packed_def', unpacked_app_out_let1] + end Region end BinSyntax diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean index af45d55..37a2605 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean @@ -25,18 +25,67 @@ theorem Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α} simp [ Region.unpack, Region.nil, Region.ret, Region.lwk0, Region.vwk_lwk, Region.vwk_lift_unpack] --- def Eqv.pack_case {Γ : Ctx α ε} {R : LCtx α} {X : Ty α} --- (r : Eqv φ ((X.prod R, ⊥)::Γ) (R.dist X, e)) : Eqv φ ((R.dist X, ⊥)::Γ) (R.pack, e) := --- case (Term.Eqv.dist X) --- (br (List.length R) Term.Eqv.pi_r (by simp)) --- (lwk_id LCtx.Wkn.id_right_dist r) - -def Eqv.pack_coprod {Γ : Ctx α ε} {R : LCtx α} - (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)) : Eqv φ ((R.pack, ⊥)::Γ) (A::L) := +def Eqv.pack_case {Γ : Ctx α ε} {R L : LCtx α} + (a : Term.Eqv φ Γ (R.pack, e)) (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L) + : Eqv φ Γ L := match R with + | [] => let1 a loop + | _::R => case a + (pack_case (e := e) Term.Eqv.nil (λi => (G i.succ).vwk1)) + (G (0 : Fin (R.length + 1))) + +theorem Eqv.vwk_pack_case {Γ : Ctx α ε} {R L : LCtx α} + {a : Term.Eqv φ Δ (R.pack, e)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Δ) L} + {ρ : Γ.InS Δ} + : (pack_case a G).vwk ρ = pack_case (a.wk ρ) (λi => (G i).vwk ρ.slift) := by + induction R generalizing Γ Δ with + | nil => simp [pack_case] + | cons A R I => + simp only [pack_case, vwk_case, I] + congr; funext i; simp only [vwk1, vwk_vwk] + congr 1; ext k; cases k <;> rfl + +theorem Eqv.vwk1_pack_case {Γ : Ctx α ε} {R L : LCtx α} + (a : Term.Eqv φ (V::Γ) (R.pack, e)) (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::V::Γ) L) + : (pack_case a G).vwk1 (inserted := inserted) = pack_case (φ := φ) a.wk1 (λi => (G i).vwk2) := by + simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_pack_case] + simp only [Ctx.InS.lift_wk0, Ctx.InS.lift_wk1]; rfl + +-- TODO: vsubst_pack_case, lwk_pack_case, lsubst_pack_case + +def Eqv.pack_coprod {Γ : Ctx α ε} {R L : LCtx α} + (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L) : Eqv φ ((R.pack, ⊥)::Γ) L := match R with - | [] => zero + | [] => loop | _::R => coprod (pack_coprod (λi => G i.succ)) (G (0 : Fin (R.length + 1))) +theorem Eqv.pack_case_nil_vwk1 {Γ : Ctx α ε} {R L : LCtx α} + (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L) + : pack_case (e := e) Term.Eqv.nil (λi => (G i).vwk1) = pack_coprod G := by induction R with + | nil => rw [ + pack_coprod, pack_case, <-Term.Eqv.wk_eff_nil (h := bot_le), let1_wk_eff, + let1_beta, vsubst_loop + ] + | cons A R I => + rw [ + pack_case, pack_coprod, <-I, coprod, <-Term.Eqv.wk_eff_nil (h := bot_le), case_wk_eff, + vwk1_pack_case] + simp only [vwk1_vwk2] + rfl + +-- TODO: vwk_lift_pack_coprod, vsubst_lift_pack_coprod, lwk_pack_coprod, lsubst_pack_coprod + +theorem Eqv.pack_coprod_empty {Γ : Ctx α ε} {L : LCtx α} + (G : (i : Fin 0) → Eqv φ (⟨[].get i, ⊥⟩::Γ) L) : (pack_coprod (R := []) G) = loop := rfl + +theorem Eqv.pack_coprod_cons {Γ : Ctx α ε} {R : LCtx α} {L : LCtx α} + (G : (i : Fin (R.length + 1)) → Eqv φ (⟨(A::R).get i, ⊥⟩::Γ) L) + : (pack_coprod (R := A::R) G) = coprod (pack_coprod (λi => G i.succ)) (G (0 : Fin (R.length + 1))) + := rfl + +theorem Eqv.pack_coprod_zero {Γ : Ctx α ε} {L : LCtx α} + (G : (i : Fin 0) → Eqv φ (⟨[].get i, ⊥⟩::Γ) (A::L)) : (pack_coprod (R := []) G) = zero := by + rw [pack_coprod_empty]; apply Eqv.zero_eq + @[simp] theorem Eqv.vwk_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (ρ : Γ.InS Δ) : Eqv.vwk (ρ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = unpack := by @@ -57,6 +106,32 @@ theorem Eqv.vsubst_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Subs apply Eqv.eq_of_reg_eq simp +theorem Eqv.lsubst_vlift_fromFCFG_unpack {Γ : Ctx α ε} {L K : LCtx α} + {G : (i : Fin L.length) → Eqv φ (⟨L.get i, ⊥⟩::Γ) K} + : Eqv.lsubst (Subst.Eqv.fromFCFG G).vlift Eqv.unpack = Eqv.pack_coprod G := by + induction L with + | nil => simp [unpack, pack_coprod] + | cons A L I => + simp [unpack, pack_coprod, lsubst_vlift_coprod] + rw [<-I, lwk0, <-lsubst_toSubstE, lsubst_lsubst] + congr + · ext k; simp only [List.get_eq_getElem, Subst.Eqv.get_comp, Subst.Eqv.get_toSubstE, + Set.mem_setOf_eq, LCtx.InS.coe_wk0, Nat.succ_eq_add_one, lsubst_br, List.length_cons, id_eq, + List.getElem_cons_succ, Subst.Eqv.get_vlift, Subst.Eqv.get_fromFCFG, vwk_id_eq, + vsubst0_var0_vwk1]; rfl + · simp [<-br_zero_eq_ret, <-ret_nil, Subst.Eqv.get_fromFCFG, Term.Eqv.nil, vsubst0_var0_vwk1] + +theorem Eqv.lsubst_vlift_unpack {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.Eqv φ Γ L K) + : Eqv.lsubst σ.vlift Eqv.unpack = Eqv.pack_coprod σ.get := by + rw [<-Subst.Eqv.fromFCFG_get (σ := σ), lsubst_vlift_fromFCFG_unpack, Subst.Eqv.fromFCFG_get] + +theorem Eqv.lsubst_fromFCFG_vwk1_unpack {Γ : Ctx α ε} {R L : LCtx α} + {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L} + : Eqv.lsubst (Subst.Eqv.fromFCFG (λi => (G i).vwk1)) Eqv.unpack + = Eqv.pack_coprod G := by + convert Eqv.lsubst_vlift_fromFCFG_unpack + ext l; simp [Subst.Eqv.get_fromFCFG] + def Subst.Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ [R.pack] R := Region.Eqv.unpack.csubst @@ -285,7 +360,7 @@ theorem Eqv.lsubst_pack_append_vlift_unpack {Γ : Ctx α ε} {L R : LCtx α} funext k simp only [Subst.comp, Region.lsubst, Subst.vlift, Nat.succ_eq_add_one, Function.comp_apply, Subst.liftn, add_lt_add_iff_right, Region.lwk, zero_add, Nat.reduceSubDiff, - vsubst0_var0_vwk1, Subst.vwk1_comp_fromLwk, vwk2_vwk1, lsubst_fromLwk] + Region.vsubst0_var0_vwk1, Subst.vwk1_comp_fromLwk, vwk2_vwk1, lsubst_fromLwk] split <;> rfl · simp [ lwk0, Term.Eqv.seq, let1_let1, Term.Eqv.sum, Term.Eqv.coprod, Term.Eqv.wk2, Term.Eqv.nil, @@ -319,6 +394,12 @@ theorem Eqv.lsubst_pack_append_vlift_unpack {Γ : Ctx α ε} {L R : LCtx α} apply eq_of_reg_eq simp +theorem Eqv.pack_coprod_pack_append {Γ : Ctx α ε} {L R : LCtx α} + : pack_coprod (Subst.Eqv.liftn_append R Subst.Eqv.pack).get + = unpack_right_out (φ := φ) (Γ := Γ) (R := R) (L := L) := by + convert lsubst_pack_append_vlift_unpack + rw [lsubst_vlift_unpack] + theorem Eqv.lsubst_pack_append_unpack {Γ : Ctx α ε} {L R : LCtx α} : lsubst (Subst.Eqv.liftn_append R Subst.Eqv.pack) (unpack (φ := φ) (Γ := Γ) (R := R ++ L)) = unpack_right_out := by @@ -433,10 +514,11 @@ theorem Eqv.extend_unpack_unpacked_app_out : r.unpacked_app_out.lsubst Subst.Eqv.unpack.extend = r.unpacked_right_out := by rw [unpacked_app_out, lsubst_lsubst, Subst.Eqv.extend_unpack_comp_unpack_app_out]; rfl -theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α} +theorem Eqv.packed_out_cfg_gloop_unpack {Γ : Ctx α ε} {R L : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} : (cfg R β G).packed_out - = gloop R.pack β.packed_out.unpacked_app_out + = gloop R.pack + β.packed_out.unpacked_app_out (unpack.lsubst (Subst.Eqv.fromFCFG (λi => (G i).packed_out.unpacked_app_out.vwk1))) := calc _ = (cfg R (β.packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend) (λi => (G i).packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend.vlift)) @@ -447,6 +529,14 @@ theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α} · ext k; simp [Subst.Eqv.get_fromFCFG] · simp [Subst.Eqv.unpack] +theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α} + {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} + : (cfg R β G).packed_out + = gloop R.pack + β.packed_out.unpacked_app_out + (pack_coprod (λi => (G i).packed_out.unpacked_app_out)) + := by rw [packed_out_cfg_gloop_unpack, lsubst_fromFCFG_vwk1_unpack] + -- theorem Eqv.packed_out_gloop {Γ : Ctx α ε} {R L : LCtx α} -- {β : Eqv φ Γ (A::L)} {G : Eqv φ (⟨A, ⊥⟩::Γ) (A::L)} -- : (gloop A β G).packed_out diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean index 1059ce8..8c83f9c 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean @@ -533,6 +533,11 @@ theorem Region.Subst.InS.get_vwk {Γ Δ : Ctx α ε} : (σ.vwk ρ).get i = (σ.get i).vwk ρ.slift := rfl +theorem Region.Subst.InS.vwk_vwk {Γ Δ Ξ : Ctx α ε} + {ρ : Γ.InS Δ} {τ : Δ.InS Ξ} {σ : Region.Subst.InS φ Ξ L K} + : (σ.vwk τ).vwk ρ = σ.vwk (ρ.comp τ) + := by ext; simp [Region.vwk_vwk, Nat.liftWk_comp] + def Region.Subst.InS.vsubst {Γ Δ : Ctx α ε} (ρ : Term.Subst.InS φ Γ Δ) (σ : Region.Subst.InS φ Δ L K) : Region.Subst.InS φ Γ L K