From 1fdc138a2902af8984c968f2e6d112a0fcb6a816 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Thu, 13 Jun 2024 14:45:24 +0100 Subject: [PATCH] Tap --- .../BinSyntax/Syntax/Compose/Region.lean | 102 ++++++- DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean | 267 +++++++++++------- DeBruijnSSA/BinSyntax/Syntax/Subst.lean | 4 + lake-manifest.json | 6 +- 4 files changed, 265 insertions(+), 114 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean index 3128a23..279fc7f 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean @@ -53,6 +53,10 @@ theorem liftn_alpha (n m) (r : Region φ) : (alpha n r).liftn m = alpha (n + m) funext i simp_arith +theorem vwk_lift_alpha (n : ℕ) (r : Region φ) + : vwk (Nat.liftWk ρ) ∘ (alpha n r) = alpha n (r.vwk (Nat.liftWk ρ)) := by + simp [alpha, Function.comp_update] + def append (r r' : Region φ) : Region φ := r.lsubst (r'.vwk1.alpha 0) instance : Append (Region φ) := ⟨Region.append⟩ @@ -100,37 +104,115 @@ theorem lsubst_alpha_cfg (β n G k) (r : Region φ) simp only [append_def, lsubst, vlift_alpha, vwk_vwk, vwk1, ← Nat.liftWk_comp, liftn_alpha] rfl +theorem vwk_liftWk_lsubst_alpha + : (lsubst (alpha n r₁) r₀).vwk (Nat.liftWk ρ) + = lsubst (alpha n (r₁.vwk (Nat.liftnWk 2 ρ))) (r₀.vwk (Nat.liftWk ρ)) + := by simp [vwk_lsubst, vwk_lift_alpha, Nat.liftnWk_eq_iterate_liftWk] + +theorem vwk1_lsubst_alpha {r₀ r₁ : Region φ} + : (lsubst (alpha n r₁) r₀).vwk1 = lsubst (alpha n (r₁.vwk (Nat.liftnWk 2 Nat.succ))) r₀.vwk1 := by + rw [vwk1, vwk_lsubst, vwk_lift_alpha, Nat.liftnWk_eq_iterate_liftWk] + rfl + +theorem vwk_liftWk_lsubst_alpha_vwk1 {r₀ r₁ : Region φ} + : (lsubst (alpha n r₁.vwk1) r₀).vwk (Nat.liftWk ρ) + = lsubst (alpha n ((r₁.vwk (Nat.liftWk ρ)).vwk1)) (r₀.vwk (Nat.liftWk ρ)) := by + rw [vwk_liftWk_lsubst_alpha] + congr + apply congrArg + simp [vwk1, vwk_vwk, Nat.liftnWk_eq_iterate_liftWk, <-Nat.liftWk_comp, Nat.liftWk_comp_succ] + +theorem vwk1_lsubst_alpha_vwk1 {r₀ r₁ : Region φ} + : (lsubst (alpha n r₁.vwk1) r₀).vwk1 = lsubst (alpha n (r₁.vwk1.vwk1)) r₀.vwk1 := by + rw [vwk1_lsubst_alpha] + simp only [vwk1, vwk_vwk] + apply congrFun + apply congrArg + apply congrArg + congr + funext k; cases k <;> rfl + +def PRwD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'} + (p : PRwD Γ r₀ r₀') (n) (r₁ : Region φ) + : PRwD Γ (r₀.lsubst (alpha n r₁)) (r₀'.lsubst (alpha n r₁)) := match p with + | let1_op f e r => cast_trg (let1_op _ _ _) (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | let1_pair a b r => cast_trg (let1_pair _ _ _) (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | let1_inl e r => cast_trg (let1_inl _ _) (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | let1_inr e r => cast_trg (let1_inr _ _) (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | let1_abort e r => cast_trg (let1_abort _ _) (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | let2_op f e r => cast_trg (let2_op _ _ _) (by + --TODO: factor more nicely... + simp only [vliftn_alpha, vwk_lsubst, vwk_lift_alpha, vwk_vwk, lsubst, vlift_alpha, vwk1] + congr + apply congrArg + apply congrFun + apply congrArg + funext k; cases k <;> rfl) + | let2_pair a b r => cast_trg (let2_pair _ _ _) (by + --TODO: factor more nicely... + simp only [lsubst, vliftn_alpha, vlift_alpha, vwk1, vwk_vwk, <-Nat.liftWk_comp] + rfl) + | let2_abort e r => cast_trg (let2_abort _ _) (by + --TODO: factor more nicely... + simp only [vliftn_alpha, vwk_lsubst, vwk_lift_alpha, vwk_vwk, lsubst, vlift_alpha, vwk1] + congr + apply congrArg + apply congrFun + apply congrArg + funext k; cases k <;> rfl) + | case_op f e r s => cast_trg (case_op _ _ _ _) (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | case_abort e r s + => cast_trg (case_abort _ _ _) (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | let1_case a b r s => cast_trg (let1_case _ _ _ _) + (by simp [vlift_alpha, <-vwk1_lsubst_alpha_vwk1]) + | let2_case a b r s => cast_trg (let2_case _ _ _ _) (by + --TODO: factor more nicely... + simp only [vliftn_alpha, vwk_lsubst, vwk_lift_alpha, vwk_vwk, lsubst, vlift_alpha, vwk1] + congr <;> + apply congrArg <;> + apply congrFun <;> + apply congrArg <;> + funext k <;> cases k <;> rfl) + | cfg_br_lt ℓ e n G hℓ => by + sorry + | cfg_let1 a β n G => cast_trg (cfg_let1 _ _ _ _) sorry + | cfg_let2 a β n G => cast_trg (cfg_let2 _ _ _ _) sorry + | cfg_case e r s n G => cast_trg (cfg_case _ _ _ _ _) sorry + | cfg_cfg β n G n' G' => cast_trg (cfg_cfg _ _ _ _ _) sorry + def PStepD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'} (p : PStepD Γ r₀ r₀') (n) (r₁ : Region φ) - : RWD (PStepD Γ) (r₀.lsubst (alpha n r₁)) (r₀'.lsubst (alpha n r₁)) := sorry + : PStepD Γ (r₀.lsubst (alpha n r₁)) (r₀'.lsubst (alpha n r₁)) := match p with + | rw p => rw (p.lsubst_alpha n r₁) + | rw_symm p => rw_symm (p.lsubst_alpha n r₁) + | _ => sorry -- TODO: factor out as more general lifting lemma def SCongD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'} (p : SCongD (PStepD Γ) r₀ r₀') (n) (r₁ : Region φ) - : RWD (PStepD Γ) (r₀.lsubst (alpha n r₁)) (r₀'.lsubst (alpha n r₁)) := - match r₀, r₀', p with - | _, _, SCongD.step s => s.lsubst_alpha n r₁ - | _, _, SCongD.let1 e p => by + : RWD (PStepD Γ) (r₀.lsubst (alpha n r₁)) (r₀'.lsubst (alpha n r₁)) := match p with + | SCongD.step s => RWD.single (SCongD.step (s.lsubst_alpha n r₁)) + | SCongD.let1 e p => by simp only [lsubst_alpha_let1] apply RWD.let1 e apply lsubst_alpha p _ _ - | _, _, SCongD.let2 e p => by + | SCongD.let2 e p => by simp only [lsubst_alpha_let2] apply RWD.let2 e apply lsubst_alpha p _ _ - | _, _, SCongD.case_left e p t => by + | SCongD.case_left e p t => by simp only [lsubst_alpha_case] apply RWD.case_left e apply lsubst_alpha p _ _ - | _, _, SCongD.case_right e s p => by + | SCongD.case_right e s p => by simp only [lsubst_alpha_case] apply RWD.case_right e apply lsubst_alpha p _ _ - | _, _, SCongD.cfg_entry p n G => by + | SCongD.cfg_entry p n G => by simp only [lsubst_alpha_cfg] apply RWD.cfg_entry apply lsubst_alpha p _ _ - | _, _, SCongD.cfg_block β n G i p => by + | SCongD.cfg_block β n G i p => by simp only [lsubst_alpha_cfg, Function.comp_update] apply RWD.cfg_block apply lsubst_alpha p _ _ diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean index 6c4c5b2..6bf4c6c 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean @@ -151,42 +151,41 @@ open Term inductive PRwD (Γ : ℕ → ε) : Region φ → Region φ → Type | let1_op (f e r) : - PRwD Γ (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + PRwD Γ (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.vwk1) | let1_pair (a b r) : PRwD Γ (let1 (pair a b) r) - (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.vwk (Nat.liftWk (· + 2)) - ) + (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.vwk1.vwk1) | let1_inl (e r) : - PRwD Γ (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + PRwD Γ (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk1) | let1_inr (e r) : - PRwD Γ (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + PRwD Γ (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk1) | let1_abort (e r) : - PRwD Γ (let1 (abort e) r) (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + PRwD Γ (let1 (abort e) r) (let1 e $ let1 (abort (var 0)) $ r.vwk1) | let2_op (f e r) : PRwD Γ (let2 (op f e) r) (let1 e $ let2 (op f (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) | let2_pair (a b r) : PRwD Γ (let2 (pair a b) r) (let1 a $ let1 (b.wk Nat.succ) $ r) | let2_abort (e r) : PRwD Γ (let2 (abort e) r) (let1 e $ let2 (abort (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) - | let1_case (a b r s) : - PRwD Γ (let1 a $ case (b.wk Nat.succ) r s) - (case b (let1 (a.wk Nat.succ) r) (let1 (a.wk Nat.succ) s)) - | let2_case (a b r s) : - PRwD Γ (let2 a $ case (b.wk (· + 2)) r s) - (case b (let2 (a.wk Nat.succ) r) (let2 (a.wk Nat.succ) s)) | case_op (f e r s) : PRwD Γ (case (op f e) r s) (let1 e $ case (op f (var 0)) - (r.vwk (Nat.liftWk Nat.succ)) - (s.vwk (Nat.liftWk Nat.succ))) + (r.vwk1) + (s.vwk1)) | case_abort (e r s) : PRwD Γ (case (abort e) r s) (let1 e $ case (abort (var 0)) - (r.vwk (Nat.liftWk Nat.succ)) - (s.vwk (Nat.liftWk Nat.succ))) + (r.vwk1) + (s.vwk1)) + | let1_case (a b r s) : + PRwD Γ (let1 a $ case (b.wk Nat.succ) r s) + (case b (let1 (a.wk Nat.succ) r) (let1 (a.wk Nat.succ) s)) + | let2_case (a b r s) : + PRwD Γ (let2 a $ case (b.wk (· + 2)) r s) + (case b (let2 (a.wk Nat.succ) r) (let2 (a.wk Nat.succ) s)) | cfg_br_lt (ℓ e n G) (h : ℓ < n) : PRwD Γ (cfg (br ℓ e) n G) (cfg ((G ⟨ℓ, h⟩).let1 e) n G) | cfg_let1 (a β n G) : - PRwD Γ (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk Nat.succ ∘ G)) + PRwD Γ (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G)) | cfg_let2 (a β n G) : PRwD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G)) | cfg_case (e r s n G) : @@ -195,56 +194,24 @@ inductive PRwD (Γ : ℕ → ε) : Region φ → Region φ → Type | cfg_cfg (β n G n' G') : PRwD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G'))) +def PRwD.cast_src {Γ : ℕ → ε} {r₀ r₀' r₁ : Region φ} (h : r₀ = r₀') (p : PRwD Γ r₀ r₁) + : PRwD Γ r₀' r₁ := h ▸ p + +def PRwD.cast_trg {Γ : ℕ → ε} {r₀ r₁ r₁' : Region φ} (p : PRwD Γ r₀ r₁) (h : r₁ = r₁') + : PRwD Γ r₀ r₁' := h ▸ p + +def PRwD.cast {Γ : ℕ → ε} {r₀ r₀' r₁ r₁' : Region φ} (h₀ : r₀ = r₀') (h₁ : r₁ = r₁') + (p : PRwD Γ r₀ r₁) : PRwD Γ r₀' r₁' := h₁ ▸ h₀ ▸ p + +-- TODO: PRwD WfD iff? + inductive PStepD (Γ : ℕ → ε) : Region φ → Region φ → Type + | rw {r r'} : PRwD Γ r r' → PStepD Γ r r' + | rw_symm {r r'} : PRwD Γ r r' → PStepD Γ r' r | let1_beta (e r) : e.effect Γ = ⊥ → PStepD Γ (let1 e r) (r.vsubst e.subst0) | case_inl (e r s) : PStepD Γ (case (inl e) r s) (let1 e r) | case_inr (e r s) : PStepD Γ (case (inr e) r s) (let1 e s) - | let1_op (f e r) : - PStepD Γ (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) - | let1_pair (a b r) : - PStepD Γ (let1 (pair a b) r) - (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.vwk (Nat.liftWk (· + 2)) - ) - | let1_inl (e r) : - PStepD Γ (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) - | let1_inr (e r) : - PStepD Γ (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) - | let1_abort (e r) : - PStepD Γ (let1 (abort e) r) (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) - | let2_op (f e r) : - PStepD Γ (let2 (op f e) r) (let1 e $ let2 (op f (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) - | let2_pair (a b r) : PStepD Γ (let2 (pair a b) r) (let1 a $ let1 (b.wk Nat.succ) $ r) - | let2_abort (e r) : - PStepD Γ (let2 (abort e) r) (let1 e $ let2 (abort (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) - | case_op (f e r s) : - PStepD Γ (case (op f e) r s) - (let1 e $ case (op f (var 0)) - (r.vwk (Nat.liftWk Nat.succ)) - (s.vwk (Nat.liftWk Nat.succ))) - | case_abort (e r s) : - PStepD Γ (case (abort e) r s) - (let1 e $ case (abort (var 0)) - (r.vwk (Nat.liftWk Nat.succ)) - (s.vwk (Nat.liftWk Nat.succ))) - | let1_case (a b r s) : - PStepD Γ (let1 a $ case (b.wk Nat.succ) r s) - (case b (let1 (a.wk Nat.succ) r) (let1 (a.wk Nat.succ) s)) - | let2_case (a b r s) : - PStepD Γ (let2 a $ case (b.wk (· + 2)) r s) - (case b (let2 (a.wk Nat.succ) r) (let2 (a.wk Nat.succ) s)) - | cfg_br_lt (ℓ e n G) (h : ℓ < n) : - PStepD Γ (cfg (br ℓ e) n G) (cfg ((G ⟨ℓ, h⟩).let1 e) n G) - | cfg_br_ge (ℓ e n G) (h : n ≤ ℓ) : - PStepD Γ (cfg (br ℓ e) n G) (br (ℓ - n) e) - | cfg_let1 (a β n G) : - PStepD Γ (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk Nat.succ ∘ G)) - | cfg_let2 (a β n G) : - PStepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G)) - | cfg_case (e r s n G) : - PStepD Γ (cfg (case e r s) n G) - (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G))) - | cfg_cfg (β n G n' G') : - PStepD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G'))) + | cfg_br_ge (ℓ e n G) (h : n ≤ ℓ) : PStepD Γ (cfg (br ℓ e) n G) (br (ℓ - n) e) | wk_cfg (β n G k) (ρ : Fin k → Fin n) /-(hρ : Function.Bijective ρ)-/ : PStepD Γ (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G)) @@ -256,6 +223,101 @@ inductive PStepD (Γ : ℕ → ε) : Region φ → Region φ → Type (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G'))) (cfg β m G') +@[match_pattern] +def PStepD.let1_op {Γ : ℕ → ε} (f e) (r : Region φ) + : PStepD Γ (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + := PStepD.rw $ PRwD.let1_op f e r + +@[match_pattern] +def PStepD.let1_pair {Γ : ℕ → ε} (a b) (r : Region φ) + : PStepD Γ (let1 (pair a b) r) + (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) r.vwk1.vwk1 + ) + := PStepD.rw $ PRwD.let1_pair a b r + +@[match_pattern] +def PStepD.let1_inl {Γ : ℕ → ε} (e) (r : Region φ) + : PStepD Γ (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + := PStepD.rw $ PRwD.let1_inl e r + +@[match_pattern] +def PStepD.let1_inr {Γ : ℕ → ε} (e) (r : Region φ) + : PStepD Γ (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + := PStepD.rw $ PRwD.let1_inr e r + +@[match_pattern] +def PStepD.let1_abort {Γ : ℕ → ε} (e) (r : Region φ) + : PStepD Γ (let1 (abort e) r) (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) + := PStepD.rw $ PRwD.let1_abort e r + +@[match_pattern] +def PStepD.let2_op {Γ : ℕ → ε} (f e) (r : Region φ) + : PStepD Γ (let2 (op f e) r) (let1 e $ let2 (op f (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) + := PStepD.rw $ PRwD.let2_op f e r + +@[match_pattern] +def PStepD.let2_pair {Γ : ℕ → ε} (a b) (r : Region φ) + : PStepD Γ (let2 (pair a b) r) (let1 a $ let1 (b.wk Nat.succ) $ r) + := PStepD.rw $ PRwD.let2_pair a b r + +@[match_pattern] +def PStepD.let2_abort {Γ : ℕ → ε} (e) (r : Region φ) + : PStepD Γ (let2 (abort e) r) (let1 e $ let2 (abort (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) + := PStepD.rw $ PRwD.let2_abort e r + +@[match_pattern] +def PStepD.case_op {Γ : ℕ → ε} (f e) (r s : Region φ) + : PStepD Γ (case (op f e) r s) + (let1 e $ case (op f (var 0)) (r.vwk (Nat.liftWk Nat.succ)) (s.vwk (Nat.liftWk Nat.succ)) + ) + := PStepD.rw $ PRwD.case_op f e r s + +@[match_pattern] +def PStepD.case_abort {Γ : ℕ → ε} (e) (r s : Region φ) + : PStepD Γ (case (abort e) r s) + (let1 e $ case (abort (var 0)) (r.vwk (Nat.liftWk Nat.succ)) (s.vwk (Nat.liftWk Nat.succ)) + ) + := PStepD.rw $ PRwD.case_abort e r s + +@[match_pattern] +def PStepD.let1_case {Γ : ℕ → ε} (a b) (r s : Region φ) + : PStepD Γ (let1 a $ case (b.wk Nat.succ) r s) + (case b (let1 (a.wk Nat.succ) r) (let1 (a.wk Nat.succ) s)) + := PStepD.rw $ PRwD.let1_case a b r s + +@[match_pattern] +def PStepD.let2_case {Γ : ℕ → ε} (a b) (r s : Region φ) + : PStepD Γ (let2 a $ case (b.wk (· + 2)) r s) + (case b (let2 (a.wk Nat.succ) r) (let2 (a.wk Nat.succ) s)) + := PStepD.rw $ PRwD.let2_case a b r s + +@[match_pattern] +def PStepD.cfg_br_lt {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : ℓ < n) + : PStepD Γ (cfg (br ℓ e) n G) (cfg ((G ⟨ℓ, h⟩).let1 e) n G) + := PStepD.rw $ PRwD.cfg_br_lt ℓ e n G h + +@[match_pattern] +def PStepD.cfg_let1 {Γ : ℕ → ε} (a : Term φ) (β n G) + : PStepD Γ (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G)) + := PStepD.rw $ PRwD.cfg_let1 a β n G + +@[match_pattern] +def PStepD.cfg_let2 {Γ : ℕ → ε} (a : Term φ) (β n G) + : PStepD Γ (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G)) + := PStepD.rw $ PRwD.cfg_let2 a β n G + +@[match_pattern] +def PStepD.cfg_case {Γ : ℕ → ε} (e : Term φ) (r s n G) + : PStepD Γ (cfg (case e r s) n G) + (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)) + ) + := PStepD.rw $ PRwD.cfg_case e r s n G + +@[match_pattern] +def PStepD.cfg_cfg {Γ : ℕ → ε} (β : Region φ) (n G n' G') + : PStepD Γ (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G'))) + := PStepD.rw $ PRwD.cfg_cfg β n G n' G' + inductive SCongD (P : Region φ → Region φ → Type u) : Region φ → Region φ → Type u | step : P r r' → SCongD P r r' | let1 (e) : SCongD P r r' → SCongD P (let1 e r) (let1 e r') @@ -268,6 +330,7 @@ inductive SCongD (P : Region φ → Region φ → Type u) : Region φ → Region | cfg_block (β n G i) : SCongD P r r' → SCongD P (cfg β n (Function.update G i r)) (cfg β n (Function.update G i r')) + abbrev RWD (P : Region φ → Region φ → Type u) := Corr.Path (SCongD P) @[match_pattern] @@ -276,115 +339,117 @@ def RWD.refl {P} (r : Region φ) : RWD P r r := Corr.Path.nil r @[match_pattern] def RWD.cons {P} {a b c : Region φ} : RWD P a b → SCongD P b c → RWD P a c := Corr.Path.cons +def RWD.single {P} {a b : Region φ} : SCongD P a b → RWD P a b := Corr.Path.single + def RWD.comp {P} {a b c : Region φ} : RWD P a b → RWD P b c → RWD P a c := Corr.Path.comp -def RWD.let1_beta (Γ : ℕ → ε) (e) (r : Region φ) (h : e.effect Γ = ⊥) +def RWD.let1_beta {Γ : ℕ → ε} (e) (r : Region φ) (h : e.effect Γ = ⊥) : RWD (PStepD Γ) (let1 e r) (r.vsubst e.subst0) := Corr.Path.single $ SCongD.step $ PStepD.let1_beta e r h -def RWD.case_inl (Γ : ℕ → ε) (e) (r s : Region φ) +def RWD.case_inl {Γ : ℕ → ε} (e) (r s : Region φ) : RWD (PStepD Γ) (case (inl e) r s) (let1 e r) := Corr.Path.single $ SCongD.step $ PStepD.case_inl e r s -def RWD.case_inr (Γ : ℕ → ε) (e) (r s : Region φ) +def RWD.case_inr {Γ : ℕ → ε} (e) (r s : Region φ) : RWD (PStepD Γ) (case (inr e) r s) (let1 e s) := Corr.Path.single $ SCongD.step $ PStepD.case_inr e r s -def RWD.let1_op (Γ : ℕ → ε) (f e) (r : Region φ) +def RWD.let1_op {Γ : ℕ → ε} (f e) (r : Region φ) : RWD (PStepD Γ) (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) := Corr.Path.single $ SCongD.step $ PStepD.let1_op f e r -def RWD.let1_pair (Γ : ℕ → ε) (a b) (r : Region φ) +def RWD.let1_pair {Γ : ℕ → ε} (a b) (r : Region φ) : RWD (PStepD Γ) (let1 (pair a b) r) - (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.vwk (Nat.liftWk (· + 2)) + (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) r.vwk1.vwk1 ) := Corr.Path.single $ SCongD.step $ PStepD.let1_pair a b r -def RWD.let1_inl (Γ : ℕ → ε) (e) (r : Region φ) +def RWD.let1_inl {Γ : ℕ → ε} (e) (r : Region φ) : RWD (PStepD Γ) (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) := Corr.Path.single $ SCongD.step $ PStepD.let1_inl e r -def RWD.let1_inr (Γ : ℕ → ε) (e) (r : Region φ) +def RWD.let1_inr {Γ : ℕ → ε} (e) (r : Region φ) : RWD (PStepD Γ) (let1 (inr e) r) (let1 e $ let1 (inr (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) := Corr.Path.single $ SCongD.step $ PStepD.let1_inr e r -def RWD.let1_abort (Γ : ℕ → ε) (e) (r : Region φ) +def RWD.let1_abort {Γ : ℕ → ε} (e) (r : Region φ) : RWD (PStepD Γ) (let1 (abort e) r) (let1 e $ let1 (abort (var 0)) $ r.vwk (Nat.liftWk Nat.succ)) := Corr.Path.single $ SCongD.step $ PStepD.let1_abort e r -def RWD.let2_op (Γ : ℕ → ε) (f e) (r : Region φ) +def RWD.let2_op {Γ : ℕ → ε} (f e) (r : Region φ) : RWD (PStepD Γ) (let2 (op f e) r) (let1 e $ let2 (op f (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) := Corr.Path.single $ SCongD.step $ PStepD.let2_op f e r -def RWD.let2_pair (Γ : ℕ → ε) (a b) (r : Region φ) +def RWD.let2_pair {Γ : ℕ → ε} (a b) (r : Region φ) : RWD (PStepD Γ) (let2 (pair a b) r) (let1 a $ let1 (b.wk Nat.succ) $ r) := Corr.Path.single $ SCongD.step (PStepD.let2_pair a b r) -def RWD.let2_abort (Γ : ℕ → ε) (e) (r : Region φ) +def RWD.let2_abort {Γ : ℕ → ε} (e) (r : Region φ) : RWD (PStepD Γ) (let2 (abort e) r) (let1 e $ let2 (abort (var 0)) $ r.vwk (Nat.liftnWk 2 Nat.succ)) := Corr.Path.single $ SCongD.step $ PStepD.let2_abort e r -def RWD.case_op (Γ : ℕ → ε) (f e) (r s : Region φ) +def RWD.case_op {Γ : ℕ → ε} (f e) (r s : Region φ) : RWD (PStepD Γ) (case (op f e) r s) (let1 e $ case (op f (var 0)) (r.vwk (Nat.liftWk Nat.succ)) (s.vwk (Nat.liftWk Nat.succ)) ) := Corr.Path.single $ SCongD.step $ PStepD.case_op f e r s -def RWD.case_abort (Γ : ℕ → ε) (e) (r s : Region φ) +def RWD.case_abort {Γ : ℕ → ε} (e) (r s : Region φ) : RWD (PStepD Γ) (case (abort e) r s) (let1 e $ case (abort (var 0)) (r.vwk (Nat.liftWk Nat.succ)) (s.vwk (Nat.liftWk Nat.succ)) ) := Corr.Path.single $ SCongD.step $ PStepD.case_abort e r s -def RWD.let1_case (Γ : ℕ → ε) (a b) (r s : Region φ) +def RWD.let1_case {Γ : ℕ → ε} (a b) (r s : Region φ) : RWD (PStepD Γ) (let1 a $ case (b.wk Nat.succ) r s) (case b (let1 (a.wk Nat.succ) r) (let1 (a.wk Nat.succ) s)) := Corr.Path.single $ SCongD.step $ PStepD.let1_case a b r s -def RWD.let2_case (Γ : ℕ → ε) (a b) (r s : Region φ) +def RWD.let2_case {Γ : ℕ → ε} (a b) (r s : Region φ) : RWD (PStepD Γ) (let2 a $ case (b.wk (· + 2)) r s) (case b (let2 (a.wk Nat.succ) r) (let2 (a.wk Nat.succ) s)) := Corr.Path.single $ SCongD.step $ PStepD.let2_case a b r s -def RWD.cfg_br_lt (Γ : ℕ → ε) (ℓ) (e : Term φ) (n G) (h : ℓ < n) +def RWD.cfg_br_lt {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : ℓ < n) : RWD (PStepD Γ) (cfg (br ℓ e) n G) (cfg ((G ⟨ℓ, h⟩).let1 e) n G) := Corr.Path.single $ SCongD.step $ PStepD.cfg_br_lt ℓ e n G h -def RWD.cfg_br_ge (Γ : ℕ → ε) (ℓ) (e : Term φ) (n G) (h : n ≤ ℓ) +def RWD.cfg_br_ge {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : n ≤ ℓ) : RWD (PStepD Γ) (cfg (br ℓ e) n G) (br (ℓ - n) e) := Corr.Path.single $ SCongD.step $ PStepD.cfg_br_ge ℓ e n G h -def RWD.cfg_let1 (Γ : ℕ → ε) (a : Term φ) (β n G) - : RWD (PStepD Γ) (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk Nat.succ ∘ G)) +def RWD.cfg_let1 {Γ : ℕ → ε} (a : Term φ) (β n G) + : RWD (PStepD Γ) (cfg (let1 a β) n G) (let1 a $ cfg β n (vwk1 ∘ G)) := Corr.Path.single $ SCongD.step $ PStepD.cfg_let1 a β n G -def RWD.cfg_let2 (Γ : ℕ → ε) (a : Term φ) (β n G) +def RWD.cfg_let2 {Γ : ℕ → ε} (a : Term φ) (β n G) : RWD (PStepD Γ) (cfg (let2 a β) n G) (let2 a $ cfg β n (vwk (· + 2) ∘ G)) := Corr.Path.single $ SCongD.step $ PStepD.cfg_let2 a β n G -def RWD.cfg_case (Γ : ℕ → ε) (e : Term φ) (r s n G) +def RWD.cfg_case {Γ : ℕ → ε} (e : Term φ) (r s n G) : RWD (PStepD Γ) (cfg (case e r s) n G) (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)) ) := Corr.Path.single $ SCongD.step $ PStepD.cfg_case e r s n G -def RWD.cfg_cfg (Γ : ℕ → ε) (β : Region φ) (n G n' G') +def RWD.cfg_cfg {Γ : ℕ → ε} (β : Region φ) (n G n' G') : RWD (PStepD Γ) (cfg (cfg β n G) n' G') (cfg β (n + n') (Fin.addCases G (lwk (· + n) ∘ G'))) := Corr.Path.single $ SCongD.step $ PStepD.cfg_cfg β n G n' G' -def RWD.wk_cfg (Γ : ℕ → ε) (β : Region φ) (n G k) (ρ : Fin k → Fin n) /-(hρ : Function.Bijective ρ)-/ +def RWD.wk_cfg {Γ : ℕ → ε} (β : Region φ) (n G k) (ρ : Fin k → Fin n) /-(hρ : Function.Bijective ρ)-/ : RWD (PStepD Γ) (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G)) (cfg β k (G ∘ ρ)) := Corr.Path.single $ SCongD.step $ PStepD.wk_cfg β n G k ρ -def RWD.dead_cfg_left (Γ : ℕ → ε) (β : Region φ) (n G m G') +def RWD.dead_cfg_left {Γ : ℕ → ε} (β : Region φ) (n G m G') : RWD (PStepD Γ) (cfg (β.lwk (· + n)) (n + m) (Fin.addCases G (lwk (· + n) ∘ G'))) (cfg β m G') := Corr.Path.single $ SCongD.step $ PStepD.dead_cfg_left β n G m G' -def RWD.swap_cfg' (Γ : ℕ → ε) (β : Region φ) (n G m G') +def RWD.swap_cfg' {Γ : ℕ → ε} (β : Region φ) (n G m G') : RWD (PStepD Γ) (cfg (lwk (Fin.toNatWk (Fin.swapAdd n m)) β) @@ -409,7 +474,7 @@ def RWD.cast {P} {r₀ r₀' r₁ r₁' : Region φ} (hr₀ : r₀ = r₀') (hr : RWD P r₀' r₁' := Corr.Path.cast hr₀ hr₁ h -def RWD.swap_cfg (Γ : ℕ → ε) (β : Region φ) (n G m G') +def RWD.swap_cfg {Γ : ℕ → ε} (β : Region φ) (n G m G') : RWD (PStepD Γ) (cfg β (n + m) (Fin.addCases G G')) (cfg @@ -425,7 +490,7 @@ def RWD.swap_cfg (Γ : ℕ → ε) (β : Region φ) (n G m G') ] simp [<-Fin.toNatWk_comp, Fin.addCases_natAdd_castAdd_nil] ) - (swap_cfg' Γ + (swap_cfg' (β.lwk (Fin.toNatWk (Fin.addCases (Fin.natAdd m) (Fin.castAdd n)))) m (lwk (Fin.toNatWk (Fin.addCases (Fin.natAdd m) (Fin.castAdd n))) ∘ G') @@ -433,10 +498,10 @@ def RWD.swap_cfg (Γ : ℕ → ε) (β : Region φ) (n G m G') (lwk (Fin.toNatWk (Fin.addCases (Fin.natAdd m) (Fin.castAdd n))) ∘ G))) (by simp [Fin.comp_addCases, Fin.swapAdd]) -def RWD.let1V0_id (Γ : ℕ → ε) (r : Region φ) (hΓ : Γ 0 = ⊥) +def RWD.let1V0_id {Γ : ℕ → ε} (r : Region φ) (hΓ : Γ 0 = ⊥) : RWD (PStepD Γ) r.let1V0 r := cast_trg - (let1_beta Γ (Term.var 0) (r.vwk (Nat.liftWk Nat.succ)) hΓ) + (let1_beta (Term.var 0) (r.vwk (Nat.liftWk Nat.succ)) hΓ) (by rw [<-vsubst_fromWk_apply, vsubst_vsubst, vsubst_id']; funext i; cases i <;> rfl) -- TODO: prefunctor lore @@ -553,26 +618,26 @@ def RWD.cfg_blocks (β n) (G G' : Fin n → Region φ) : RWD P (Region.cfg β n G) (Region.cfg β n G') := cast_trg (cfg_blocks_partial β n G G' h n) (by simp) -def RWD.dead_cfg_right (Γ : ℕ → ε) (β : Region φ) (n G m G') +def RWD.dead_cfg_right {Γ : ℕ → ε} (β : Region φ) (n G m G') : RWD (PStepD Γ) (cfg (β.lwk (n.liftnWk (· + m))) (n + m) (Fin.addCases (lwk (n.liftnWk (· + m)) ∘ G) G')) (cfg β n G) := - (cast_trg (swap_cfg Γ (β.lwk (n.liftnWk (· + m))) n (lwk (n.liftnWk (· + m)) ∘ G) m G') + (cast_trg (swap_cfg (β.lwk (n.liftnWk (· + m))) n (lwk (n.liftnWk (· + m)) ∘ G) m G') (by rw [Fin.comp_addCases, lwk_lwk, <-Function.comp.assoc, comp_lwk, Fin.toNatWk_swapAdd_comp_liftnWk_add] )).comp - (dead_cfg_left Γ β m _ n G) + (dead_cfg_left β m _ n G) def RWD.cfg_elim {Γ : ℕ → ε} (β : Region φ) (n G) : RWD (PStepD Γ) (cfg (β.lwk (· + n)) n G) β := match β with - | Region.br ℓ e => (cfg_br_ge Γ (ℓ + n) e n G (by simp)).cast_trg (by simp) - | Region.let1 a β => (cfg_let1 Γ a (β.lwk (· + n)) n G).comp (let1 a (cfg_elim β n _)) - | Region.let2 a β => (cfg_let2 Γ a (β.lwk (· + n)) n G).comp (let2 a (cfg_elim β n _)) + | Region.br ℓ e => (cfg_br_ge (ℓ + n) e n G (by simp)).cast_trg (by simp) + | Region.let1 a β => (cfg_let1 a (β.lwk (· + n)) n G).comp (let1 a (cfg_elim β n _)) + | Region.let2 a β => (cfg_let2 a (β.lwk (· + n)) n G).comp (let2 a (cfg_elim β n _)) | Region.case e r s => - (cfg_case Γ e (r.lwk (· + n)) (s.lwk (· + n)) n G).comp + (cfg_case e (r.lwk (· + n)) (s.lwk (· + n)) n G).comp (case e (cfg_elim r n _) (cfg_elim s n _)) - | Region.cfg β n' G' => (cfg_cfg Γ _ _ _ _ _).comp (dead_cfg_right Γ _ _ _ _ _) + | Region.cfg β n' G' => (cfg_cfg _ _ _ _ _).comp (dead_cfg_right _ _ _ _ _) end Region diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst.lean index 2813f93..6e4b6b5 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Subst.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Subst.lean @@ -1164,8 +1164,12 @@ theorem lsubst_id' : @lsubst φ (λi => Region.br i (Term.var 0)) = id := funext /-- Create a substitution from a label renaming -/ def Subst.fromLwk (ρ : ℕ -> ℕ): Subst φ := λn => Region.br (ρ n) (Term.var 0) +@[simp] theorem Subst.vwk_lift_comp_fromLwk (ρ σ) : vwk (Nat.liftWk ρ) ∘ fromLwk σ = @fromLwk φ σ := rfl +@[simp] +theorem Subst.vwk_lift_comp_id (ρ) : vwk (Nat.liftWk ρ) ∘ Subst.id = @Subst.id φ := rfl + @[simp] theorem Subst.fromLwk_vlift (ρ) : (@fromLwk φ ρ).vlift = fromLwk ρ := rfl diff --git a/lake-manifest.json b/lake-manifest.json index 19c8147..9997ba9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "6a63eb6a326181df29d95a84ce1f16c1145e66d8", + "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "bfaec997eb25d276dfb9180d1834e2b4cda60315", + "rev": "659d35143a857ceb5ba7c02a0e1530a1c7aec70c", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -67,7 +67,7 @@ {"url": "https://github.com/imbrem/discretion.git", "type": "git", "subDir": null, - "rev": "e7739c31128205ecdc5e892dd35161c4812c5f6e", + "rev": "4935f56c515d9fe8037d78af4cc009b065045a11", "name": "discretion", "manifestFile": "lake-manifest.json", "inputRev": "main",