From e29bb04a43480db03ff2e7ec984c8d1a50ebdea5 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Sat, 28 Sep 2024 20:37:49 +0100 Subject: [PATCH] Nicened packed_cfg_split --- .../Rewrite/Region/Compose/Cast.lean | 9 +++- .../Rewrite/Region/Compose/Completeness.lean | 8 +++- .../BinSyntax/Rewrite/Region/Structural.lean | 16 ++++--- .../Rewrite/Region/Structural/Sum.lean | 44 ++++++++++++++++--- 4 files changed, 64 insertions(+), 13 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean index dce92b9..e62b470 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean @@ -8,7 +8,7 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O 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]) + : Eqv φ ((X, ⊥)::Γ) (Y::L) := ret (Term.Eqv.nil.cast rfl (by rw [h])) @[simp] theorem Eqv.acast_rfl {Γ : Ctx α ε} {L : LCtx α} {X : Ty α} @@ -17,7 +17,12 @@ theorem Eqv.acast_rfl {Γ : Ctx α ε} {L : LCtx α} {X : Ty α} @[simp] theorem Eqv.vwk1_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y} : (Eqv.acast (φ := φ) (Γ := Γ) (L := L) h).vwk1 (inserted := inserted) = Eqv.acast h - := by cases h; simp + := rfl + +@[simp] +theorem Eqv.lwk1_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y} + : (Eqv.acast (φ := φ) (Γ := Γ) (L := L) h).lwk1 (inserted := inserted) = Eqv.acast h + := rfl theorem Eqv.acast_seq {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y} {r : Eqv φ ((Y, ⊥)::Γ) (Z::L)} diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean index 99ebeb8..9a4ed98 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean @@ -175,7 +175,7 @@ open Term.Eqv -- -- congr 1 -- sorry -theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α} +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 @@ -191,6 +191,11 @@ theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α} Nat.zero_eq] rfl +theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α} + {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} : r.unpacked_app_out + = r.lwk1 ;; ret Term.Eqv.pack_app ;; left_exit + := by rw [unpacked_app_out_eq_left_exit', lwk1_seq, lwk1_ret] + theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} : (cfg R β G).packed (L := []) (Δ := Δ) = (ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv ;; sum pi_r nil) @@ -264,4 +269,5 @@ theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R + simp [seq_assoc, ltimes_eq_ret, assoc_eq_ret, packed_out_ret_seq] apply congrArg apply congrArg + --simp only [unpacked_app_out_eq_left_exit] sorry diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean index 9e90447..48cdd42 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean @@ -97,6 +97,11 @@ theorem Eqv.vsubst_liftn₂_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eq : r.packed.vsubst (σ.liftn₂ (le_refl _) (le_refl V)) = r.packed (L := L) (Δ := _::Δ') := by simp [<-Term.Subst.Eqv.lift_lift] +@[simp] +theorem Eqv.lwk1_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R} + : r.packed.lwk1 (inserted := inserted) = r.packed (L := _::L) (Δ := Δ) := by + rw [packed_def', lwk1_packed_out, <-packed_def'] + open Term.Eqv theorem Eqv.packed_br {Γ : Ctx α ε} {L : LCtx α} @@ -157,12 +162,13 @@ theorem Eqv.packed_cfg_split {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R (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))) := by + ;; (pack_coprod (λi => acast R.get_dist + ;; (G (i.cast R.length_dist)).packed)).unpacked_app_out)) := by rw [packed, packed_out_cfg_letc, packed_in_letc_split] congr 3 · rw [packed_in_unpacked_app_out, <-packed] - · rw [packed_in_pack_coprod_arr]; congr; funext i; rw [packed_in_unpacked_app_out, <-packed] + · rw [packed_in_pack_coprod_arr, unpacked_app_out_pack_coprod] + congr; funext i; rw [packed_in_unpacked_app_out, <-packed, unpacked_app_out_seq, lwk1_acast] theorem Eqv.packed_cfg_split_vwk1 {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G} : (cfg R β G).packed (Δ := Δ) @@ -170,8 +176,8 @@ theorem Eqv.packed_cfg_split_vwk1 {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ (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 + ;; (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] diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean index bc1b61c..6580f94 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean @@ -1,6 +1,7 @@ import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum +import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Cast import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Letc import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Sum import DeBruijnSSA.BinSyntax.Typing.Region.Structural @@ -58,6 +59,11 @@ def Eqv.pack_coprod {Γ : Ctx α ε} {R L : LCtx α} | [] => loop | _::R => coprod (pack_coprod (λi => G i.succ)) (G (0 : Fin (R.length + 1))) +theorem Eqv.pack_coprod_seq {Γ : Ctx α ε} {R L : LCtx α} + {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)} {r : Eqv φ ((A, ⊥)::Γ) (B::L)} + : pack_coprod G ;; r = pack_coprod (λi => (G i) ;; r) + := by induction R <;> simp [pack_coprod, coprod_seq, *] + 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 @@ -577,6 +583,13 @@ 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.vsubst_unpacked_app_out {Γ Δ : Ctx α ε} {R L : LCtx α} + {σ : Term.Subst.Eqv φ Γ Δ} {r : Eqv φ Δ [(R ++ L).pack]} + : r.unpacked_app_out.vsubst σ = (r.vsubst σ).unpacked_app_out := by + rw [unpacked_app_out, vsubst_lsubst, Subst.Eqv.vsubst_unpack_app_out] + rfl + +@[simp] 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, @@ -598,6 +611,11 @@ theorem Eqv.unpacked_app_out_case {Γ : Ctx α ε} {R L : LCtx α} : (case a l r).unpacked_app_out = case a l.unpacked_app_out r.unpacked_app_out := by simp [unpacked_app_out] +theorem Eqv.unpacked_app_out_coprod {Γ : Ctx α ε} {R L : LCtx α} + {l : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} {r : Eqv φ ((B, ⊥)::Γ) [(R ++ L).pack]} + : (coprod l r).unpacked_app_out = coprod l.unpacked_app_out r.unpacked_app_out + := by simp [coprod, unpacked_app_out_case, vwk1_unpacked_app_out] + theorem Eqv.extend_unpack_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ Γ [(R ++ L).pack]} : r.unpacked_app_out.lsubst Subst.Eqv.unpack.extend = r.unpacked_right_out := by @@ -691,20 +709,36 @@ theorem Eqv.packed_out_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α} rw [packed_out_unpacked_app_out_inner] simp [Term.Eqv.sum, ret_of_coprod, sum, ret_of_seq, inj_l_eq_ret, inj_r_eq_ret, seq_assoc] -theorem Eqv.packed_out_unpacked_app_out_ret_seq {Γ : Ctx α ε} {R L : LCtx α} +theorem Eqv.packed_out_unpacked_app_out_ret_seq {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ ((X, ⊥)::Γ) [(R ++ L).pack]} {c : Term.Eqv φ ((R.pack, ⊥)::Γ) (C, ⊥)} : (r.unpacked_app_out ;; ret c).packed_out = r ;; ret Term.Eqv.pack_app ;; sum inj_r (ret c) := by rw [packed_out_binary_ret_seq, packed_out_unpacked_app_out, seq_assoc, sum_seq_sum] simp -theorem Eqv.packed_out_unpacked_app_out_ret_seq_inner {Γ : Ctx α ε} {R L : LCtx α} +theorem Eqv.packed_out_unpacked_app_out_ret_seq_inner {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ ((X, ⊥)::Γ) [(R ++ L).pack]} {c : Term.Eqv φ ((R.pack, ⊥)::Γ) (C, ⊥)} : (r.unpacked_app_out ;; ret c).packed_out = r ;; (ret (Term.Eqv.pack_app ;;' Term.Eqv.sum Term.Eqv.inj_r c)) := by rw [packed_out_unpacked_app_out_ret_seq, ret_of_seq] simp [Term.Eqv.sum, ret_of_coprod, sum, ret_of_seq, inj_l_eq_ret, inj_r_eq_ret, seq_assoc] -end Region - -end BinSyntax +theorem Eqv.unpacked_app_out_pack_coprod {Γ : Ctx α ε} {R L K : LCtx α} + {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) [(L ++ K).pack]} + : (pack_coprod G).unpacked_app_out = pack_coprod (λi => (G i).unpacked_app_out) + := by induction R with + | nil => simp [pack_coprod, unpacked_app_out] + | cons B R I => simp [pack_coprod, unpacked_app_out_coprod, I] + +theorem Eqv.unpacked_app_out_seq {Γ : Ctx α ε} {R L : LCtx α} + {r : Eqv φ ((A, ⊥)::Γ) [B]} {s : Eqv φ ((B, ⊥)::Γ) [(R ++ L).pack]} + : (r ;; s).unpacked_app_out = r.lwk1 ;; s.unpacked_app_out := by + rw [seq, unpacked_app_out, lsubst_lsubst, seq, lwk1, <-lsubst_toSubstE, lsubst_lsubst] + congr 1; 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.get_comp, Subst.Eqv.vlift_unpack_app_out, get_alpha0, + List.length_nil, Fin.val_succ, List.getElem_cons_succ, Fin.cases_zero, Subst.Eqv.get_toSubstE, + Set.mem_setOf_eq, Fin.coe_fin_one, LCtx.InS.coe_wk1, Nat.liftWk_zero, lsubst_br, + List.length_cons, Nat.reduceAdd, Fin.zero_eta, Subst.Eqv.get_vlift, zero_add, vwk_id_eq, + vsubst0_var0_vwk1] + rw [vwk1_unpacked_app_out]; rfl