Made cfg_br_ge derived

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -230,13 +230,20 @@ def PRwD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}
         rw [Nat.add_comm n n', <-Nat.add_assoc]
         simp [h]
   )
+  | cfg_zero β G => by
+    simp only [lsubst, Subst.liftn_zero]
+    apply cfg_zero
 
 def PStepD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}
   (p : PStepD Γ r₀ r₀') (n) (r₁ : Region φ)
   : 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
+  | 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
+  | dead_cfg_left β n G m G' => sorry
 
 -- TODO: factor out as more general lifting lemma
 def SCongD.lsubst_alpha {Γ : ℕ → ε} {r₀ r₀'}

DeBruijnSSA/BinSyntax/Syntax/Rewrite.lean

@@ -193,6 +193,7 @@ inductive PRwD (Γ : ℕ → ε) : Region φ → Region φ → Type
       (case e (cfg r n (vwk Nat.succ ∘ G)) (cfg s n (vwk Nat.succ ∘ G)))
   | 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) β
 
 def PRwD.cast_src {Γ : ℕ → ε} {r₀ r₀' r₁ : Region φ} (h : r₀ = r₀') (p : PRwD Γ r₀ r₁)
   : PRwD Γ r₀' r₁ := h ▸ p
@@ -211,7 +212,7 @@ inductive PStepD (Γ : ℕ → ε) : Region φ → Region φ → Type
   | 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)
-  | cfg_br_ge (ℓ e n G) (h : n ≤ ℓ) : PStepD Γ (cfg (br ℓ e) n G) (br (ℓ - n) e)
+  -- | 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))
@@ -318,6 +319,19 @@ 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'
 
+@[match_pattern]
+def PStepD.cfg_zero {Γ : ℕ → ε} (β : Region φ) (G)
+  : PStepD Γ (cfg β 0 G) β := PStepD.rw $ PRwD.cfg_zero β G
+
+def PStepD.cast_trg {Γ : ℕ → ε} {r₀ r₁ r₁' : Region φ} (p : PStepD Γ r₀ r₁) (h : r₁ = r₁')
+  : PStepD Γ r₀ r₁' := h ▸ p
+
+def PStepD.cast_src {Γ : ℕ → ε} {r₀ r₀' r₁ : Region φ} (h : r₀' = r₀) (p : PStepD Γ r₀ r₁)
+  : PStepD Γ r₀' r₁ := h ▸ p
+
+def PStepD.cast {Γ : ℕ → ε} {r₀ r₀' r₁ r₁' : Region φ} (h₀ : r₀ = r₀') (h₁ : r₁ = r₁')
+  (p : PStepD Γ r₀ r₁) : PStepD Γ r₀' r₁' := h₁ ▸ h₀ ▸ p
+
 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')
@@ -345,109 +359,108 @@ def RWD.comp {P} {a b c : Region φ} : RWD P a b → RWD P b c → RWD P a c :=
 
 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
+  := single $ SCongD.step $ PStepD.let1_beta e r h
 
 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
+  := single $ SCongD.step $ PStepD.case_inl e r s
 
 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
+  := single $ SCongD.step $ PStepD.case_inr e r s
 
 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
+  := single $ SCongD.step $ PStepD.let1_op f e r
 
 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.vwk1.vwk1
   )
-  := Corr.Path.single $ SCongD.step $ PStepD.let1_pair a b r
+  := single $ SCongD.step $ PStepD.let1_pair a b r
 
 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
+  := single $ SCongD.step $ PStepD.let1_inl e r
 
 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
+  := single $ SCongD.step $ PStepD.let1_inr e r
 
 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
+  := single $ SCongD.step $ PStepD.let1_abort e r
 
 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
+  := single $ SCongD.step $ PStepD.let2_op f e r
 
 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)
+  := single $ SCongD.step (PStepD.let2_pair a b r)
 
 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
+  := single $ SCongD.step $ PStepD.let2_abort e r
 
 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
+  := single $ SCongD.step $ PStepD.case_op f e r s
 
 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
+  := single $ SCongD.step $ PStepD.case_abort e r s
 
 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
+  := single $ SCongD.step $ PStepD.let1_case a b r s
 
 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
+  := single $ SCongD.step $ PStepD.let2_case a b r s
 
 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 ≤ ℓ)
-  : RWD (PStepD Γ) (cfg (br ℓ e) n G) (br (ℓ - n) e)
-  := Corr.Path.single $ SCongD.step $ PStepD.cfg_br_ge ℓ e n G h
+  := single $ SCongD.step $ PStepD.cfg_br_lt ℓ e n G h
 
 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
+  := single $ SCongD.step $ PStepD.cfg_let1 a β 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
+  := single $ SCongD.step $ PStepD.cfg_let2 a β 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
+  := single $ SCongD.step $ PStepD.cfg_case e r s 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'
+  := single $ SCongD.step $ PStepD.cfg_cfg β n G n' G'
+
+def RWD.cfg_zero {Γ : ℕ → ε} (β : Region φ) (G)
+  : RWD (PStepD Γ) (cfg β 0 G) β := single $ SCongD.step $ PStepD.cfg_zero β G
 
 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 ρ
+  := single $ SCongD.step $ PStepD.wk_cfg β n G k ρ
 
 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'
+  := single $ SCongD.step $ PStepD.dead_cfg_left β n G m G'
 
 def RWD.swap_cfg' {Γ : ℕ → ε} (β : Region φ) (n G m G')
   : RWD (PStepD Γ)
@@ -630,14 +643,24 @@ def RWD.dead_cfg_right {Γ : ℕ → ε} (β : Region φ) (n G m 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.case e r s =>
-    (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 _ _ _ _ _)
+  :=
+  let s : RWD (PStepD Γ)
+    (cfg (β.lwk (· + n)) n G)
+    (cfg (β.lwk (· + n)) (n + 0) (Fin.addCases G (lwk (· + n) ∘ Fin.elim0)))
+    := RWD.of_eq (by simp [Fin.addCases_zero])
+  (s.comp (dead_cfg_left β n G 0 Fin.elim0)).comp (RWD.cfg_zero _ _)
+  -- := 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.case e r s =>
+  --   (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 _ _ _ _ _)
+
+def RWD.cfg_br_ge {Γ : ℕ → ε} (ℓ) (e : Term φ) (n G) (h : n ≤ ℓ)
+  : RWD (PStepD Γ) (cfg (br ℓ e) n G) (br (ℓ - n) e)
+  := cast_src (by simp [h]) (cfg_elim (br (ℓ - n) e) n G)
 
 end Region
 

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981",
+   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
+   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
+   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "659d35143a857ceb5ba7c02a0e1530a1c7aec70c",
+   "rev": "bdd39e92aed38bcac548ae0859ba269c95dbc2f2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/imbrem/discretion.git",
    "type": "git",
    "subDir": null,
-   "rev": "4935f56c515d9fe8037d78af4cc009b065045a11",
+   "rev": "2fa59d9ba61ab32092229dc7bdd739c0df030b31",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc1
+leanprover/lean4:v4.9.0-rc2