From 45e8c5997234a36c62081a77c2250eb969411aa9 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Wed, 11 Sep 2024 14:52:43 +0100 Subject: [PATCH] Began experimenting with term completeness --- .../Rewrite/Region/Compose/Structural.lean | 34 ++------ .../Rewrite/Term/Compose/Completeness.lean | 54 +++++++++++++ DeBruijnSSA/BinSyntax/Typing/Ctx.lean | 77 ++++++++++++++++++- 3 files changed, 137 insertions(+), 28 deletions(-) create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Completeness.lean diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean index 453ff9b..20025c2 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean @@ -1,34 +1,13 @@ 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.Completeness import DeBruijnSSA.BinSyntax.Typing.Region.Structural namespace BinSyntax variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε] -namespace Term - -def Eqv.pack {Γ : 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 R i)) - -theorem Eqv.pack_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} - : Eqv.pack (φ := φ) (Γ := Γ) 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, I, inr_quot, Fin.cases_succ] - apply congrArg - ext - simp [Term.pack0, Term.Wf.pack0, -Function.iterate_succ, Function.iterate_succ'] - -end Term - namespace Region def Eqv.unpack {Γ : Ctx α ε} {R : LCtx α} : Eqv φ ((R.pack, ⊥)::Γ) R := @@ -77,7 +56,7 @@ def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R [R.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 R i) LCtx.Trg.shead := by rw [pack, Term.Eqv.pack_def]; rfl + = 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 α} @@ -85,19 +64,20 @@ theorem Subst.Eqv.vlift_pack {Γ : Ctx α ε} {R : LCtx α} := 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 R ℓ).subst0 + : (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, Fin.val_succ, Fin.cases_zero, unpack, coprod, vsubst_case, + 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, - LCtx.pack.eq_2, Term.Eqv.pack, Fin.val_zero, List.getElem_cons_zero, Fin.cases_succ, unpack, + 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 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Completeness.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Completeness.lean new file mode 100644 index 0000000..7c72b6f --- /dev/null +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Completeness.lean @@ -0,0 +1,54 @@ +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Seq +import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum +import DeBruijnSSA.BinSyntax.Typing.Region.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 α ε} : Eqv φ Γ (Γ.pack, Γ.sup_effect) := match Γ with + | [] => unit ⊥ + | V::Γ => pair (var 0 (by cases V; simp)) ((pack (Γ := Γ)).wk0.wk_eff (by simp)) + +def _root_.BinSyntax.Ctx.Pure.packE {Γ : Ctx α ε} (h : Γ.Pure) : Eqv φ Γ (Γ.pack, ⊥) := match Γ with + | [] => Eqv.unit ⊥ + | V::Γ => Eqv.pair (Eqv.var 0 (by cases V; convert h.head; simp)) h.tail.packE.wk0 + +def Eqv.unpack {Γ Δ : 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 => unpack i)) + +-- TODO: wk lift unpack + +-- TODO: let1 pack (unpack i) = var i + +-- TODO: need InS version for this... :( + +-- def Subst.Eqv.unpacked {Γ Δ : Ctx α ε} (i : Fin Γ.length) : Subst.Eqv φ ((Γ.pack, ⊥)::Δ) Γ +-- := sorry + +end Term diff --git a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean index 12650fd..fd6dfd5 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean @@ -718,6 +718,58 @@ theorem effect_append_bot₂ {left right : Ty α} {tail : Ctx α ε} : effect (⟨left, ⊥⟩::⟨right, ⊥⟩::tail) = Nat.liftnBot 2 tail.effect := by simp only [effect_append_bot, Nat.liftnBot_two_apply] +theorem effect_tail {Γ : Ctx α ε} (i : ℕ) + : effect (Γ.tail) i = Γ.effect (i + 1) := by cases Γ <;> simp [effect] + +theorem effect_cons_match {head} {Γ : Ctx α ε} (i : ℕ) + : effect (head::Γ) i = match i with | 0 => head.2 | i + 1 => Γ.effect i := by + cases i <;> simp [effect] + +@[simp] +theorem effect_cons_zero {head} {Γ : Ctx α ε} + : effect (head::Γ) 0 = head.2 := by simp [effect_cons_match] + +@[simp] +theorem effect_cons_succ {head} {Γ : Ctx α ε} (i : ℕ) + : effect (head::Γ) (i + 1) = Γ.effect i := by simp [effect_cons_match] + +@[simp] +theorem effect_empty : effect (α := α) (ε := ε) [] = ⊥ := by funext i; simp [effect] + +def pack : Ctx α ε → Ty α + | [] => Ty.unit + | V::Γ => V.1.prod (pack Γ) + +def Pure (Γ : Ctx α ε) : Prop := Γ.effect = ⊥ + +theorem pure_def {Γ : Ctx α ε} : Pure Γ ↔ Γ.effect = ⊥ := Iff.rfl + +theorem Pure.effect {Γ : Ctx α ε} (h : Pure Γ) (i : ℕ) : Γ.effect i = ⊥ + := by rw [h]; rfl + +theorem Pure.of_effect' {Γ : Ctx α ε} (h : Γ.effect = ⊥) : Pure Γ := h + +theorem Pure.of_effect {Γ : Ctx α ε} (h : ∀i, Γ.effect i = ⊥) : Pure Γ := funext h + +theorem Pure.effect' {Γ : Ctx α ε} (h : Pure Γ) : Γ.effect = ⊥ := h + +theorem Pure.nil : Pure (α := α) (ε := ε) [] := by simp [Pure] + +theorem Pure.cons {head} {Γ : Ctx α ε} (h : Pure Γ) : Pure ((head, ⊥)::Γ) := by + funext k; cases k <;> simp [Pure, effect_append_bot, h.effect', Nat.liftBot] + +theorem Pure.cons' {head} {Γ : Ctx α ε} (h : head.2 = ⊥) (h' : Pure Γ) : Pure (head::Γ) := by + cases head; cases h; exact h'.cons + +theorem Pure.head {head} {Γ : Ctx α ε} (h : Pure (head::Γ)): head.2 = ⊥ := by + convert h.effect 0; simp [Ctx.effect] + +theorem Pure.tail {Γ : Ctx α ε} (h : Pure Γ) : Pure Γ.tail + := of_effect (λi => by simp [effect_tail, h.effect (i + 1)]) + +theorem Pure.cons_iff {head} {Γ : Ctx α ε} : Pure (head::Γ) ↔ head.2 = ⊥ ∧ Pure Γ + := ⟨λh => ⟨h.head, h.tail⟩, λ⟨h, h'⟩ => h'.cons' h⟩ + variable [PartialOrder α] [PartialOrder ε] theorem Wkn.effect {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ ρ) (i : ℕ) (hi : i < Δ.length) @@ -733,7 +785,6 @@ theorem Var.toEffect {Γ : Ctx α ε} {n : ℕ} {V} (h : Γ.Var n V) exact h.get.1 simp [effect, h.length] ⟩ - -- def WknTy (Γ Δ : Ctx α ε) (ρ : ℕ → ℕ) : Prop := Γ.Types.NWkn Δ.Types ρ -- theorem WknTy.id_types_len_le {Γ Δ : Ctx α ε} @@ -761,4 +812,28 @@ theorem IsInitial.wk {Γ Δ : Ctx α ε} {ρ : ℕ → ℕ} (h : Γ.Wkn Δ ρ) : end OrderBot +section SemilatticeSup + +variable [Φ: EffInstSet φ (Ty α) ε] [SemilatticeSup ε] [OrderBot ε] + +@[simp] +def sup_effect : Ctx α ε → ε + | [] => ⊥ + | V::Γ => V.2 ⊔ sup_effect Γ + +theorem effect_le_sup_effect {Γ : Ctx α ε} (i : ℕ) : Γ.effect i ≤ sup_effect Γ + := by induction Γ generalizing i with + | nil => simp [effect, sup_effect] + | cons V Γ ih => + cases i with | zero => simp | succ i => exact le_sup_of_le_right (by simp [ih i]) + +theorem Pure.sup_effect_iff {Γ : Ctx α ε} : Pure Γ ↔ Γ.sup_effect = ⊥ + := by induction Γ <;> simp [nil, cons_iff, *] + +theorem Pure.sup_effect {Γ : Ctx α ε} : Pure Γ → Γ.sup_effect = ⊥ := Pure.sup_effect_iff.mp + +theorem Pure.of_sup_effect {Γ : Ctx α ε} : Γ.sup_effect = ⊥ → Pure Γ := Pure.sup_effect_iff.mpr + +end SemilatticeSup + end Ctx