diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean index 2f68f52..98aae29 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean +++ b/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 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Basic.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Basic.lean new file mode 100644 index 0000000..879386d --- /dev/null +++ b/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 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Product.lean new file mode 100644 index 0000000..dec6b6c --- /dev/null +++ b/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 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural/Sum.lean new file mode 100644 index 0000000..7cfcc5f --- /dev/null +++ b/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 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean index 62012c2..0e24ebd 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean +++ b/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} diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean index 8de0ff1..e7ce74e 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean @@ -1,428 +1,2 @@ -import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Seq -import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum -import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Product -import DeBruijnSSA.BinSyntax.Typing.Term.Structural - - -namespace BinSyntax - -variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε] - -namespace Term - -def Eqv.pack_sum {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) : Eqv φ ((R.get i, ⊥)::Γ) (R.pack, ⊥) - := match R with - | [] => i.elim0 - | _::R => i.cases (inl nil) (λi => inr (pack_sum R i)) - -theorem Eqv.pack_sum_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} - : Eqv.pack_sum (φ := φ) (Γ := Γ) R i = ⟦Term.InS.pack0 R i⟧ := by - induction R generalizing Γ with - | nil => exact i.elim0 - | cons _ _ I => - cases i using Fin.cases with - | zero => rfl - | succ i => - simp only [pack_sum, I, inr_quot, Fin.cases_succ] - apply congrArg - ext - simp [Term.pack0, Term.Wf.pack0, -Function.iterate_succ, Function.iterate_succ'] - -def Eqv.pack {Γ : Ctx α ε} (h : ∀i, Γ.effect i ≤ e) : Eqv φ Γ (Γ.pack, e) := match Γ with - | [] => unit e - | V::Γ => pair - (var 0 (Ctx.Var.head (by constructor; rfl; convert (h 0); simp) _)) - ((pack (Γ := Γ) (λi => by convert h (i + 1) using 1; simp)).wk0) - -theorem Eqv.pack_def {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ e} - : Eqv.pack (φ := φ) (Γ := Γ) h = ⟦Term.InS.pack h⟧ := by - induction Γ with - | nil => rfl - | cons _ _ I => simp only [pack, I]; rfl - -abbrev _root_.BinSyntax.Ctx.Pure.packE {Γ : Ctx α ε} (h : Γ.Pure) : Eqv φ Γ (Γ.pack, ⊥) - := Eqv.pack (e := ⊥) (h := λi => by simp [h.effect i]) - -theorem Eqv.packE_def' {Γ : Ctx α ε} {h : Γ.Pure} : h.packE (φ := φ) = ⟦h.pack⟧ := by - simp only [Ctx.Pure.packE, pack_def] - -theorem Eqv.packE_cons {Γ : Ctx α ε} {h : Ctx.Pure (V::Γ)} - : h.packE (φ := φ) = pair (var 0 (h.any_effect_refl (by simp))) h.tail.packE.wk0 - := rfl - -@[simp] -theorem Eqv.wk_eff_pack {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ lo} {h' : lo ≤ hi} - : (pack (φ := φ) h).wk_eff h' = pack (λi => (h i).trans h') := by - simp [pack_def] - -theorem Eqv.wk_eff_packE {Γ : Ctx α ε} {h : Γ.Pure} - : h.packE.wk_eff bot_le = pack (φ := φ) (e := hi) (λi => by simp [h.effect]) := by simp - -@[simp] -theorem _root_.BinSyntax.Ctx.Pure.packP {Γ : Ctx α ε} (h : Γ.Pure) (h') - : Eqv.Pure (Eqv.pack (φ := φ) (Γ := Γ) (e := e) h') - := ⟨h.packE, by simp⟩ - -def Eqv.pack_drop {Γ Δ : Ctx α ε} (i : Fin Γ.length) - : Eqv φ ((Γ.pack, ⊥)::Δ) (Ctx.pack (Γ.drop i), e) - := ⟦InS.pack_drop i⟧ - -theorem Eqv.Pure.pack_drop {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : Pure (pack_drop (φ := φ) (Δ := Δ) (e := e) i) - := ⟨Eqv.pack_drop i, rfl⟩ - -def Eqv.pack_drop' {Γ Δ : Ctx α ε} (i : Fin Γ.length) - : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1.prod (Ctx.pack (Γ.drop (i + 1))), e) - := ⟦InS.pack_drop' i⟧ - -theorem Eqv.Pure.pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : Pure (pack_drop' (φ := φ) (Δ := Δ) (e := e) i) - := ⟨Eqv.pack_drop' i, rfl⟩ - -theorem Eqv.cast_pack_drop {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (Eqv.pack_drop (φ := φ) (Δ := Δ) (e := e) i).cast rfl (by rw [Ctx.pack_drop_fin]) = pack_drop' i - := rfl - -theorem Eqv.cast_pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (Eqv.pack_drop' (φ := φ) (Δ := Δ) (e := e) i).cast rfl (by rw [<-Ctx.pack_drop_fin]) - = pack_drop i - := rfl - -def Eqv.pack_drop_succ {Γ Δ : Ctx α ε} (i : Fin Γ.length) - : pack_drop (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ - = (pack_drop' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.castSucc).pr := by - simp only [pack_drop, InS.pack_drop_succ]; rfl - -def Eqv.unpack0 {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e) - := ⟦InS.unpack0 i⟧ - -theorem Eqv.Pure.unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : Pure (unpack0 (φ := φ) (Δ := Δ) (e := e) i) - := ⟨Eqv.unpack0 i, rfl⟩ - -@[simp] -theorem Eqv.wk1_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk1 (inserted := inserted) = unpack0 i := by - simp [unpack0] - -@[simp] -theorem Eqv.wk2_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := V::Δ) (e := e) i).wk2 (inserted := inserted) - = unpack0 i := by - simp only [List.get_eq_getElem, wk2, ←Ctx.InS.lift_wk1, unpack0, wk_quot] - apply congrArg - ext - rw [InS.coe_wk, InS.coe_unpack0, InS.coe_unpack0] - exact wk_lift_unpack0 - -@[simp] -theorem Eqv.wk_lift_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} {ρ : Γ.InS Δ} - : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk (ρ.lift (le_refl _)) = unpack0 i := by - simp [unpack0] - -@[simp] -theorem Eqv.subst_lift_unpack0 {Γ Δ Δ' : Ctx α ε} {i : Fin Γ.length} {σ : Subst.Eqv φ Δ' Δ} - : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).subst (σ.lift (le_refl _)) = unpack0 i := by - induction σ using Quotient.inductionOn - simp [unpack0] - -@[simp] -theorem Eqv.subst0_nil_pr_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (Eqv.unpack0 (φ := φ) (Γ := Γ) (e := e) i).subst (nil.pr.subst0) - = unpack0 (φ := φ) (Γ := V::Γ) (Δ := Δ) i.succ := by - apply eq_of_term_eq - apply Term.subst0_nil_pr_unpack0 - -@[simp] -theorem Eqv.subst0_pi_r_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (Eqv.unpack0 (φ := φ) (Γ := Γ) (e := e) i).subst pi_r.subst0 - = unpack0 (φ := φ) (Γ := V::Γ) (Δ := Δ) i.succ := subst0_nil_pr_unpack0 - -theorem Eqv.pl_pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (Eqv.pack_drop' (φ := φ) (Δ := Δ) (e := e) i).pl = unpack0 i := rfl - -theorem Eqv.unpack0_def {Γ Δ : Ctx α ε} (i : Fin Γ.length) : - Eqv.unpack0 (φ := φ) (Δ := Δ) (e := e) i = ⟦Term.InS.unpack0 i⟧ := rfl - -theorem Eqv.unpack0_zero {Γ Δ : Ctx α ε} - : Eqv.unpack0 (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) (0 : Fin (Γ.length + 1)) = pi_l := rfl - -theorem Eqv.unpack0_succ {Γ Δ : Ctx α ε} (i : Fin Γ.length) - : unpack0 (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ = pi_r ;;' unpack0 i := by - rw [seq, <-wk_eff_pi_r, let1_beta, wk1_unpack0, subst0_pi_r_unpack0] - -theorem Eqv.unpack0_one {Γ Δ : Ctx α ε} - : Eqv.unpack0 (φ := φ) (Γ := V::V'::Γ) (Δ := Δ) (e := e) (1 : Fin (Γ.length + 2)) - = pi_r ;;' pi_l := by exact unpack0_succ (Γ := V'::Γ) (0 : Fin (Γ.length + 1)) - -def Eqv.unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e) - := match Γ with - | [] => i.elim0 - | V::Γ => let2 - (var (V := (V.1.prod (Ctx.pack Γ), e)) 0 (by simp [Ctx.pack])) - (i.cases (var 1 (by simp)) (λi => unpack0' i)) - -theorem Eqv.unpack0_def' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : - unpack0' (φ := φ) (Δ := Δ) (e := e) i = ⟦Term.InS.unpack0' i⟧ := by - induction Γ generalizing Δ with - | nil => exact i.elim0 - | cons _ _ I => - simp only [ - List.get_eq_getElem, List.length_cons, unpack0', var, Fin.val_zero, - List.getElem_cons_zero, I, InS.unpack0' - ] - cases i using Fin.cases <;> rfl - -def Subst.Eqv.unpack {Γ Δ : Ctx α ε} : Subst.Eqv φ ((Γ.pack, ⊥)::Δ) Γ := ⟦Subst.InS.unpack⟧ - -@[simp] -theorem Subst.Eqv.get_unpack {Γ Δ : Ctx α ε} {i} - : (unpack (φ := φ) (Γ := Γ) (Δ := Δ)).get i = Eqv.unpack0 i - := rfl - -def _root_.BinSyntax.Ctx.Pure.packSE {Γ} (h : Γ.Pure) : Subst.Eqv φ Γ [(Γ.pack, ⊥)] - := ⟦h.packS⟧ - -@[simp] -theorem Subst.Eqv.get_packSE_zero {Γ : Ctx α ε} (h : Γ.Pure) - : (h.packSE (φ := φ)).get (0 : Fin 1) = h.packE - := by simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero, - List.getElem_cons_zero, Ctx.Pure.packSE, get_quot, Fin.getElem_fin, Ctx.Pure.packE, - Eqv.pack_def]; congr; ext; simp [Ctx.Pure.packS, pack] - -def Eqv.packed {Γ Δ : Ctx α ε} (a : Eqv φ Γ V) : Eqv φ ((Γ.pack, ⊥)::Δ) V - := a.subst Subst.Eqv.unpack - -@[simp] -theorem Eqv.packed_pair {Γ Δ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (A, e)} {b : Eqv φ Γ (B, e)} - : (pair a b).packed (Δ := Δ) = pair a.packed b.packed := by simp [packed] - -def Eqv.unpacked {Γ : Ctx α ε} (a : Eqv φ [(Γ.pack, ⊥)] (A, e)) (h : Γ.Pure) - : Eqv φ Γ (A, e) := let1 (pack (by simp [h.effect])) (a.wk_id (by simp [Ctx.Wkn.drop])) - -theorem Eqv.unpacked_def' {Γ : Ctx α ε} {a : Eqv φ [(Γ.pack, ⊥)] (A, e)} {h : Γ.Pure} - : a.unpacked (φ := φ) (Γ := Γ) h = a.subst h.packSE := by - rw [unpacked, <-wk_eff_packE (h := h), let1_beta, <-wk_eq_wk_id, <-subst_fromWk, subst_subst] - congr - ext k; cases k using Fin.elim1 - simp [Subst.Eqv.get_comp] - -theorem Eqv.packed_wk0 {Γ : Ctx α ε} {a : Eqv φ Γ (A, e)} - : (a.wk0 (head := head)).packed (Δ := Δ) = pi_r ;;' a.packed := by - rw [ - packed, wk0, <-subst_fromWk, subst_subst, seq, <-wk_eff_pi_r, let1_beta, wk1, <-subst_fromWk, - subst_subst, packed, subst_subst - ] - congr 1; ext k - simp only [List.get_eq_getElem, Subst.Eqv.get_comp, Subst.Eqv.get_fromWk, Fin.eta, - Set.mem_setOf_eq, Ctx.InS.coe_wk0, Nat.succ_eq_add_one, subst_var, id_eq, - List.getElem_cons_succ, List.length_cons, Subst.Eqv.get_unpack, wk_res_self, ← subst_subst, - subst_fromWk] - rw [<-wk1, wk1_unpack0, subst0_pi_r_unpack0] - rfl - -theorem Eqv.packed_packE {Γ : Ctx α ε} {h : Γ.Pure} : h.packE.packed (Δ := Δ) = nil (φ := φ) := by - induction Γ generalizing Δ with - | nil => exact Eqv.terminal - | cons V Γ I => - rw [packE_cons, packed_pair] - convert Eqv.Pure.pair_eta _ - · rfl - · simp [packed_wk0, I]; rfl - · simp - -@[simp] -theorem Subst.Eqv.unpack_comp_packSE {Γ : Ctx α ε} (h : Γ.Pure) - : unpack.comp h.packSE = Subst.Eqv.id (φ := φ) := by - 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, get_comp, get_packSE_zero, get_id, Fin.coe_fin_one] - exact Eqv.packed_packE - -theorem Eqv.unpack0_eq_unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : - Eqv.unpack0 (φ := φ) (Δ := Δ) (e := e) i = Eqv.unpack0' i := by - induction Γ generalizing Δ with - | nil => exact i.elim0 - | cons V Γ I => - simp only [List.length_cons] at i - cases i using Fin.cases with - | zero => rfl - | succ => - simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, - unpack0', Fin.val_zero, List.getElem_cons_zero, Fin.cases_succ, <-I] - rw [<-wk1_unpack0, <-wk1_unpack0, <-nil, <-pi_r_seq, unpack0_succ] - -theorem Eqv.unpacked_unpack0 {Γ : Ctx α ε} {h : Γ.Pure} {i} - : (Eqv.unpack0 (φ := φ) (e := e) i).unpacked h = var i (h.any_effect_refl i.prop) - := by induction Γ with - | nil => exact i.elim0 - | cons V Γ I => cases i using Fin.cases with - | zero => - simp [unpack0_zero, unpacked_def', pi_l, nil, subst_var, pl, Subst.Eqv.get_liftn₂_one] - rw [<-pl, pack, Pure.pl_pair] - exact Pure.wk0 ⟨h.tail.packE, by simp⟩ - | succ i => - rw [unpacked_def', unpack0_succ, seq] - simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, - wk1_unpack0, subst_let1, subst_lift_unpack0] - simp [pi_r, pr, nil, subst_var] - rw [<-pr, pack, Pure.pr_pair, <-wk1_unpack0, <-wk0_let1, <-wk0_var] - apply congrArg - exact I (h := h.tail) - exact ⟨var 0 (h.any_effect_refl (by simp)), rfl⟩ - -@[simp] -theorem Subst.Eqv.packSE_comp_unpack {Γ : Ctx α ε} (h : Γ.Pure) - : h.packSE.comp unpack = Subst.Eqv.id (φ := φ) := by - ext k; simp only [List.get_eq_getElem, get_comp, get_unpack, get_id] - rw [<-Eqv.unpacked_unpack0, Eqv.unpacked_def'] - -theorem Eqv.packed_unpacked {Γ : Ctx α ε} {a : Eqv φ [(Γ.pack, ⊥)] (A, e)} {h : Γ.Pure} - : (a.unpacked h).packed = a := by simp [unpacked_def', packed, subst_subst] - -theorem Eqv.unpacked_packed {Γ : Ctx α ε} {a : Eqv φ Γ (A, e)} {h : Γ.Pure} - : a.packed.unpacked h = a := by simp [unpacked_def', packed, subst_subst] - -theorem Eqv.packed_injective {Γ : Ctx α ε} {a b : Eqv φ Γ V} (hΓ : Γ.Pure) - (h : a.packed (Δ := []) = b.packed) : a = b := by - rw [<-unpacked_packed (a := a), <-unpacked_packed (a := b), h]; exact hΓ - -theorem Eqv.unpacked_injective {Γ : Ctx α ε} {a b : Eqv φ [(Γ.pack, ⊥)] (A, e)} {hΓ : Γ.Pure} - (h : a.unpacked hΓ = b.unpacked hΓ) : a = b := by - rw [<-packed_unpacked (a := a), <-packed_unpacked (a := b), h] - -@[simp] -theorem Eqv.packed_var {Γ : Ctx α ε} {i} {hv} - : (var (V := V) i hv).packed (Δ := Δ) - = (unpack0 (φ := φ) (Γ := Γ) ⟨i, hv.length⟩).wk_res hv.get := by simp [packed, subst_var] - -theorem Subst.Eqv.lift_unpack {Γ Δ : Ctx α ε} - : (unpack (φ := φ) (Γ := Γ) (Δ := Δ)).lift (le_refl (A, ⊥)) - = ((Eqv.var 0 (by simp)).pair (Eqv.var 1 (by simp))).subst0.comp Subst.Eqv.unpack := by - ext k - cases k using Fin.cases with - | zero => - simp [ - Subst.Eqv.get_comp, Eqv.unpack0_zero, Eqv.pi_l, Eqv.nil, Eqv.pl, Eqv.let2_pair, - Eqv.let1_beta_var0, Eqv.let1_beta_var1] - | succ k => - simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, - get_lift_succ, get_unpack, get_comp, Eqv.unpack0_succ, Eqv.seq, Eqv.pi_r, Eqv.pr, Eqv.nil, - Eqv.wk1_unpack0, Eqv.subst_let1, Eqv.subst_let2, Eqv.var0_subst0, Fin.zero_eta, Fin.val_zero, - List.getElem_cons_zero, Eqv.wk_res_eff, Eqv.wk_eff_pair, Eqv.wk_eff_var, ge_iff_le, - Prod.mk_le_mk, le_refl, bot_le, and_self, Eqv.subst_liftn₂_var_zero, Eqv.let2_pair, - Eqv.wk0_var, Nat.reduceAdd, Eqv.let1_beta_var0, Eqv.var_succ_subst0, Eqv.subst_lift_var_zero, - Eqv.let1_beta_var1, Nat.add_zero, Nat.zero_eq, Eqv.subst_lift_unpack0] - rw [Eqv.wk0, <-Eqv.subst_fromWk] - apply Eqv.eq_of_term_eq - apply subst_eqOn_fvi - intro i - simp only [InS.coe_unpack0, fvi_unpack0] - simp only [Set.mem_Iio, Nat.lt_one_iff, Set.mem_setOf_eq, Ctx.InS.coe_toSubst, Ctx.InS.coe_wk0, - Subst.fromWk_apply, Nat.succ_eq_add_one, InS.coe_subst0, InS.coe_var] - intro i; cases i; rfl - -theorem Subst.Eqv.liftn₂_unpack {Γ Δ : Ctx α ε} - : (unpack (φ := φ) (Γ := Γ) (Δ := Δ)).liftn₂ (le_refl (A, ⊥)) (le_refl (B, ⊥)) - = (Eqv.pair (Eqv.var 0 (by simp)) - (Eqv.pair (Eqv.var 1 (by simp)) (Eqv.var 2 (by simp)))).subst0.comp Subst.Eqv.unpack := by - ext k - cases k using Fin.cases with - | zero => - simp only [List.get_eq_getElem, List.length_cons, Fin.val_zero, List.getElem_cons_zero, - get_liftn₂_zero, get_comp, get_unpack, Eqv.unpack0_zero, Eqv.pi_l, Eqv.pl, Eqv.nil, - Eqv.subst_let2, Eqv.var0_subst0, Fin.zero_eta, Eqv.wk_res_self, Eqv.subst_liftn₂_var_one, - Eqv.let2_pair, Eqv.wk0_pair, Eqv.wk0_var, Nat.reduceAdd, Eqv.let1_beta_var0, Eqv.subst_let1, - Eqv.subst_pair, Eqv.var_succ_subst0, Eqv.subst_lift_var_succ, zero_add] - rw [Eqv.let1_beta' - (a' := (Eqv.pair (Eqv.var 1 (by simp)) (Eqv.var 2 (by simp)))) (h := by simp)] - rfl - | succ k => - cases k using Fin.cases with - | zero => - simp [ - Subst.Eqv.get_comp, Eqv.unpack0_zero, Eqv.pi_l, Eqv.nil, Eqv.pl, Eqv.let2_pair, - Eqv.let1_beta_var0, get_liftn₂_one, - ] - rw [Eqv.unpack0_one, Eqv.seq_pi_l] - simp only [Eqv.pi_r, Eqv.subst_pl, Eqv.subst_pr, Eqv.nil_subst0, Eqv.wk_eff_self] - rw [Eqv.Pure.pr_pair, Eqv.Pure.pl_pair] <;> simp - | succ k => - simp only [List.length_cons, List.get_eq_getElem, Fin.val_succ, List.getElem_cons_succ, - get_liftn₂_succ, get_lift_succ, get_unpack, get_comp] - rw [Eqv.unpack0_succ (Γ := _::Γ) (i := k.succ)] - rw [Eqv.unpack0_succ] - simp only [Eqv.seq, List.get_eq_getElem, List.length_cons, Fin.val_succ, - List.getElem_cons_succ, Eqv.pi_r, Eqv.nil, Eqv.wk1_unpack0, Eqv.wk1_let1, Eqv.wk1_pr, - Eqv.wk1_var0, Fin.zero_eta, Fin.val_zero, List.getElem_cons_zero, Eqv.wk2_unpack0, - Eqv.subst_let1, Eqv.subst_pr, Eqv.var0_subst0, Eqv.wk_res_eff, Eqv.wk_eff_pair, - Eqv.wk_eff_var, Eqv.subst_lift_var_zero, Eqv.subst_lift_unpack0] - rw [Eqv.Pure.pr_pair] - rw [Eqv.let1_beta' - (a' := (Eqv.pair (Eqv.var 1 (by simp)) (Eqv.var 2 (by simp)))) (h := by simp)] - simp only [Eqv.subst_let1, Eqv.subst_pr, Eqv.var0_subst0, List.length_cons, Nat.add_zero, - Nat.zero_eq, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, - Eqv.wk_res_eff, Eqv.wk_eff_pair, Eqv.wk_eff_var, Eqv.subst_lift_unpack0] - rw [Eqv.Pure.pr_pair, Eqv.let1_beta_var2, Eqv.wk0, Eqv.wk0, Eqv.wk_wk, <-Eqv.subst_fromWk] - apply Eqv.eq_of_term_eq - apply subst_eqOn_fvi - intro i - rw [InS.coe_unpack0, fvi_unpack0] - simp only [Set.mem_Iio, Nat.lt_one_iff, Set.mem_setOf_eq, Ctx.InS.coe_toSubst, - Ctx.InS.coe_comp, Ctx.InS.coe_wk0, fromWk_apply, Function.comp_apply, Nat.succ_eq_add_one, - InS.coe_subst0, Term.InS.coe_var] - intro h; cases h; rfl - exact ⟨Eqv.var 1 (by simp), rfl⟩ - exact ⟨Eqv.var 0 (by simp), rfl⟩ - -theorem Eqv.packed_let1 {Γ : Ctx α ε} {A B : Ty α} - {a : Eqv φ Γ (A, e)} {b : Eqv φ ((A, ⊥)::Γ) (B, e)} - : (let1 a b).packed (Δ := Δ) - = let1 a.packed (let1 (pair (var 0 (by simp)) (var 1 (by simp))) b.packed) := by - rw [packed, subst_let1]; apply congrArg - rw [ - packed, let1_beta' (a' := pair (var 0 (by simp)) (var 1 (by simp))) (h := by simp), - subst_subst, Subst.Eqv.lift_unpack - ] - -theorem Eqv.packed_let2 {Γ : Ctx α ε} {A B C : Ty α} - {a : Eqv φ Γ (A.prod B, e)} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) (C, e)} - : (let2 a b).packed (Δ := Δ) - = let2 a.packed ( - let1 (pair (var 0 (by simp)) (pair (var 1 (by simp)) (var 2 (by simp)))) b.packed) := by - rw [packed, subst_let2]; congr - rw [ - packed, - let1_beta' - (a' := (pair (var 0 (by simp)) (pair (var 1 (by simp)) (var 2 (by simp))))) (h := by simp), - subst_subst, Subst.Eqv.liftn₂_unpack, - ] - -theorem Eqv.packed_case {Γ : Ctx α ε} {A B : Ty α} - {a : Eqv φ Γ (A.coprod B, e)} {l : Eqv φ ((A, ⊥)::Γ) (C, e)} {r : Eqv φ ((B, ⊥)::Γ) (C, e)} - : (case a l r).packed (Δ := Δ) - = case a.packed - (let1 (pair (var 0 (by simp)) (var 1 (by simp))) l.packed) - (let1 (pair (var 0 (by simp)) (var 1 (by simp))) r.packed) := by - rw [packed, subst_case]; congr <;> rw [ - packed, let1_beta' (a' := pair (var 0 (by simp)) (var 1 (by simp))) (h := by simp), - subst_subst, Subst.Eqv.lift_unpack - ] - -@[simp] -theorem Eqv.packed_inl {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (A, e)} - : (inl (B := B) a).packed (Δ := Δ) = inl a.packed := by simp [packed] - -@[simp] -theorem Eqv.packed_inr {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (B, e)} - : (inr (A := A) a).packed (Δ := Δ) = inr a.packed := by simp [packed] - -@[simp] -theorem Eqv.packed_abort {Γ : Ctx α ε} {A : Ty α} {a : Eqv φ Γ (Ty.empty, e)} - : (abort a A).packed (Δ := Δ) = abort a.packed A := by simp [packed] - -@[simp] -theorem Eqv.packed_unit {Γ : Ctx α ε} : (unit (φ := φ) (Γ := Γ) (e := e)).packed (Δ := Δ) = unit _ - := rfl - -end Term +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Sum +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Product diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural/Product.lean new file mode 100644 index 0000000..2f25a85 --- /dev/null +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural/Product.lean @@ -0,0 +1,409 @@ +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Seq +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Product +import DeBruijnSSA.BinSyntax.Typing.Term.Structural + +namespace BinSyntax + +variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε] + +namespace Term + +def Eqv.pack {Γ : Ctx α ε} (h : ∀i, Γ.effect i ≤ e) : Eqv φ Γ (Γ.pack, e) := match Γ with + | [] => unit e + | V::Γ => pair + (var 0 (Ctx.Var.head (by constructor; rfl; convert (h 0); simp) _)) + ((pack (Γ := Γ) (λi => by convert h (i + 1) using 1; simp)).wk0) + +theorem Eqv.pack_def {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ e} + : Eqv.pack (φ := φ) (Γ := Γ) h = ⟦Term.InS.pack h⟧ := by + induction Γ with + | nil => rfl + | cons _ _ I => simp only [pack, I]; rfl + +abbrev _root_.BinSyntax.Ctx.Pure.packE {Γ : Ctx α ε} (h : Γ.Pure) : Eqv φ Γ (Γ.pack, ⊥) + := Eqv.pack (e := ⊥) (h := λi => by simp [h.effect i]) + +theorem Eqv.packE_def' {Γ : Ctx α ε} {h : Γ.Pure} : h.packE (φ := φ) = ⟦h.pack⟧ := by + simp only [Ctx.Pure.packE, pack_def] + +theorem Eqv.packE_cons {Γ : Ctx α ε} {h : Ctx.Pure (V::Γ)} + : h.packE (φ := φ) = pair (var 0 (h.any_effect_refl (by simp))) h.tail.packE.wk0 + := rfl + +@[simp] +theorem Eqv.wk_eff_pack {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ lo} {h' : lo ≤ hi} + : (pack (φ := φ) h).wk_eff h' = pack (λi => (h i).trans h') := by + simp [pack_def] + +theorem Eqv.wk_eff_packE {Γ : Ctx α ε} {h : Γ.Pure} + : h.packE.wk_eff bot_le = pack (φ := φ) (e := hi) (λi => by simp [h.effect]) := by simp + +@[simp] +theorem _root_.BinSyntax.Ctx.Pure.packP {Γ : Ctx α ε} (h : Γ.Pure) (h') + : Eqv.Pure (Eqv.pack (φ := φ) (Γ := Γ) (e := e) h') + := ⟨h.packE, by simp⟩ + +def Eqv.pack_drop {Γ Δ : Ctx α ε} (i : Fin Γ.length) + : Eqv φ ((Γ.pack, ⊥)::Δ) (Ctx.pack (Γ.drop i), e) + := ⟦InS.pack_drop i⟧ + +theorem Eqv.Pure.pack_drop {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : Pure (pack_drop (φ := φ) (Δ := Δ) (e := e) i) + := ⟨Eqv.pack_drop i, rfl⟩ + +def Eqv.pack_drop' {Γ Δ : Ctx α ε} (i : Fin Γ.length) + : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1.prod (Ctx.pack (Γ.drop (i + 1))), e) + := ⟦InS.pack_drop' i⟧ + +theorem Eqv.Pure.pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : Pure (pack_drop' (φ := φ) (Δ := Δ) (e := e) i) + := ⟨Eqv.pack_drop' i, rfl⟩ + +theorem Eqv.cast_pack_drop {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (Eqv.pack_drop (φ := φ) (Δ := Δ) (e := e) i).cast rfl (by rw [Ctx.pack_drop_fin]) = pack_drop' i + := rfl + +theorem Eqv.cast_pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (Eqv.pack_drop' (φ := φ) (Δ := Δ) (e := e) i).cast rfl (by rw [<-Ctx.pack_drop_fin]) + = pack_drop i + := rfl + +def Eqv.pack_drop_succ {Γ Δ : Ctx α ε} (i : Fin Γ.length) + : pack_drop (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ + = (pack_drop' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.castSucc).pr := by + simp only [pack_drop, InS.pack_drop_succ]; rfl + +def Eqv.proj_n {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e) + := ⟦InS.proj_n i⟧ + +theorem Eqv.Pure.proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : Pure (proj_n (φ := φ) (Δ := Δ) (e := e) i) + := ⟨Eqv.proj_n i, rfl⟩ + +@[simp] +theorem Eqv.wk1_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (Eqv.proj_n (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk1 (inserted := inserted) = proj_n i := by + simp [proj_n] + +@[simp] +theorem Eqv.wk2_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (Eqv.proj_n (φ := φ) (Γ := Γ) (Δ := V::Δ) (e := e) i).wk2 (inserted := inserted) + = proj_n i := by + simp only [List.get_eq_getElem, wk2, ←Ctx.InS.lift_wk1, proj_n, wk_quot] + apply congrArg + ext + rw [InS.coe_wk, InS.coe_proj_n, InS.coe_proj_n] + exact wk_lift_proj_n + +@[simp] +theorem Eqv.wk_lift_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} {ρ : Γ.InS Δ} + : (Eqv.proj_n (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk (ρ.lift (le_refl _)) = proj_n i := by + simp [proj_n] + +@[simp] +theorem Eqv.subst_lift_proj_n {Γ Δ Δ' : Ctx α ε} {i : Fin Γ.length} {σ : Subst.Eqv φ Δ' Δ} + : (Eqv.proj_n (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).subst (σ.lift (le_refl _)) = proj_n i := by + induction σ using Quotient.inductionOn + simp [proj_n] + +@[simp] +theorem Eqv.subst0_nil_pr_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (Eqv.proj_n (φ := φ) (Γ := Γ) (e := e) i).subst (nil.pr.subst0) + = proj_n (φ := φ) (Γ := V::Γ) (Δ := Δ) i.succ := by + apply eq_of_term_eq + apply Term.subst0_nil_pr_proj_n + +@[simp] +theorem Eqv.subst0_pi_r_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (Eqv.proj_n (φ := φ) (Γ := Γ) (e := e) i).subst pi_r.subst0 + = proj_n (φ := φ) (Γ := V::Γ) (Δ := Δ) i.succ := subst0_nil_pr_proj_n + +theorem Eqv.pl_pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (Eqv.pack_drop' (φ := φ) (Δ := Δ) (e := e) i).pl = proj_n i := rfl + +theorem Eqv.proj_n_def {Γ Δ : Ctx α ε} (i : Fin Γ.length) : + Eqv.proj_n (φ := φ) (Δ := Δ) (e := e) i = ⟦Term.InS.proj_n i⟧ := rfl + +theorem Eqv.proj_n_zero {Γ Δ : Ctx α ε} + : Eqv.proj_n (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) (0 : Fin (Γ.length + 1)) = pi_l := rfl + +theorem Eqv.proj_n_succ {Γ Δ : Ctx α ε} (i : Fin Γ.length) + : proj_n (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ = pi_r ;;' proj_n i := by + rw [seq, <-wk_eff_pi_r, let1_beta, wk1_proj_n, subst0_pi_r_proj_n] + +theorem Eqv.proj_n_one {Γ Δ : Ctx α ε} + : Eqv.proj_n (φ := φ) (Γ := V::V'::Γ) (Δ := Δ) (e := e) (1 : Fin (Γ.length + 2)) + = pi_r ;;' pi_l := by exact proj_n_succ (Γ := V'::Γ) (0 : Fin (Γ.length + 1)) + +def Eqv.proj_n' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Eqv φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e) + := match Γ with + | [] => i.elim0 + | V::Γ => let2 + (var (V := (V.1.prod (Ctx.pack Γ), e)) 0 (by simp [Ctx.pack])) + (i.cases (var 1 (by simp)) (λi => proj_n' i)) + +theorem Eqv.proj_n_def' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : + proj_n' (φ := φ) (Δ := Δ) (e := e) i = ⟦Term.InS.proj_n' i⟧ := by + induction Γ generalizing Δ with + | nil => exact i.elim0 + | cons _ _ I => + simp only [ + List.get_eq_getElem, List.length_cons, proj_n', var, Fin.val_zero, + List.getElem_cons_zero, I, InS.proj_n' + ] + cases i using Fin.cases <;> rfl + +def Subst.Eqv.unpack {Γ Δ : Ctx α ε} : Subst.Eqv φ ((Γ.pack, ⊥)::Δ) Γ := ⟦Subst.InS.unpack⟧ + +@[simp] +theorem Subst.Eqv.get_unpack {Γ Δ : Ctx α ε} {i} + : (unpack (φ := φ) (Γ := Γ) (Δ := Δ)).get i = Eqv.proj_n i + := rfl + +def _root_.BinSyntax.Ctx.Pure.packSE {Γ} (h : Γ.Pure) : Subst.Eqv φ Γ [(Γ.pack, ⊥)] + := ⟦h.packS⟧ + +@[simp] +theorem Subst.Eqv.get_packSE_zero {Γ : Ctx α ε} (h : Γ.Pure) + : (h.packSE (φ := φ)).get (0 : Fin 1) = h.packE + := by simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero, + List.getElem_cons_zero, Ctx.Pure.packSE, get_quot, Fin.getElem_fin, Ctx.Pure.packE, + Eqv.pack_def]; congr; ext; simp [Ctx.Pure.packS, pack] + +def Eqv.packed {Γ Δ : Ctx α ε} (a : Eqv φ Γ V) : Eqv φ ((Γ.pack, ⊥)::Δ) V + := a.subst Subst.Eqv.unpack + +@[simp] +theorem Eqv.packed_pair {Γ Δ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (A, e)} {b : Eqv φ Γ (B, e)} + : (pair a b).packed (Δ := Δ) = pair a.packed b.packed := by simp [packed] + +def Eqv.unpacked {Γ : Ctx α ε} (a : Eqv φ [(Γ.pack, ⊥)] (A, e)) (h : Γ.Pure) + : Eqv φ Γ (A, e) := let1 (pack (by simp [h.effect])) (a.wk_id (by simp [Ctx.Wkn.drop])) + +theorem Eqv.unpacked_def' {Γ : Ctx α ε} {a : Eqv φ [(Γ.pack, ⊥)] (A, e)} {h : Γ.Pure} + : a.unpacked (φ := φ) (Γ := Γ) h = a.subst h.packSE := by + rw [unpacked, <-wk_eff_packE (h := h), let1_beta, <-wk_eq_wk_id, <-subst_fromWk, subst_subst] + congr + ext k; cases k using Fin.elim1 + simp [Subst.Eqv.get_comp] + +theorem Eqv.packed_wk0 {Γ : Ctx α ε} {a : Eqv φ Γ (A, e)} + : (a.wk0 (head := head)).packed (Δ := Δ) = pi_r ;;' a.packed := by + rw [ + packed, wk0, <-subst_fromWk, subst_subst, seq, <-wk_eff_pi_r, let1_beta, wk1, <-subst_fromWk, + subst_subst, packed, subst_subst + ] + congr 1; ext k + simp only [List.get_eq_getElem, Subst.Eqv.get_comp, Subst.Eqv.get_fromWk, Fin.eta, + Set.mem_setOf_eq, Ctx.InS.coe_wk0, Nat.succ_eq_add_one, subst_var, id_eq, + List.getElem_cons_succ, List.length_cons, Subst.Eqv.get_unpack, wk_res_self, ← subst_subst, + subst_fromWk] + rw [<-wk1, wk1_proj_n, subst0_pi_r_proj_n] + rfl + +theorem Eqv.packed_packE {Γ : Ctx α ε} {h : Γ.Pure} : h.packE.packed (Δ := Δ) = nil (φ := φ) := by + induction Γ generalizing Δ with + | nil => exact Eqv.terminal + | cons V Γ I => + rw [packE_cons, packed_pair] + convert Eqv.Pure.pair_eta _ + · rfl + · simp [packed_wk0, I]; rfl + · simp + +@[simp] +theorem Subst.Eqv.unpack_comp_packSE {Γ : Ctx α ε} (h : Γ.Pure) + : unpack.comp h.packSE = Subst.Eqv.id (φ := φ) := by + 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, get_comp, get_packSE_zero, get_id, Fin.coe_fin_one] + exact Eqv.packed_packE + +theorem Eqv.proj_n_eq_proj_n' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : + Eqv.proj_n (φ := φ) (Δ := Δ) (e := e) i = Eqv.proj_n' i := by + induction Γ generalizing Δ with + | nil => exact i.elim0 + | cons V Γ I => + simp only [List.length_cons] at i + cases i using Fin.cases with + | zero => rfl + | succ => + simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, + proj_n', Fin.val_zero, List.getElem_cons_zero, Fin.cases_succ, <-I] + rw [<-wk1_proj_n, <-wk1_proj_n, <-nil, <-pi_r_seq, proj_n_succ] + +theorem Eqv.unpacked_proj_n {Γ : Ctx α ε} {h : Γ.Pure} {i} + : (Eqv.proj_n (φ := φ) (e := e) i).unpacked h = var i (h.any_effect_refl i.prop) + := by induction Γ with + | nil => exact i.elim0 + | cons V Γ I => cases i using Fin.cases with + | zero => + simp [proj_n_zero, unpacked_def', pi_l, nil, subst_var, pl, Subst.Eqv.get_liftn₂_one] + rw [<-pl, pack, Pure.pl_pair] + exact Pure.wk0 ⟨h.tail.packE, by simp⟩ + | succ i => + rw [unpacked_def', proj_n_succ, seq] + simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, + wk1_proj_n, subst_let1, subst_lift_proj_n] + simp [pi_r, pr, nil, subst_var] + rw [<-pr, pack, Pure.pr_pair, <-wk1_proj_n, <-wk0_let1, <-wk0_var] + apply congrArg + exact I (h := h.tail) + exact ⟨var 0 (h.any_effect_refl (by simp)), rfl⟩ + +@[simp] +theorem Subst.Eqv.packSE_comp_unpack {Γ : Ctx α ε} (h : Γ.Pure) + : h.packSE.comp unpack = Subst.Eqv.id (φ := φ) := by + ext k; simp only [List.get_eq_getElem, get_comp, get_unpack, get_id] + rw [<-Eqv.unpacked_proj_n, Eqv.unpacked_def'] + +theorem Eqv.packed_unpacked {Γ : Ctx α ε} {a : Eqv φ [(Γ.pack, ⊥)] (A, e)} {h : Γ.Pure} + : (a.unpacked h).packed = a := by simp [unpacked_def', packed, subst_subst] + +theorem Eqv.unpacked_packed {Γ : Ctx α ε} {a : Eqv φ Γ (A, e)} {h : Γ.Pure} + : a.packed.unpacked h = a := by simp [unpacked_def', packed, subst_subst] + +theorem Eqv.packed_injective {Γ : Ctx α ε} {a b : Eqv φ Γ V} (hΓ : Γ.Pure) + (h : a.packed (Δ := []) = b.packed) : a = b := by + rw [<-unpacked_packed (a := a), <-unpacked_packed (a := b), h]; exact hΓ + +theorem Eqv.unpacked_injective {Γ : Ctx α ε} {a b : Eqv φ [(Γ.pack, ⊥)] (A, e)} {hΓ : Γ.Pure} + (h : a.unpacked hΓ = b.unpacked hΓ) : a = b := by + rw [<-packed_unpacked (a := a), <-packed_unpacked (a := b), h] + +@[simp] +theorem Eqv.packed_var {Γ : Ctx α ε} {i} {hv} + : (var (V := V) i hv).packed (Δ := Δ) + = (proj_n (φ := φ) (Γ := Γ) ⟨i, hv.length⟩).wk_res hv.get := by simp [packed, subst_var] + +theorem Subst.Eqv.lift_unpack {Γ Δ : Ctx α ε} + : (unpack (φ := φ) (Γ := Γ) (Δ := Δ)).lift (le_refl (A, ⊥)) + = ((Eqv.var 0 (by simp)).pair (Eqv.var 1 (by simp))).subst0.comp Subst.Eqv.unpack := by + ext k + cases k using Fin.cases with + | zero => + simp [ + Subst.Eqv.get_comp, Eqv.proj_n_zero, Eqv.pi_l, Eqv.nil, Eqv.pl, Eqv.let2_pair, + Eqv.let1_beta_var0, Eqv.let1_beta_var1] + | succ k => + simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, + get_lift_succ, get_unpack, get_comp, Eqv.proj_n_succ, Eqv.seq, Eqv.pi_r, Eqv.pr, Eqv.nil, + Eqv.wk1_proj_n, Eqv.subst_let1, Eqv.subst_let2, Eqv.var0_subst0, Fin.zero_eta, Fin.val_zero, + List.getElem_cons_zero, Eqv.wk_res_eff, Eqv.wk_eff_pair, Eqv.wk_eff_var, ge_iff_le, + Prod.mk_le_mk, le_refl, bot_le, and_self, Eqv.subst_liftn₂_var_zero, Eqv.let2_pair, + Eqv.wk0_var, Nat.reduceAdd, Eqv.let1_beta_var0, Eqv.var_succ_subst0, Eqv.subst_lift_var_zero, + Eqv.let1_beta_var1, Nat.add_zero, Nat.zero_eq, Eqv.subst_lift_proj_n] + rw [Eqv.wk0, <-Eqv.subst_fromWk] + apply Eqv.eq_of_term_eq + apply subst_eqOn_fvi + intro i + simp only [InS.coe_proj_n, fvi_proj_n] + simp only [Set.mem_Iio, Nat.lt_one_iff, Set.mem_setOf_eq, Ctx.InS.coe_toSubst, Ctx.InS.coe_wk0, + Subst.fromWk_apply, Nat.succ_eq_add_one, InS.coe_subst0, InS.coe_var] + intro i; cases i; rfl + +theorem Subst.Eqv.liftn₂_unpack {Γ Δ : Ctx α ε} + : (unpack (φ := φ) (Γ := Γ) (Δ := Δ)).liftn₂ (le_refl (A, ⊥)) (le_refl (B, ⊥)) + = (Eqv.pair (Eqv.var 0 (by simp)) + (Eqv.pair (Eqv.var 1 (by simp)) (Eqv.var 2 (by simp)))).subst0.comp Subst.Eqv.unpack := by + ext k + cases k using Fin.cases with + | zero => + simp only [List.get_eq_getElem, List.length_cons, Fin.val_zero, List.getElem_cons_zero, + get_liftn₂_zero, get_comp, get_unpack, Eqv.proj_n_zero, Eqv.pi_l, Eqv.pl, Eqv.nil, + Eqv.subst_let2, Eqv.var0_subst0, Fin.zero_eta, Eqv.wk_res_self, Eqv.subst_liftn₂_var_one, + Eqv.let2_pair, Eqv.wk0_pair, Eqv.wk0_var, Nat.reduceAdd, Eqv.let1_beta_var0, Eqv.subst_let1, + Eqv.subst_pair, Eqv.var_succ_subst0, Eqv.subst_lift_var_succ, zero_add] + rw [Eqv.let1_beta' + (a' := (Eqv.pair (Eqv.var 1 (by simp)) (Eqv.var 2 (by simp)))) (h := by simp)] + rfl + | succ k => + cases k using Fin.cases with + | zero => + simp [ + Subst.Eqv.get_comp, Eqv.proj_n_zero, Eqv.pi_l, Eqv.nil, Eqv.pl, Eqv.let2_pair, + Eqv.let1_beta_var0, get_liftn₂_one, + ] + rw [Eqv.proj_n_one, Eqv.seq_pi_l] + simp only [Eqv.pi_r, Eqv.subst_pl, Eqv.subst_pr, Eqv.nil_subst0, Eqv.wk_eff_self] + rw [Eqv.Pure.pr_pair, Eqv.Pure.pl_pair] <;> simp + | succ k => + simp only [List.length_cons, List.get_eq_getElem, Fin.val_succ, List.getElem_cons_succ, + get_liftn₂_succ, get_lift_succ, get_unpack, get_comp] + rw [Eqv.proj_n_succ (Γ := _::Γ) (i := k.succ)] + rw [Eqv.proj_n_succ] + simp only [Eqv.seq, List.get_eq_getElem, List.length_cons, Fin.val_succ, + List.getElem_cons_succ, Eqv.pi_r, Eqv.nil, Eqv.wk1_proj_n, Eqv.wk1_let1, Eqv.wk1_pr, + Eqv.wk1_var0, Fin.zero_eta, Fin.val_zero, List.getElem_cons_zero, Eqv.wk2_proj_n, + Eqv.subst_let1, Eqv.subst_pr, Eqv.var0_subst0, Eqv.wk_res_eff, Eqv.wk_eff_pair, + Eqv.wk_eff_var, Eqv.subst_lift_var_zero, Eqv.subst_lift_proj_n] + rw [Eqv.Pure.pr_pair] + rw [Eqv.let1_beta' + (a' := (Eqv.pair (Eqv.var 1 (by simp)) (Eqv.var 2 (by simp)))) (h := by simp)] + simp only [Eqv.subst_let1, Eqv.subst_pr, Eqv.var0_subst0, List.length_cons, Nat.add_zero, + Nat.zero_eq, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, + Eqv.wk_res_eff, Eqv.wk_eff_pair, Eqv.wk_eff_var, Eqv.subst_lift_proj_n] + rw [Eqv.Pure.pr_pair, Eqv.let1_beta_var2, Eqv.wk0, Eqv.wk0, Eqv.wk_wk, <-Eqv.subst_fromWk] + apply Eqv.eq_of_term_eq + apply subst_eqOn_fvi + intro i + rw [InS.coe_proj_n, fvi_proj_n] + simp only [Set.mem_Iio, Nat.lt_one_iff, Set.mem_setOf_eq, Ctx.InS.coe_toSubst, + Ctx.InS.coe_comp, Ctx.InS.coe_wk0, fromWk_apply, Function.comp_apply, Nat.succ_eq_add_one, + InS.coe_subst0, Term.InS.coe_var] + intro h; cases h; rfl + exact ⟨Eqv.var 1 (by simp), rfl⟩ + exact ⟨Eqv.var 0 (by simp), rfl⟩ + +theorem Eqv.packed_let1 {Γ : Ctx α ε} {A B : Ty α} + {a : Eqv φ Γ (A, e)} {b : Eqv φ ((A, ⊥)::Γ) (B, e)} + : (let1 a b).packed (Δ := Δ) + = let1 a.packed (let1 (pair (var 0 (by simp)) (var 1 (by simp))) b.packed) := by + rw [packed, subst_let1]; apply congrArg + rw [ + packed, let1_beta' (a' := pair (var 0 (by simp)) (var 1 (by simp))) (h := by simp), + subst_subst, Subst.Eqv.lift_unpack + ] + +theorem Eqv.packed_let2 {Γ : Ctx α ε} {A B C : Ty α} + {a : Eqv φ Γ (A.prod B, e)} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) (C, e)} + : (let2 a b).packed (Δ := Δ) + = let2 a.packed ( + let1 (pair (var 0 (by simp)) (pair (var 1 (by simp)) (var 2 (by simp)))) b.packed) := by + rw [packed, subst_let2]; congr + rw [ + packed, + let1_beta' + (a' := (pair (var 0 (by simp)) (pair (var 1 (by simp)) (var 2 (by simp))))) (h := by simp), + subst_subst, Subst.Eqv.liftn₂_unpack, + ] + +theorem Eqv.packed_case {Γ : Ctx α ε} {A B : Ty α} + {a : Eqv φ Γ (A.coprod B, e)} {l : Eqv φ ((A, ⊥)::Γ) (C, e)} {r : Eqv φ ((B, ⊥)::Γ) (C, e)} + : (case a l r).packed (Δ := Δ) + = case a.packed + (let1 (pair (var 0 (by simp)) (var 1 (by simp))) l.packed) + (let1 (pair (var 0 (by simp)) (var 1 (by simp))) r.packed) := by + rw [packed, subst_case]; congr <;> rw [ + packed, let1_beta' (a' := pair (var 0 (by simp)) (var 1 (by simp))) (h := by simp), + subst_subst, Subst.Eqv.lift_unpack + ] + +@[simp] +theorem Eqv.packed_inl {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (A, e)} + : (inl (B := B) a).packed (Δ := Δ) = inl a.packed := by simp [packed] + +@[simp] +theorem Eqv.packed_inr {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (B, e)} + : (inr (A := A) a).packed (Δ := Δ) = inr a.packed := by simp [packed] + +@[simp] +theorem Eqv.packed_abort {Γ : Ctx α ε} {A : Ty α} {a : Eqv φ Γ (Ty.empty, e)} + : (abort a A).packed (Δ := Δ) = abort a.packed A := by simp [packed] + +@[simp] +theorem Eqv.packed_unit {Γ : Ctx α ε} : (unit (φ := φ) (Γ := Γ) (e := e)).packed (Δ := Δ) = unit _ + := rfl + +end Term diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural/Sum.lean new file mode 100644 index 0000000..f82b1d7 --- /dev/null +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural/Sum.lean @@ -0,0 +1,58 @@ +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Seq +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Product +import DeBruijnSSA.BinSyntax.Typing.Term.Structural + + +namespace BinSyntax + +variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε] + +namespace Term + +set_option linter.unusedVariables false in +def Eqv.inj + {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} (a : Eqv φ Γ (R.get i, e)) : Eqv φ Γ (R.pack, e) + := match R with + | [] => i.elim0 + | _::R => by cases i using Fin.cases with | zero => exact a.inl | succ i => exact inr (inj a) + +-- TODO: pack_inj is just inj (nil) + +def Eqv.inj_n {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) : Eqv φ ((R.get i, ⊥)::Γ) (R.pack, e) + := match R with + | [] => i.elim0 + | _::R => i.cases (inl nil) (λi => inr (inj_n R i)) + +theorem Eqv.inj_n_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} + : Eqv.inj_n (φ := φ) (Γ := Γ) R i = ⟦Term.InS.inj_n R i⟧ := by + induction R generalizing Γ with + | nil => exact i.elim0 + | cons _ _ I => + cases i using Fin.cases with + | zero => rfl + | succ i => + simp only [inj_n, I, inr_quot, Fin.cases_succ] + apply congrArg + ext + simp [Term.inj_n, Term.inj, Term.Wf.inj_n, -Function.iterate_succ, Function.iterate_succ'] + +-- def Eqv.pack_case {Γ : Ctx α ε} {R : LCtx α} +-- (d : Eqv φ Γ (R.pack, e)) (G : ∀i : Fin R.length, Eqv φ ((R.get i, ⊥)::Γ) (A, e)) +-- : Eqv φ Γ (C, e) := sorry + +-- def Eqv.pack_app_inl {Γ : Ctx α ε} {L R : LCtx α} : Eqv φ ((L.pack, ⊥)::Γ) ((L ++ R).pack, e) +-- := sorry + +-- def Eqv.pack_app_inr {Γ : Ctx α ε} {L R : LCtx α} : Eqv φ ((R.pack, ⊥)::Γ) ((L ++ R).pack, e) +-- := sorry + +-- def Eqv.pack_app {Γ : Ctx α ε} {L R : LCtx α} +-- : Eqv φ (((L ++ R).pack, ⊥)::Γ) (L.pack.coprod R.pack, e) +-- := sorry + +-- TODO: pack_app + +-- TODO: pack_app_pack_case => pack_case + +end Term diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/Structural.lean b/DeBruijnSSA/BinSyntax/Typing/Region/Structural.lean index 0fcfd13..de23d9c 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Region/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Region/Structural.lean @@ -16,11 +16,11 @@ variable open Term -def Subst.pack : Region.Subst φ := λℓ => br 0 (Term.pack0 ℓ) +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.pack0 + : Subst.Wf Γ R [R.pack] (Subst.pack (φ := φ)) := λ_ => Wf.br LCtx.Trg.shead Term.Wf.inj_n @[simp] def Subst.InS.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.InS φ Γ R [R.pack] := @@ -28,7 +28,7 @@ def Subst.InS.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.InS φ Γ R [R.pack] : @[simp] theorem Subst.InS.coe_pack {Γ : Ctx α ε} {R : LCtx α} (ℓ : ℕ) - : (Subst.InS.pack (φ := φ) (Γ := Γ) (R := R) : Region.Subst φ) ℓ = br 0 (Term.pack0 ℓ) := rfl + : (Subst.InS.pack (φ := φ) (Γ := Γ) (R := R) : Region.Subst φ) ℓ = br 0 (Term.inj_n ℓ) := rfl @[simp] theorem Subst.vlift_pack diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/VSubst.lean b/DeBruijnSSA/BinSyntax/Typing/Region/VSubst.lean index a4e08dd..ddec5d2 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Region/VSubst.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Region/VSubst.lean @@ -29,6 +29,10 @@ theorem Region.InS.coe_vsubst {Γ Δ : Ctx α ε} {σ : Term.Subst.InS φ Γ Δ} : (r.vsubst σ : Region φ) = (r : Region φ).vsubst σ := rfl +@[simp] +theorem Region.InS.vsubst_id {Γ : Ctx α ε} {L : LCtx α} (r : InS φ Γ L) + : InS.vsubst Term.Subst.InS.id r = r := by ext; simp + @[simp] theorem Region.InS.vsubst_br {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.InS φ Γ Δ} {ℓ} {a : Term.InS φ Δ (A, ⊥)} {hℓ : L.Trg ℓ A} diff --git a/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean b/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean index 59fa6ee..0e498aa 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean @@ -10,7 +10,7 @@ section Product variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε] - {Γ Δ : Ctx α ε} {σ : Region.Subst φ} + {Γ Δ : Ctx α ε} def pack : ℕ → Term φ | 0 => unit @@ -56,38 +56,42 @@ theorem InS.wk_eff_pack {Γ : Ctx α ε} {h : ∀i, Γ.effect i ≤ lo} {h' : lo : (pack (φ := φ) h).wk_eff h' = pack (λi => (h i).trans h') := by ext; simp -def unpack0 (x : ℕ) : Term φ := pl (pr^[x] (var 0)) +def pi_n (x : ℕ) (e : Term φ) : Term φ := pl (pr^[x] e) + +-- TODO: pi_n well-formedness lore + +def proj_n (x : ℕ) : Term φ := pl (pr^[x] (var 0)) @[simp] -theorem wk_lift_unpack0 {x : ℕ} : (unpack0 (φ := φ) x).wk (Nat.liftWk ρ) = unpack0 x := by - simp only [unpack0, wk_pl] +theorem wk_lift_proj_n {x : ℕ} : (proj_n (φ := φ) x).wk (Nat.liftWk ρ) = proj_n x := by + simp only [proj_n, wk_pl] apply congrArg induction x with | zero => rfl | succ x ih => simp only [wk_pr, Function.iterate_succ_apply', ih] @[simp] -theorem fvi_unpack0 {x : ℕ} : fvi (unpack0 (φ := φ) x) = 1 := by +theorem fvi_proj_n {x : ℕ} : fvi (proj_n (φ := φ) x) = 1 := by simp only [fvi, Nat.reduceAdd, le_refl, tsub_eq_zero_of_le, zero_le, max_eq_left] induction x with | zero => rfl | succ x ih => simp [Function.iterate_succ_apply', ih] @[simp] -theorem subst_lift_unpack0 {x : ℕ} {σ : Subst φ} : (unpack0 x).subst σ.lift = unpack0 x := by - simp only [unpack0, subst_pl] +theorem subst_lift_proj_n {x : ℕ} {σ : Subst φ} : (proj_n x).subst σ.lift = proj_n x := by + simp only [proj_n, subst_pl] apply congrArg induction x with | zero => rfl | succ x ih => simp only [subst_pr, Function.iterate_succ_apply', ih] @[simp] -theorem wk1_unpack0 {x : ℕ} : (unpack0 (φ := φ) x).wk1 = unpack0 x := wk_lift_unpack0 +theorem wk1_proj_n {x : ℕ} : (proj_n (φ := φ) x).wk1 = proj_n x := wk_lift_proj_n @[simp] -theorem subst0_nil_pr_unpack0 {x : ℕ} : (unpack0 x).subst nil.pr.subst0 = unpack0 (φ := φ) (x + 1) +theorem subst0_nil_pr_proj_n {x : ℕ} : (proj_n x).subst nil.pr.subst0 = proj_n (φ := φ) (x + 1) := by - simp only [unpack0, subst_pl] + simp only [proj_n, subst_pl] apply congrArg induction x with | zero => rfl @@ -99,11 +103,11 @@ theorem Wf.pack_drop' {Γ Δ : Ctx α ε} {i : ℕ} (hi : i < Γ.length) := by induction i generalizing Γ with | zero => cases Γ with | nil => cases hi - | cons _ Γ => simp [unpack0, Ctx.pack] + | cons _ Γ => simp [proj_n, Ctx.pack] | succ i I => cases Γ with | nil => cases hi | cons head Γ => - simp only [BinSyntax.Term.unpack0, List.length_cons, Fin.val_succ, Function.iterate_succ', + simp only [BinSyntax.Term.proj_n, List.length_cons, Fin.val_succ, Function.iterate_succ', Function.comp_apply, List.get_eq_getElem, List.getElem_cons_succ, Ctx.pack] apply Wf.pr convert I (Γ := head::Γ) (Nat.lt_of_succ_lt hi) @@ -126,8 +130,8 @@ theorem Wf.pack_drop {Γ Δ : Ctx α ε} {i : ℕ} (hi : i < Γ.length) : Wf (φ := φ) ((Γ.pack, ⊥)::Δ) (Term.pr^[i] (Term.var 0)) (Ctx.pack (Γ.drop i), e) := by rw [Ctx.pack_drop hi]; apply Wf.pack_drop' hi -theorem Wf.unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : Wf (φ := φ) ((Γ.pack, ⊥)::Δ) (unpack0 i) ((Γ.get i).1, e) +theorem Wf.proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : Wf (φ := φ) ((Γ.pack, ⊥)::Δ) (proj_n i) ((Γ.get i).1, e) := Wf.pl (pack_drop' i.prop) def InS.pack_drop {Γ Δ : Ctx α ε} (i : Fin Γ.length) @@ -164,46 +168,46 @@ def InS.pack_drop_succ {Γ Δ : Ctx α ε} (i : Fin Γ.length) rw [<-Term.pr, <-Function.iterate_succ_apply, Function.iterate_succ_apply'] rfl -def InS.unpack0 {Γ Δ : Ctx α ε} (i : Fin Γ.length) +def InS.proj_n {Γ Δ : Ctx α ε} (i : Fin Γ.length) : InS φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e) - := ⟨Term.unpack0 i, Wf.unpack0⟩ + := ⟨Term.proj_n i, Wf.proj_n⟩ theorem InS.pl_pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (InS.pack_drop' (φ := φ) (Δ := Δ) (e := e) i).pl = unpack0 i := rfl + : (InS.pack_drop' (φ := φ) (Δ := Δ) (e := e) i).pl = proj_n i := rfl -theorem InS.coe_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (InS.unpack0 (φ := φ) (Δ := Δ) (e := e) i : Term φ) = Term.unpack0 i := rfl +theorem InS.coe_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (InS.proj_n (φ := φ) (Δ := Δ) (e := e) i : Term φ) = Term.proj_n i := rfl --- TODO: wk_lift unpack0 +-- TODO: wk_lift proj_n --- TODO: subst_lift unpack0 +-- TODO: subst_lift proj_n @[simp] -theorem InS.wk1_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (InS.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk1 (inserted := inserted) = unpack0 i := by - ext; rw [coe_unpack0, coe_wk1, coe_unpack0, Term.wk1_unpack0] +theorem InS.wk1_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (InS.proj_n (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk1 (inserted := inserted) = proj_n i := by + ext; rw [coe_proj_n, coe_wk1, coe_proj_n, Term.wk1_proj_n] @[simp] -theorem InS.wk_lift_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} {ρ : Γ.InS Δ} - : (InS.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk (ρ.lift (le_refl _)) = unpack0 i := by - ext; rw [coe_unpack0, coe_wk, coe_unpack0, Ctx.InS.coe_lift, Term.wk_lift_unpack0] +theorem InS.wk_lift_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} {ρ : Γ.InS Δ} + : (InS.proj_n (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk (ρ.lift (le_refl _)) = proj_n i := by + ext; rw [coe_proj_n, coe_wk, coe_proj_n, Ctx.InS.coe_lift, Term.wk_lift_proj_n] @[simp] -theorem InS.subst_lift_unpack0 {Γ Δ Δ' : Ctx α ε} {i : Fin Γ.length} {σ : Subst.InS φ Δ' Δ} - : (InS.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).subst (σ.lift (le_refl _)) = unpack0 i := by - ext; rw [coe_unpack0, coe_subst, coe_unpack0, Subst.InS.coe_lift, Term.subst_lift_unpack0] +theorem InS.subst_lift_proj_n {Γ Δ Δ' : Ctx α ε} {i : Fin Γ.length} {σ : Subst.InS φ Δ' Δ} + : (InS.proj_n (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).subst (σ.lift (le_refl _)) = proj_n i := by + ext; rw [coe_proj_n, coe_subst, coe_proj_n, Subst.InS.coe_lift, Term.subst_lift_proj_n] @[simp] -theorem InS.subst0_nil_pr_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (InS.unpack0 (φ := φ) (Γ := Γ) (e := e) i).subst (nil.pr.subst0) - = unpack0 (φ := φ) (Γ := V::Γ) (Δ := Δ) i.succ := by ext; exact Term.subst0_nil_pr_unpack0 +theorem InS.subst0_nil_pr_proj_n {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (InS.proj_n (φ := φ) (Γ := Γ) (e := e) i).subst (nil.pr.subst0) + = proj_n (φ := φ) (Γ := V::Γ) (Δ := Δ) i.succ := by ext; exact Term.subst0_nil_pr_proj_n -def unpack0' (n : ℕ) (i : ℕ) : Term φ := match n with +def proj_n' (n : ℕ) (i : ℕ) : Term φ := match n with | 0 => unit -| n + 1 => let2 (var 0) (match i with | 0 => var 1 | i + 1 => unpack0' n i) +| n + 1 => let2 (var 0) (match i with | 0 => var 1 | i + 1 => proj_n' n i) -theorem Wf.unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) - : Wf (φ := φ) ((Γ.pack, ⊥)::Δ) (unpack0' Γ.length i) ((Γ.get i).1, e) +theorem Wf.proj_n' {Γ Δ : Ctx α ε} (i : Fin Γ.length) + : Wf (φ := φ) ((Γ.pack, ⊥)::Δ) (proj_n' Γ.length i) ((Γ.get i).1, e) := by induction Γ generalizing Δ with | nil => exact i.elim0 | cons V Γ I => @@ -215,41 +219,41 @@ theorem Wf.unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) simp only [List.length_cons, Fin.val_succ, List.get_eq_getElem, List.getElem_cons_succ] exact I i -def InS.unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : InS φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e) +def InS.proj_n' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : InS φ ((Γ.pack, ⊥)::Δ) ((Γ.get i).1, e) := match Γ with | [] => i.elim0 | V::Γ => let2 (var (V := (V.1.prod (Ctx.pack Γ), e)) 0 (by simp [Ctx.pack])) - (i.cases (var 1 (by simp)) (λi => unpack0' (Γ := Γ) i)) + (i.cases (var 1 (by simp)) (λi => proj_n' (Γ := Γ) i)) @[simp] -theorem InS.coe_unpack0' {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : (InS.unpack0' (φ := φ) (Δ := Δ) (e := e) i : Term φ) = Term.unpack0' Γ.length i := by +theorem InS.coe_proj_n' {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : (InS.proj_n' (φ := φ) (Δ := Δ) (e := e) i : Term φ) = Term.proj_n' Γ.length i := by induction Γ generalizing Δ with | nil => exact i.elim0 | cons V Γ I => - simp only [List.get_eq_getElem, List.length_cons, Set.mem_setOf_eq, unpack0', Fin.val_zero, - List.getElem_cons_zero, InS.coe_let2, coe_var, Term.unpack0', let2.injEq, true_and] + simp only [List.get_eq_getElem, List.length_cons, Set.mem_setOf_eq, proj_n', Fin.val_zero, + List.getElem_cons_zero, InS.coe_let2, coe_var, Term.proj_n', let2.injEq, true_and] cases i using Fin.cases with | zero => rfl | succ i => exact I -theorem InS.unpack0_zero' {Γ Δ : Ctx α ε} - : InS.unpack0' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) (by simp only [List.length_cons]; exact 0) +theorem InS.proj_n_zero' {Γ Δ : Ctx α ε} + : InS.proj_n' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) (by simp only [List.length_cons]; exact 0) = (by simp only [Ctx.pack]; apply InS.pi_l) := rfl -theorem InS.unpack0_succ' {Γ Δ : Ctx α ε} {i : Fin Γ.length} - : InS.unpack0' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ +theorem InS.proj_n_succ' {Γ Δ : Ctx α ε} {i : Fin Γ.length} + : InS.proj_n' (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) i.succ = let2 (var (V := (V.1.prod (Ctx.pack Γ), e)) 0 (by simp [Ctx.pack])) - (unpack0' (Γ := Γ) i) := rfl + (proj_n' (Γ := Γ) i) := rfl -def Subst.unpack0 : Subst φ := λi => Term.unpack0 i +def Subst.proj_n : Subst φ := λi => Term.proj_n i -theorem Subst.Wf.unpack0 {Γ Δ : Ctx α ε} - : Subst.Wf (φ := φ) ((Γ.pack, ⊥)::Δ) Γ Subst.unpack0 := λ_ => Term.Wf.unpack0 +theorem Subst.Wf.proj_n {Γ Δ : Ctx α ε} + : Subst.Wf (φ := φ) ((Γ.pack, ⊥)::Δ) Γ Subst.proj_n := λ_ => Term.Wf.proj_n -def Subst.InS.unpack {Γ Δ : Ctx α ε} : Subst.InS φ ((Γ.pack, ⊥)::Δ) Γ := ⟨Subst.unpack0, Wf.unpack0⟩ +def Subst.InS.unpack {Γ Δ : Ctx α ε} : Subst.InS φ ((Γ.pack, ⊥)::Δ) Γ := ⟨Subst.proj_n, Wf.proj_n⟩ def Subst.pack (n : ℕ) : Subst φ := λ_ => Term.pack n @@ -275,67 +279,117 @@ section Sum variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [PartialOrder ε] [OrderBot ε] - {Γ Δ : Ctx α ε} {σ : Region.Subst φ} + {Γ Δ : Ctx α ε} -def pack0 (ℓ : ℕ) : Term φ := inr^[ℓ] (inl (var 0)) +def inj (ℓ : ℕ) (e : Term φ) : Term φ := inr^[ℓ] (inl e) @[simp] -theorem wk_lift_pack0 {ℓ : ℕ} : (pack0 ℓ).wk (Nat.liftWk ρ) = pack0 (φ := φ) ℓ := by - simp only [pack0] +theorem wk_inj {ℓ : ℕ} {e : Term φ} : (inj ℓ e).wk ρ = inj ℓ (e.wk ρ) := by + simp only [inj] induction ℓ with | zero => rfl | succ ℓ ih => simp [ih, -Function.iterate_succ, Function.iterate_succ'] @[simp] -theorem wk1_pack0 : (pack0 ℓ).wk1 = pack0 (φ := φ) ℓ := by - simp only [wk1, wk_lift_pack0] +theorem wk0_inj {ℓ : ℕ} {e : Term φ} : (inj ℓ e).wk0 = inj ℓ (e.wk0) := by + simp only [wk0, wk_inj] + +@[simp] +theorem wk1_inj {ℓ : ℕ} {e : Term φ} : (inj ℓ e).wk1 = inj ℓ (e.wk1) := by + simp only [wk1, wk_inj] @[simp] -theorem subst_lift_pack0 {ℓ : ℕ} {σ : Subst φ} : (pack0 ℓ).subst σ.lift = pack0 (φ := φ) ℓ := by - simp only [pack0] +theorem wk2_inj {ℓ : ℕ} {e : Term φ} : (inj ℓ e).wk2 = inj ℓ (e.wk2) := by + simp only [wk2, wk_inj] + +@[simp] +theorem subst_inj {ℓ : ℕ} {e : Term φ} : (inj ℓ e).subst σ = inj ℓ (e.subst σ) := by + simp only [inj] induction ℓ with | zero => rfl | succ ℓ ih => simp [ih, -Function.iterate_succ, Function.iterate_succ'] +theorem Wf.inj {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : Term φ} + (h : a.Wf Γ (R.get i, e)) : Term.Wf (φ := φ) Γ (inj i a) (R.pack, e) := by + induction R generalizing Γ with + | nil => exact i.elim0 + | cons _ _ I => + cases i using Fin.cases with + | zero => exact Wf.inl $ h + | succ i => + simp only [ + Fin.val_succ, Function.iterate_succ', Function.comp_apply, LCtx.pack, + Wf.inr_iff, BinSyntax.Term.inj + ] + apply I + apply h + +def InS.inj {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} (a : Term.InS φ Γ (R.get i, e)) + : Term.InS φ Γ (R.pack, e) := ⟨a.val.inj i, a.prop.inj⟩ + +@[simp] +theorem InS.coe_inj {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : Term.InS φ Γ (R.get i, e)} + : (InS.inj (φ := φ) (Γ := Γ) (R := R) a : Term φ) = Term.inj i a := rfl + +def inj_n (ℓ : ℕ) : Term φ := inj ℓ nil + +@[simp] +theorem wk_lift_inj_n {ℓ : ℕ} : (inj_n ℓ).wk (Nat.liftWk ρ) = inj_n (φ := φ) ℓ := by + simp only [inj_n, wk_inj, wk, Nat.liftWk_zero]; rfl + +@[simp] +theorem wk1_inj_n : (inj_n ℓ).wk1 = inj_n (φ := φ) ℓ := by + simp only [wk1, wk_lift_inj_n] + +@[simp] +theorem wk2_inj_n : (inj_n ℓ).wk2 = inj_n (φ := φ) ℓ := by + simp only [inj_n, wk2_inj]; rfl + +@[simp] +theorem subst_lift_inj_n {ℓ : ℕ} {σ : Subst φ} : (inj_n ℓ).subst σ.lift = inj_n (φ := φ) ℓ := by + simp only [inj_n, subst_inj, subst, Subst.lift_zero]; rfl + @[simp] -theorem Wf.pack0 {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} - : Term.Wf (φ := φ) ((R.get i, ⊥)::Γ) (pack0 i) (R.pack, ⊥) := by +theorem Wf.inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} + : Term.Wf (φ := φ) ((R.get i, ⊥)::Γ) (inj_n i) (R.pack, ⊥) := by induction R generalizing Γ with | nil => exact i.elim0 | cons _ _ I => cases i using Fin.cases with | zero => exact Wf.inl $ Wf.var Ctx.Var.shead | succ i => - simp only [Fin.val_succ, - BinSyntax.Term.pack0, Function.iterate_succ', Function.comp_apply, LCtx.pack, Wf.inr_iff] + simp only [ + Fin.val_succ, BinSyntax.Term.inj_n, Function.iterate_succ', Function.comp_apply, LCtx.pack, + Wf.inr_iff, BinSyntax.Term.inj + ] apply I -def InS.pack0 {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) +def InS.inj_n {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) : Term.InS φ ((R.get i, ⊥)::Γ) (R.pack, ⊥) := - ⟨Term.pack0 i, Term.Wf.pack0⟩ + ⟨Term.inj_n i, Term.Wf.inj_n⟩ @[simp] -theorem InS.coe_pack0 {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} - : (InS.pack0 (φ := φ) (Γ := Γ) (R := R) i : Term φ) = Term.pack0 i := rfl +theorem InS.coe_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} + : (InS.inj_n (φ := φ) (Γ := Γ) (R := R) i : Term φ) = Term.inj_n i := rfl @[simp] -theorem InS.wk_lift_pack0 {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {ρ : Γ.InS Δ} - : (InS.pack0 (φ := φ) R i).wk (ρ.lift (le_refl _)) = pack0 R i := by ext; simp +theorem InS.wk_lift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {ρ : Γ.InS Δ} + : (InS.inj_n (φ := φ) R i).wk (ρ.lift (le_refl _)) = inj_n R i := by ext; simp @[simp] -theorem InS.wk_slift_pack0 {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {ρ : Γ.InS Δ} - : (InS.pack0 (φ := φ) R i).wk (ρ.slift) = pack0 R i := by ext; simp +theorem InS.wk_slift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {ρ : Γ.InS Δ} + : (InS.inj_n (φ := φ) R i).wk (ρ.slift) = inj_n R i := by ext; simp @[simp] -theorem InS.subst_lift_pack0 {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {σ : Subst.InS φ Γ Δ} - : (InS.pack0 (φ := φ) R i).subst (σ.lift (le_refl _)) = pack0 R i := by ext; simp +theorem InS.subst_lift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {σ : Subst.InS φ Γ Δ} + : (InS.inj_n (φ := φ) R i).subst (σ.lift (le_refl _)) = inj_n R i := by ext; simp @[simp] -theorem InS.subst_slift_pack0 {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {σ : Subst.InS φ Γ Δ} - : (InS.pack0 (φ := φ) R i).subst σ.slift = pack0 R i := by ext; simp +theorem InS.subst_slift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {σ : Subst.InS φ Γ Δ} + : (InS.inj_n (φ := φ) R i).subst σ.slift = inj_n R i := by ext; simp @[simp] -theorem InS.wk1_pack0 {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} - : (InS.pack0 (φ := φ) (Γ := Γ) R i).wk1 (inserted := inserted) = pack0 R i := by ext; simp +theorem InS.wk1_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} + : (InS.inj_n (φ := φ) (Γ := Γ) R i).wk1 (inserted := inserted) = inj_n R i := by ext; simp end Sum