lsubst alpha

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -242,7 +242,19 @@ def PStepD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}
   | let1_beta e r he => cast_trg (let1_beta e _ he) (by rw [vsubst_subst0_lsubst_vlift])
   | case_inl e r s => case_inl e _ _
   | case_inr e r s => case_inr e _ _
-  | wk_cfg β n G k ρ => sorry
+  | wk_cfg β n G k ρ => by
+    rw [
+      lsubst_cfg, lsubst_cfg,
+      lsubst_liftn_lwk_toNatWk,
+      <-Function.comp.assoc,
+      Subst.vlift_liftn_comm,
+      lsubst_liftn_comp_lwk_toNatWk,
+      Function.comp.assoc
+    ]
+    apply cast_trg
+    apply wk_cfg
+    rw [Subst.vlift_liftn_comm]
+    rfl
   | dead_cfg_left β n G m G' =>
     cast_src (by
       simp only [lsubst_cfg, Fin.comp_addCases, liftn_alpha, vlift_alpha, lsubst_lwk, lwk_lsubst]

DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean

@@ -194,6 +194,10 @@ 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')))
   | cfg_zero (β G) : PRwD Γ (cfg β 0 G) β
+  -- | cfg_perm (β n G k) (ρ : Fin k → Fin n) /-(hρ : Function.Bijective ρ)-/ :
+  --   PRwD Γ
+  --     (cfg (lwk (Fin.toNatWk ρ) β) n (lwk (Fin.toNatWk ρ) ∘ G))
+  --     (cfg β k (G ∘ ρ))
 
 def PRwD.cast_src {Γ : ℕ → ε} {r₀ r₀' r₁ : Region φ} (h : r₀ = r₀') (p : PRwD Γ r₀ r₁)
   : PRwD Γ r₀' r₁ := h ▸ p

DeBruijnSSA/BinSyntax/Syntax/Subst.lean

@@ -1466,6 +1466,47 @@ def let1Br : Subst φ := λℓ => (br ℓ (Term.var 0)).let1 (Term.var 0)
 
 theorem Subst.let1V0_comp_id : @let1V0 φ ∘ id = let1Br := rfl
 
+theorem lwk_lsubst_swap (σ σ' : Subst φ) (ρ ρ') (r : Region φ)
+  (h : lwk ρ ∘ σ = σ' ∘ ρ')
+  : (r.lsubst σ).lwk ρ = (r.lwk ρ').lsubst σ'
+  := by rw [lwk_lsubst, lsubst_lwk, h]
+
+theorem lsubst_lwk_swap (σ σ' : Subst φ) (ρ ρ') (r : Region φ)
+  (h : σ ∘ ρ = lwk ρ' ∘ σ')
+  : (r.lwk ρ).lsubst σ = (r.lsubst σ').lwk ρ'
+  := by rw [lwk_lsubst, lsubst_lwk, h]
+
+theorem lwk_lsubst_comm (σ : Subst φ) (ρ) (r : Region φ)
+  (h : lwk ρ ∘ σ = σ ∘ ρ)
+  : (r.lsubst σ).lwk ρ = (r.lwk ρ).lsubst σ
+  := lwk_lsubst_swap σ σ ρ ρ r h
+
+theorem lsubst_lwk_comm (σ : Subst φ) (ρ) (r : Region φ)
+  (h : σ ∘ ρ = lwk ρ ∘ σ)
+  : (r.lwk ρ).lsubst σ = (r.lsubst σ).lwk ρ
+  := lsubst_lwk_swap σ σ ρ ρ r h
+
+theorem Subst.liftn_comp_toNatWk {ρ : Fin k → Fin n}
+  : (@liftn φ n σ) ∘ (Fin.toNatWk ρ) = (lwk $ Fin.toNatWk ρ) ∘ (@liftn φ k σ) := by
+  funext i
+  simp only [Function.comp_apply, liftn, Fin.toNatWk]
+  split
+  case isTrue h => simp [Fin.toNatWk, h]
+  case isFalse h =>
+    simp [Nat.sub_add_cancel (Nat.le_of_not_lt h), h, lwk_lwk, Fin.toNatWk_comp_add]
+
+theorem lsubst_liftn_lwk_toNatWk {ρ : Fin k → Fin n}
+    : (lsubst (@Subst.liftn φ n σ) (lwk (Fin.toNatWk ρ) r))
+      = (lwk (Fin.toNatWk ρ) (lsubst (Subst.liftn k σ) r)) := by
+  apply lsubst_lwk_swap
+  apply Subst.liftn_comp_toNatWk
+
+theorem lsubst_liftn_comp_lwk_toNatWk {ρ : Fin k → Fin n}
+    : (lsubst (Subst.liftn n σ) ∘ lwk (Fin.toNatWk ρ))
+      = (lwk (Fin.toNatWk ρ) ∘ lsubst (Subst.liftn k σ)) := by
+  funext r
+  apply lsubst_liftn_lwk_toNatWk
+
 end Region
 
 /-- Substitute the free labels in this control-flow graph -/

lake-manifest.json

@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "bdd39e92aed38bcac548ae0859ba269c95dbc2f2",
+   "rev": "009daa3a647f6c05cfffe3581c322317821212ae",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/imbrem/discretion.git",
    "type": "git",
    "subDir": null,
-   "rev": "2fa59d9ba61ab32092229dc7bdd739c0df030b31",
+   "rev": "fda507a630cd395ae8dff7d9c8b4307e3678cc0f",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",