PStepD.effect_le

DeBruijnSSA/BinSyntax/Syntax/Effect/Definitions.lean

@@ -265,6 +265,11 @@ theorem Region.effect_lwk (ρ : ℕ → ℕ) (Γ : ℕ → ε) (r : Region φ)
   := by induction r generalizing Γ ρ
     <;> simp [Term.effect_wk, Nat.liftBot_comp_liftWk, *]
 
+@[simp]
+theorem Region.effect_comp_lwk (ρ : ℕ → ℕ) (Γ : ℕ → ε)
+  : effect Γ ∘ @lwk φ ρ = effect Γ
+  := by funext i; simp [effect_lwk]
+
 /-- Infer the control effect of a `Region`, _without_ taking control-flow into account -/
 @[simp]
 def Region.control_effect (Γ : ℕ → ε) : Region φ → ε

DeBruijnSSA/BinSyntax/Syntax/Effect/Subst.lean

@@ -22,6 +22,13 @@ theorem effect_liftBot_lift (Γ : ℕ → ε) (σ : Subst φ)
   : effect (Nat.liftBot Γ) (σ.lift) = Nat.liftBot (effect Γ σ)
   := by funext k; cases k <;> simp [Nat.liftBot, Term.effect_wk]
 
+theorem effect_liftnBot_liftn (Γ : ℕ → ε) (σ : Subst φ)
+  : effect (Nat.liftnBot n Γ) (σ.liftn n) = Nat.liftnBot n (effect Γ σ) := by
+  simp only [Subst.liftn_eq_iterate_lift_apply, Nat.liftnWk_eq_iterate_liftWk, Nat.liftnBot_iterate]
+  induction n with
+  | zero => rfl
+  | succ n I => simp only [Function.iterate_succ', Function.comp_apply, effect_liftBot_lift, I]
+
 end Subst
 
 theorem effect_subst (Γ : ℕ → ε) (σ : Subst φ) (e : Term φ)
@@ -48,9 +55,10 @@ def hasTrgEffect (target : ℕ) (Γ : ℕ → ε) (σ : Subst φ) (e : ε) : Pro
 
 end Subst
 
--- theorem effect_vsubst (Γ : ℕ → ε) (σ : Term.Subst φ) (t : Terminator φ)
---   : (t.vsubst σ).effect Γ = t.effect (σ.effect Γ)
---     := sorry --by induction t generalizing Γ σ <;> simp [Term.effect_subst, *]
+theorem effect_vsubst (Γ : ℕ → ε) (σ : Term.Subst φ) (t : Terminator φ)
+  : (t.vsubst σ).effect Γ = t.effect (σ.effect Γ)
+    := by induction t generalizing Γ σ
+    <;> simp [Term.effect_subst, Term.Subst.effect_liftBot_lift, *]
 
 end Terminator
 
@@ -70,6 +78,13 @@ def hasTrgEffect (target : ℕ) (Γ : ℕ → ε) (σ : Subst φ) (e : ε) : Pro
 
 end Subst
 
+theorem effect_vsubst (Γ : ℕ → ε) (σ : Term.Subst φ) (r : Region φ)
+  : (r.vsubst σ).effect Γ = r.effect (σ.effect Γ)
+    := by induction r generalizing Γ σ
+    <;> simp [Term.effect_subst,
+      Term.Subst.effect_liftBot_lift,
+      Term.Subst.effect_liftnBot_liftn, *]
+
 end Region
 
 end Definitions

DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean

@@ -5,7 +5,7 @@ import Mathlib.CategoryTheory.PathCategory
 import Discretion.Correspondence.Definitions
 
 import DeBruijnSSA.BinSyntax.Syntax.Subst
-import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions
+import DeBruijnSSA.BinSyntax.Syntax.Effect.Subst
 
 namespace BinSyntax
 
@@ -410,6 +410,34 @@ def PStepD.cast_src {Γ : ℕ → ε} {r₀ r₀' r₁ : Region φ} (h : r₀' =
 def PStepD.cast {Γ : ℕ → ε} {r₀ r₀' r₁ r₁' : Region φ} (h₀ : r₀ = r₀') (h₁ : r₁ = r₁')
   (p : PStepD Γ r₀ r₁) : PStepD Γ r₀' r₁' := h₁ ▸ h₀ ▸ p
 
+theorem PStepD.effect_le {Γ : ℕ → ε} {r r' : Region φ} (p : PStepD Γ r r')
+  : r'.effect Γ ≤ r.effect Γ := by
+  cases p with
+  | rw p => rw [p.effect]
+  | rw_symm p => rw [p.effect]
+  | let1_beta _ _ he =>
+    apply le_of_eq
+    simp only [effect_vsubst, Subst.effect, effect, he, ge_iff_le, bot_le, sup_of_le_right]
+    congr
+    funext k
+    cases k with
+    | zero => simp [he, Nat.liftBot]
+    | succ k => rfl
+  | case_inl _ _ _ => simp
+  | case_inr e r s =>
+    simp only [effect, Term.effect]
+    rw [sup_assoc, sup_comm (r.effect _), <-sup_assoc]
+    simp
+  | wk_cfg _ _ _ _ _ =>
+    simp only [effect_cfg, effect_lwk, <-Function.comp.assoc, effect_comp_lwk]
+    apply sup_le_sup_left
+    apply Fin.sup_comp_le
+  | dead_cfg_left _ _ _ _ =>
+    simp only [effect_cfg, effect_lwk, Fin.comp_addCases, Fin.sup_addCases]
+    apply sup_le_sup_left
+    apply le_sup_of_le_right
+    rw [<-Function.comp.assoc, effect_comp_lwk]
+
 -- TODO: PStepD is effect monotonic
 
 inductive SCongD (P : Region φ → Region φ → Type u) : Region φ → Region φ → Type u

lake-manifest.json

@@ -67,7 +67,7 @@
   {"url": "https://github.com/imbrem/discretion.git",
    "type": "git",
    "subDir": null,
-   "rev": "806f74d6f6a0528288c44a473b1c00e09869e8f4",
+   "rev": "55551dc6588c63676811094add43a73a28b9bbe1",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",