From d80021b105d71bbc4f57338fc65eb1b253d6e92f Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Sat, 28 Sep 2024 01:51:17 +0100 Subject: [PATCH] Further Elgotwork --- .../Rewrite/Region/Compose/Completeness.lean | 80 ++++++++++++++++--- .../Rewrite/Region/Compose/Product.lean | 26 ++++++ .../BinSyntax/Rewrite/Region/Compose/Seq.lean | 24 ++++++ .../BinSyntax/Rewrite/Region/Compose/Sum.lean | 36 +++++++++ .../BinSyntax/Rewrite/Region/Structural.lean | 15 +++- .../Rewrite/Region/Structural/Elgot.lean | 27 ++++--- .../Rewrite/Region/Structural/Product.lean | 4 + .../Rewrite/Region/Structural/Sum.lean | 27 ++++++- .../Rewrite/Term/Compose/Distrib.lean | 5 ++ .../Rewrite/Term/Compose/Product.lean | 8 ++ .../Rewrite/Term/Structural/Distrib.lean | 13 +++ 11 files changed, 242 insertions(+), 23 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean index 39658f9..955c4ce 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean @@ -159,18 +159,74 @@ theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α} open Term.Eqv +-- theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} +-- : (cfg R β G).packed (Δ := Δ) +-- = 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 +-- ))) := by +-- -- rw [ +-- -- packed_cfg_unpack, letc_to_vwk1, letc_vwk1_den, ret_seq, <-vsubst_packed_out, +-- -- <-vwk1_packed_out, <-ret_seq +-- -- ] +-- -- simp only [seq_assoc] +-- -- congr 1 +-- sorry + +theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α} + {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} : r.unpacked_app_out + = (r ;; ret Term.Eqv.pack_app).lwk1 ;; left_exit + := by + rw [seq, seq, lwk1, <-lsubst_toSubstE, lsubst_lsubst, lsubst_lsubst, unpacked_app_out] + congr; 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, Subst.Eqv.unpack_app_out, unpack_app_out, csubst_get, cast_rfl, + left_exit, List.getElem_cons_succ, vwk1_case, wk1_var0, List.length_cons, Fin.zero_eta, vwk2_br, + wk2_var0, vwk1_br, wk1_pack_app, Subst.Eqv.get_comp, get_alpha0, List.length_nil, Fin.val_succ, + Fin.cases_zero, lsubst_br, Subst.Eqv.get_vlift, Subst.Eqv.get_toSubstE, Set.mem_setOf_eq, + Fin.coe_fin_one, LCtx.InS.coe_wk1, Nat.liftWk_zero, Nat.reduceAdd, zero_add, vwk_id_eq, + vsubst_case, var0_subst0, wk_res_self, vsubst_br, subst_lift_var_zero, Nat.add_zero, + Nat.zero_eq] + rfl + theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} : (cfg R β G).packed (Δ := Δ) - = 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 - ))) := by - rw [ - packed_cfg_unpack, letc_to_vwk1, letc_vwk1_den, ret_seq, <-vsubst_packed_out, - <-vwk1_packed_out, <-ret_seq - ] - simp only [seq_assoc] + = (ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv ;; sum pi_r nil) + ;; coprod nil ( + fixpoint ( + 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 ;; ret Term.Eqv.pack_app) + ;; distl_inv + ;; sum pi_r nil + ) + ) + ) + := by + rw [packed_cfg_split_vwk1, fixpoint_def', letc_vwk1_den] congr 1 - sorry + · rw [ret_seq, <-vsubst_packed_out, <-vwk1_packed_out, <-ret_seq] + simp only [seq_assoc] + congr 1 + simp [distl_inv_eq_ret, ret_seq, sum, coprod, vwk1_vwk2] + simp [ + vwk1_seq, Term.Eqv.distl_inv, vsubst_lift_seq, rtimes, packed_out_let2, let2_seq, + vwk1_unpacked_app_out, wk1_coprod, wk1_let2, <-Ctx.InS.lift_lift, wk_lift_coprod, + Nat.liftnWk + ] + congr 1 + conv => rhs; rw [<-ret, case_let2, seq_assoc]; rhs; rw [ret_seq] + simp [ + vwk1_let2, <-Term.Subst.Eqv.lift_lift, vsubst_lift_coprod, vwk2_seq, vwk1_seq, vwk3, + vwk_lift_seq, vsubst_lift_seq, <-Ctx.InS.lift_wk2, Nat.liftnWk, Term.Eqv.coprod, let2_pair, + let1_beta, case_case + ] + simp [ + case_inl, case_inr + ] + sorry + · rw [fixpoint_def'] + congr 5 + sorry diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean index 46f7a78..b45d894 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean @@ -209,6 +209,19 @@ theorem Eqv.runit_eq_ret {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α} theorem Eqv.vwk1_pi_l {Γ : Ctx α ε} {L : LCtx α} : (pi_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = pi_l := rfl +@[simp] +theorem Eqv.vwk2_pi_l {Γ : Ctx α ε} {L : LCtx α} + : (pi_l (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted) = pi_l := rfl + +@[simp] +theorem Eqv.vwk_lift_pi_l {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Ctx.InS Γ Δ} + : (pi_l (φ := φ) (A := A) (B := B) (L := L)).vwk (ρ.lift (le_refl _)) = pi_l := rfl + +@[simp] +theorem Eqv.vsubst_lift_pi_l {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Term.Subst.Eqv φ Γ Δ} + : (pi_l (φ := φ) (A := A) (B := B) (L := L)).vsubst (ρ.lift (le_refl _)) = pi_l := by + induction ρ using Quotient.inductionOn; rfl + theorem Eqv.ret_pair_pi_l {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} {a : Term.Eqv φ ((X, ⊥)::Γ) (A, ⊥)} {b : Term.Eqv φ ((X, ⊥)::Γ) (B, ⊥)} : ret (targets := L) (a.pair b) ;; pi_l = ret a @@ -259,6 +272,19 @@ theorem Eqv.lunit_eq_ret {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α} theorem Eqv.vwk1_pi_r {Γ : Ctx α ε} {L : LCtx α} : (pi_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = pi_r := rfl +@[simp] +theorem Eqv.vwk2_pi_r {Γ : Ctx α ε} {L : LCtx α} + : (pi_r (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted) = pi_r := rfl + +@[simp] +theorem Eqv.vwk_lift_pi_r {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Ctx.InS Γ Δ} + : (pi_r (φ := φ) (A := A) (B := B) (L := L)).vwk (ρ.lift (le_refl _)) = pi_r := rfl + +@[simp] +theorem Eqv.vsubst_lift_pi_r {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Term.Subst.Eqv φ Γ Δ} + : (pi_r (φ := φ) (A := A) (B := B) (L := L)).vsubst (ρ.lift (le_refl _)) = pi_r := by + induction ρ using Quotient.inductionOn; rfl + theorem Eqv.ret_pair_pi_r {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} {a : Term.Eqv φ ((X, ⊥)::Γ) (A, ⊥)} {b : Term.Eqv φ ((X, ⊥)::Γ) (B, ⊥)} : ret (targets := L) (a.pair b) ;; pi_r = ret b diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean index a563866..61f9b22 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean @@ -949,3 +949,27 @@ theorem Eqv.loop_seq {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ ((B, ⊥)::Γ) ( : loop (Γ := (A, ⊥)::Γ) (L := B::L) ;; r = loop := by induction r using Quotient.inductionOn simp [loop_def, Region.InS.append_def] + +theorem Eqv.lsubst_vlift_ret_seq {Γ : Ctx α ε} {L K : LCtx α} + {σ : Subst.Eqv φ Γ (C::L) K} {a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)} + : (ret a ;; r).lsubst σ.vlift = vsubst a.subst0 (r.lsubst σ.vlift).vwk1 := by + induction a using Quotient.inductionOn + induction r using Quotient.inductionOn + induction σ using Quotient.inductionOn + apply Eqv.eq_of_reg_eq + simp only [Set.mem_setOf_eq, InS.lsubst_br, List.length_cons, Fin.zero_eta, List.get_eq_getElem, + Fin.val_zero, List.getElem_cons_zero, InS.coe_lsubst, Subst.InS.coe_vlift, InS.coe_vsubst, + Term.InS.coe_subst0, InS.coe_vwk_id, Subst.InS.coe_get, InS.coe_alpha0, InS.coe_vwk, + Ctx.InS.coe_wk1, ← Region.vsubst_fromWk, Region.vsubst_vsubst, Term.liftWk_succ_comp_subst0] + simp only [Subst.vlift, Region.vsubst_lsubst] + congr 1 + · funext k; + simp only [Region.vwk1, ← Region.vsubst_fromWk, Function.comp_apply, Region.vsubst_vsubst] + congr + funext j; cases j <;> rfl + · simp [Region.alpha, Term.alpha, Region.vsubst_vsubst] + +theorem Eqv.lsubst_vlift_ret_seq' {Γ : Ctx α ε} {L K : LCtx α} + {σ : Subst.Eqv φ Γ (C::L) (C'::K)} {a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)} + : (ret a ;; r).lsubst σ.vlift = ret a ;; r.lsubst σ.vlift := by + rw [lsubst_vlift_ret_seq, ret_seq] diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean index 9458ab8..f7d7b6a 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean @@ -113,10 +113,28 @@ def Eqv.inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} theorem Eqv.inj_l_eq_ret {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} : Eqv.inj_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = ret Term.Eqv.inj_l := rfl +@[simp] theorem Eqv.vwk1_inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} : (inj_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = inj_l := rfl +@[simp] +theorem Eqv.vwk2_inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} + : (inj_l (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted) + = inj_l := rfl + +@[simp] +theorem Eqv.vwk_lift_inj_l {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + {ρ : Γ.InS Δ} + : (inj_l (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vwk (ρ.slift) + = inj_l := rfl + +@[simp] +theorem Eqv.vsubst_lift_inj_l {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + {ρ : Term.Subst.Eqv φ Γ Δ} + : (inj_l (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vsubst (ρ.lift (le_refl _)) + = inj_l := by induction ρ using Quotient.inductionOn; rfl + theorem Eqv.lwk1_inj_l {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} : (inj_l (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).lwk1 (inserted := inserted) = inj_l := rfl @@ -135,10 +153,28 @@ def Eqv.inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} theorem Eqv.inj_r_eq_ret {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} : Eqv.inj_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L) = ret Term.Eqv.inj_r := rfl +@[simp] theorem Eqv.vwk1_inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} : (inj_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).vwk1 (inserted := inserted) = inj_r := rfl +@[simp] +theorem Eqv.vwk2_inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} + : (inj_r (φ := φ) (A := A) (B := B) (Γ := V::Γ) (L := L)).vwk2 (inserted := inserted) + = inj_r := rfl + +@[simp] +theorem Eqv.vwk_lift_inj_r {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + {ρ : Γ.InS Δ} + : (inj_r (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vwk (ρ.slift) + = inj_r := rfl + +@[simp] +theorem Eqv.vsubst_lift_inj_r {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + {ρ : Term.Subst.Eqv φ Γ Δ} + : (inj_r (φ := φ) (A := A) (B := B) (Γ := Δ) (L := L)).vsubst (ρ.lift (le_refl _)) + = inj_r := by induction ρ using Quotient.inductionOn; rfl + theorem Eqv.lwk1_inj_r {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} : (inj_r (φ := φ) (A := A) (B := B) (Γ := Γ) (L := L)).lwk1 (inserted := inserted) = inj_r := rfl diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean index 12c2023..a30946e 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean @@ -73,7 +73,7 @@ theorem Eqv.vwk_liftn₂_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv simp [<-Ctx.InS.lift_lift] @[simp] -theorem Eqv.vwk1_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R} +theorem Eqv.vwk1_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R} : r.packed.vwk1 (inserted := inserted) = r.packed (Δ := _::Δ) := by rw [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_packed] @@ -161,6 +161,19 @@ theorem Eqv.packed_cfg_split {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R · rw [packed_in_unpacked_app_out, <-packed] · rw [packed_in_pack_coprod_arr]; congr; funext i; rw [packed_in_unpacked_app_out, <-packed] +theorem Eqv.packed_cfg_split_vwk1 {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} + : (cfg R β G).packed (Δ := Δ) + = letc (Γ.pack.prod R.pack) + (ret Term.Eqv.split ;; _ ⋊ β.packed.unpacked_app_out) + (ret Term.Eqv.split ⋉ _ ;; assoc + ;; _ ⋊ (ret Term.Eqv.distl_pack + ;; pack_coprod (λi => acast R.get_dist + ;; (G (i.cast R.length_dist)).packed.unpacked_app_out))).vwk1 := by + rw [packed_cfg_split] + simp only [List.get_eq_getElem, Fin.coe_cast, vwk1_seq, vwk1_ltimes, vwk1_br, wk1_split, + vwk1_rtimes, wk1_distl_pack, vwk1_pack_coprod, vwk1_acast, vwk1_unpacked_app_out, vwk1_packed] + rfl + -- TODO: unpacked_app_out ltimes dinaturality end Region diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean index b8cbdca..570f0da 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Elgot.lean @@ -8,17 +8,26 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O namespace Region -def Eqv.fixpoint_def' {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)) - : Eqv φ (⟨A, ⊥⟩::Γ) (B::L) := letc A nil (f.vwk1.lwk1 ;; left_exit) +def Eqv.fixpoint_def' {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} + {f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)} + : fixpoint f = letc A nil (f.vwk1.lwk1 ;; left_exit) + := rfl -theorem Eqv.letc_to_vwk1 {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} {β : Eqv φ ((B, ⊥)::Γ) (A::L)} {G} - : letc A β G = letc (B.prod A) - (ret Term.Eqv.split ;; _ ⋊ β) - ((ret Term.Eqv.split ⋉ _ ;; assoc ;; _ ⋊ (let2 (Term.Eqv.var 0 Ctx.Var.shead) G.vwk2)).vwk1) - := by - sorry + +def Eqv.fixpoint_def_vwk1 {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} + {f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L)} + : fixpoint f = letc A nil (f.lwk1 ;; left_exit).vwk1 + := by rw [vwk1_seq, vwk1_lwk1]; rfl + +-- theorem Eqv.letc_to_vwk1 {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} {β : Eqv φ ((B, ⊥)::Γ) (A::L)} {G} +-- : letc A β G = letc (B.prod A) +-- (ret Term.Eqv.split ;; _ ⋊ β) +-- ((ret Term.Eqv.split ⋉ _ ;; assoc ;; _ ⋊ (let2 (Term.Eqv.var 0 Ctx.Var.shead) G.vwk2)).vwk1) +-- := by +-- sorry theorem Eqv.letc_vwk1_den {Γ : Ctx α ε} {A B : Ty α} {β : Eqv φ ((X, ⊥)::Γ) [A, B]} {G : Eqv φ ((A, ⊥)::Γ) [A, B]} - : letc A β G.vwk1 = β.packed_out ;; fixpoint (coprod (coprod zero inj_l) (G.packed_out ;; inj_r)) + : letc A β G.vwk1 = (β.packed_out ;; sum (coprod zero nil) nil) ;; + coprod nil (fixpoint (G.packed_out ;; coprod (coprod zero inj_l) inj_r)) := sorry diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Product.lean index f584da6..320877c 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Product.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Product.lean @@ -60,6 +60,10 @@ theorem Eqv.vwk2_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R} : r.packed_in.vwk2 (inserted := inserted) = r.packed_in (Δ := head::_::Δ) := by rw [vwk2, <-Ctx.InS.lift_wk1, vwk_slift_packed_in] +theorem Eqv.lwk1_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ (A::R)} + : r.packed_in.lwk1 (inserted := inserted) = r.lwk1.packed_in (Δ := Δ) := by + rw [packed_in, lwk1, packed_in, lwk1, vsubst_lwk] + @[simp] theorem Eqv.vsubst_lift_packed_in {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R} {σ : Term.Subst.Eqv φ Δ' Δ} diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean index ea2f68a..8200d7a 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean @@ -169,6 +169,19 @@ theorem Subst.Eqv.vliftn₂_unpack {Γ : Ctx α ε} {R : LCtx α} : (Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).vliftn₂ (left := left) (right := right) = unpack := by simp [Subst.Eqv.vliftn₂_eq_vlift_vlift] +@[simp] +theorem Subst.Eqv.vwk_unpack {Γ : Ctx α ε} {R : LCtx α} {ρ : Γ.InS Δ} + : (Subst.Eqv.unpack (φ := φ) (R := R)).vwk ρ = unpack := by + rw [unpack_def, vwk_quot, unpack_def] + apply congrArg; ext; simp + +@[simp] +theorem Subst.Eqv.vsubst_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (σ : Term.Subst.Eqv φ Δ Γ) + : (Subst.Eqv.unpack (φ := φ) (R := R)).vsubst σ = unpack := by + induction σ using Quotient.inductionOn + 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⟧ @[simp] @@ -243,7 +256,13 @@ theorem Eqv.unpacked_out_case {Γ : Ctx α ε} {R : LCtx α} (l : Eqv φ ((A, ⊥)::Γ) [R.pack]) (r : Eqv φ ((B, ⊥)::Γ) [R.pack]) : (case a l r).unpacked_out = case a l.unpacked_out r.unpacked_out := by simp [unpacked_out] --- TODO: unpacking a cfg is a quarter of Böhm–Jacopini +theorem Eqv.vsubst_unpacked_out {Γ : Ctx α ε} {R : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ} + {r : Eqv φ Δ [R.pack]} : r.unpacked_out.vsubst σ = (r.vsubst σ).unpacked_out := by + simp [unpacked_out, vsubst_lsubst] + +theorem Eqv.unpacked_out_vsubst {Γ : Ctx α ε} {R : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ} + {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] := h.lsubst Subst.Eqv.pack @@ -556,6 +575,12 @@ theorem Eqv.vwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R 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.unpacked_app_out_let1 {Γ : Ctx α ε} {R L : LCtx α} {a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} : (let1 a r).unpacked_app_out = let1 a r.unpacked_app_out := by simp [unpacked_app_out] diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean index 2663aa9..4c07eae 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean @@ -21,6 +21,11 @@ theorem Eqv.wk1_distl_inv {A B C : Ty α} {Γ : Ctx α ε} (inserted := inserted) = distl_inv := rfl +@[simp] +theorem Eqv.wk_lift_distl_inv {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} + : (distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Δ) (e := e)).wk ρ.slift + = distl_inv := rfl + theorem Eqv.seq_distl_inv_eq_let {X A B C : Ty α} {Γ : Ctx α ε} {r : Eqv φ ((X, ⊥)::Γ) ⟨A.prod (B.coprod C), e⟩} : r ;;' distl_inv = let1 r distl_inv diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean index 333ea34..a7e470a 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean @@ -90,6 +90,14 @@ theorem Eqv.let2_nil {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B, def Eqv.split {A : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.prod A, e⟩ := pair nil nil +@[simp] +theorem Eqv.wk_lift_split {A : Ty α} {Γ Δ : Ctx α ε} {ρ : Ctx.InS Γ Δ} + : split.wk ρ.slift = split (φ := φ) (A := A) (e := e) := rfl + +@[simp] +theorem Eqv.wk1_split {A : Ty α} {Γ : Ctx α ε} + : (split (Γ := Γ)).wk1 (inserted := inserted) = split (φ := φ) (A := A) (e := e) := rfl + theorem Eqv.pl_split {A : Ty α} {Γ : Ctx α ε} : split.pl = nil (φ := φ) (Γ := Γ) (A := A) (e := e) := by rw [pl, split, let2_pair, nil, let1_beta_var0, wk0_var, let1_beta_var1]; rfl diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Distrib.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Distrib.lean index 023bfad..8882570 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Distrib.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Distrib.lean @@ -22,6 +22,19 @@ theorem Eqv.split_rtimes_pi_r_distl_packed {A B : Ty α} {Γ : Ctx α ε} (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv) := split_rtimes_pi_r_distl +@[simp] +theorem Eqv.wk_lift_distl_pack {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} + : (distl_pack (φ := φ) (R := R) (X := X) (e := e)).wk ρ.slift = distl_pack := by + induction R with + | nil => rfl + | cons A R I => simp [distl_pack, wk_lift_seq, wk_lift_coprod, I] + +@[simp] +theorem Eqv.wk1_distl_pack {Γ : Ctx α ε} {R : LCtx α} {X : Ty α} + : (distl_pack (φ := φ) (Γ := Γ) (R := R) (X := X) (e := e)).wk1 (inserted := inserted) + = distl_pack + := by rw [wk1, <-Ctx.InS.lift_wk0, wk_lift_distl_pack] + -- theorem Eqv.split_rtimes_nil_packed_distl {A B C : Ty α} {Γ : Ctx α ε} -- : split (φ := φ) (A := Ctx.pack ((A.coprod B, ⊥)::Γ)) (e := e) (Γ := Δ) -- ;;' _ ⋊' Term.Eqv.nil.packed ;;' distl_inv