From 0b05fc7b989eee5d2a31b6660373ad5ac31bc7e9 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Tue, 17 Sep 2024 16:30:17 +0100 Subject: [PATCH] Work on packed term theory --- .../Rewrite/Term/Compose/Product.lean | 14 ++ .../Rewrite/Term/Compose/Structural.lean | 120 ++++++++++++++++-- DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean | 45 +++++++ .../BinSyntax/Typing/Term/Structural.lean | 17 +++ 4 files changed, 186 insertions(+), 10 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean index 704937b..982bb91 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean @@ -21,11 +21,18 @@ def Eqv.pl {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B, e⟩) : Eq theorem Eqv.pl_quot {A B : Ty α} {Γ : Ctx α ε} {a : InS φ Γ ⟨A.prod B, e⟩} : pl ⟦a⟧ = ⟦a.pl⟧ := rfl +@[simp] theorem Eqv.wk_pl {A B : Ty α} {Γ : Ctx α ε} {ρ : Ctx.InS Γ Δ} {a : Eqv φ Δ ⟨A.prod B, e⟩} : (a.pl).wk ρ = (a.wk ρ).pl := by induction a using Quotient.inductionOn; rfl +@[simp] +theorem Eqv.subst_pl {A B : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ} + {a : Eqv φ Δ ⟨A.prod B, e⟩} + : (a.pl).subst σ = (a.subst σ).pl := by + induction a using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl + theorem Eqv.wk0_pl {A B : Ty α} {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A.prod B, e⟩} : (a.pl).wk0 (head := head) = a.wk0.pl := by rw [wk0, wk_pl]; rfl @@ -49,11 +56,18 @@ def Eqv.pr {A B : Ty α} {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A.prod B, e⟩) : Eq theorem Eqv.pr_quot {A B : Ty α} {Γ : Ctx α ε} {a : InS φ Γ ⟨A.prod B, e⟩} : pr ⟦a⟧ = ⟦a.pr⟧ := rfl +@[simp] theorem Eqv.wk_pr {A B : Ty α} {Γ : Ctx α ε} {ρ : Ctx.InS Γ Δ} {a : Eqv φ Δ ⟨A.prod B, e⟩} : (a.pr).wk ρ = (a.wk ρ).pr := by induction a using Quotient.inductionOn; rfl +@[simp] +theorem Eqv.subst_pr {A B : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ} + {a : Eqv φ Δ ⟨A.prod B, e⟩} + : (a.pr).subst σ = (a.subst σ).pr := by + induction a using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl + theorem Eqv.wk0_pr {A B : Ty α} {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A.prod B, e⟩} : (a.pr).wk0 (head := head) = a.wk0.pr := by rw [wk0, wk_pr]; rfl diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean index 24d2e79..257d5f7 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Structural.lean @@ -105,6 +105,17 @@ theorem Eqv.wk1_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} : (Eqv.unpack0 (φ := φ) (Γ := Γ) (Δ := Δ) (e := e) i).wk1 (inserted := inserted) = unpack0 i := by simp [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) @@ -123,6 +134,9 @@ theorem Eqv.pl_pack_drop' {Γ Δ : Ctx α ε} {i : Fin Γ.length} 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] @@ -224,20 +238,106 @@ theorem Eqv.unpack0_eq_unpack0' {Γ Δ : Ctx α ε} (i : Fin Γ.length) : 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) --- := sorry +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'] +@[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.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 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 + ]; congr + ext k + cases k using Fin.cases with + | zero => + simp [Subst.Eqv.get_comp, unpack0_zero, pi_l, nil, pl, let2_pair, let1_beta_var0, let1_beta_var1] + | succ k => + simp [ + Subst.Eqv.get_comp, unpack0_succ, seq, pi_r, nil, pr, let2_pair, let1_beta_var0, + let1_beta_var1 + ] + rw [wk0, <-subst_fromWk] + apply 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 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 +-- sorry + +-- 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 +-- sorry + +@[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/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean index b001214..a77fd42 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean @@ -668,6 +668,51 @@ def Subst.Eqv.get (σ : Subst.Eqv φ Γ Δ) (i : Fin Δ.length) : Term.Eqv φ Γ theorem Subst.Eqv.get_quot {σ : Subst.InS φ Γ Δ} {i : Fin Δ.length} : get ⟦σ⟧ i = ⟦σ.get i⟧ := rfl +@[simp] +theorem Subst.Eqv.get_lift_zero {h : lo ≤ hi} {σ : Eqv φ Γ Δ} + : (σ.lift h).get (0 : Fin (Δ.length + 1)) = Eqv.var 0 (by simp [h]) := by + induction σ using Quotient.inductionOn + apply Eqv.eq_of_term_eq + rfl + +@[simp] +theorem Subst.Eqv.get_lift_succ {h : lo ≤ hi} {σ : Eqv φ Γ Δ} {i : Fin Δ.length} + : (σ.lift h).get i.succ = (σ.get i).wk0 := by + induction σ using Quotient.inductionOn + apply Eqv.eq_of_term_eq + rfl + +@[simp] +theorem Subst.Eqv.get_liftn₂_zero {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ} + : (σ.liftn₂ h₁ h₂).get (0 : Fin (Δ.length + 2)) = Eqv.var 0 (by simp [h₁]) := by + induction σ using Quotient.inductionOn + apply Eqv.eq_of_term_eq + rfl + +theorem Subst.Eqv.get_liftn₂_one {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ} + : (σ.liftn₂ h₁ h₂).get (1 : Fin (Δ.length + 2)) = Eqv.var 1 (by simp [h₂]) := by + induction σ using Quotient.inductionOn + apply Eqv.eq_of_term_eq + rfl + +theorem Subst.Eqv.get_liftn₂_succ_succ + {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ} {i : Fin Δ.length} + : (σ.liftn₂ h₁ h₂).get i.succ.succ = (σ.get i).wk0.wk0 := by + induction σ using Quotient.inductionOn + apply Eqv.eq_of_term_eq + simp only [Nat.succ_eq_add_one, List.get_eq_getElem, List.length_cons, Fin.val_succ, + List.getElem_cons_succ, Set.mem_setOf_eq, InS.coe_get, InS.coe_liftn₂, liftn, Nat.reduceSubDiff, + InS.coe_wk, Ctx.InS.coe_wk0, wk_wk] + rfl + +@[simp] +theorem Subst.Eqv.get_liftn₂_succ {h₁ : lo₁ ≤ hi₁} {h₂ : lo₂ ≤ hi₂} {σ : Eqv φ Γ Δ} + {i : Fin (Δ.length + 1)} + : (σ.liftn₂ h₁ h₂).get i.succ = ((σ.lift h₂).get i).wk0 := by + cases i using Fin.cases with + | zero => convert get_liftn₂_one; simp + | succ i => convert get_liftn₂_succ_succ using 1; simp + theorem Subst.Eqv.ext_quot {σ τ : Subst.InS φ Γ Δ} (h : ∀i, (⟦σ.get i⟧ : Term.Eqv φ _ _) = ⟦τ.get i⟧) : (⟦σ⟧ : Subst.Eqv φ Γ Δ) = ⟦τ⟧ := Quotient.sound (λi => Quotient.exact $ h i) diff --git a/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean b/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean index 0668b29..59fa6ee 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean @@ -66,6 +66,13 @@ theorem wk_lift_unpack0 {x : ℕ} : (unpack0 (φ := φ) x).wk (Nat.liftWk ρ) = | zero => rfl | succ x ih => simp only [wk_pr, Function.iterate_succ_apply', ih] +@[simp] +theorem fvi_unpack0 {x : ℕ} : fvi (unpack0 (φ := φ) 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] @@ -176,6 +183,16 @@ 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] +@[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] + +@[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] + @[simp] theorem InS.subst0_nil_pr_unpack0 {Γ Δ : Ctx α ε} {i : Fin Γ.length} : (InS.unpack0 (φ := φ) (Γ := Γ) (e := e) i).subst (nil.pr.subst0)