Finite attempt...

DeBruijnSSA/BinSyntax/Fin/Syntax/Definitions.lean

@@ -0,0 +1,56 @@
+import Discretion.Wk.Nat
+import Discretion.Wk.Fin
+
+namespace BinSyntax
+
+/-! ### Basic syntax definitions
+
+Free variables and simple coercions are given immediately after each definition to give an idea of how
+the de-Bruijn indices are supposed to be interpreted.
+ -/
+section Definitions
+
+/-- A simple term, consisting of variables, operations, pairs, units, and booleans -/
+inductive FTerm (φ : Type _) (vars : ℕ) : Type _
+  | var : Fin vars → FTerm φ vars
+  | op : φ → FTerm φ vars → FTerm φ vars
+  | pair : FTerm φ vars → FTerm φ vars → FTerm φ vars
+  | unit : FTerm φ vars
+  | inl : FTerm φ vars → FTerm φ vars
+  | inr : FTerm φ vars → FTerm φ vars
+  | abort : FTerm φ vars → FTerm φ vars
+
+/-- Rename the variables in a `Term` using `ρ` -/
+@[simp]
+def FTerm.wk (ρ : Fin varsIn → Fin varsOut) : FTerm φ varsIn → FTerm φ varsOut
+  | var x => var (ρ x)
+  | op f e => op f (wk ρ e)
+  | pair l r => pair (wk ρ l) (wk ρ r)
+  | unit => unit
+  | inl a => inl (wk ρ a)
+  | inr a => inr (wk ρ a)
+  | abort a => abort (wk ρ a)
+
+/-- A single-entry multiple-exit region, similar to [A-normal
+  form](https://en.wikipedia.org/wiki/A-normal_form) -/
+inductive FRegion (φ : Type _) : ℕ → ℕ → Type _
+  | br : Fin labels → FTerm φ vars → FRegion φ labels vars
+  | case : FTerm φ vars →
+    FRegion φ labels (vars + 1) →
+    FRegion φ labels (vars + 1) →
+    FRegion φ labels vars
+  | let1 : FTerm φ vars → FRegion φ labels (vars + 1) → FRegion φ labels vars
+  | let2 : FTerm φ vars → FRegion φ labels (vars + 2) → FRegion φ labels vars
+  | cfg (cfgLabels : Nat) (β : FRegion φ (labels + cfgLabels) vars) :
+    (Fin cfgLabels → FRegion φ (labels + cfgLabels) (vars + 1)) → FRegion φ labels vars
+
+-- Why is recursion failing here???
+
+-- /-- Rename the variables in a `Region` using `ρ` -/
+-- @[simp]
+-- def FRegion.vwk (ρ : Fin varsIn → Fin varsOut) : FRegion φ labels varsIn → FRegion φ labels varsOut
+--   | br n e => br n (e.wk ρ)
+--   | case e s t => case (e.wk ρ) (vwk (Fin.liftWk ρ) s) (vwk (Fin.liftWk ρ) t)
+--   | let1 e t => let1 (e.wk ρ) (vwk (Fin.liftWk ρ) t)
+--   | let2 e t => let2 (e.wk ρ) (vwk (Fin.liftnWk 2 ρ) t)
+--   | cfg n β G => cfg n (β.vwk ρ) (λi => (G i).vwk (Fin.liftWk ρ))

DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean

@@ -14,10 +14,72 @@ def Term.WfD.subst₂ {Γ : Ctx α ε} {a b : Term φ}
   | ⟨1, _⟩ => hb
   | ⟨n + 2, h⟩ => var ⟨by simp at h; exact h, le_refl _⟩
 
-structure HaveTarget (Γ : Ctx α ε) (L : LCtx α) (r r' : Region φ) where
+structure Region.HaveTrg (Γ : Ctx α ε) (L : LCtx α) (r r' : Region φ) where
   left : r.WfD Γ L
   right : r'.WfD Γ L
 
+inductive Region.WfD.Cong (P : Ctx α ε → LCtx α → Region φ → Region φ → Type _)
+  : Ctx α ε → LCtx α → Region φ → Region φ → Type _
+  | step : P Γ L r r' → Cong P Γ L r r'
+  | case_left : e.WfD Γ ⟨Ty.coprod A B, ⊥⟩ → Cong P (⟨A, ⊥⟩::Γ) L r r' → s.WfD (⟨B, ⊥⟩::Γ) L
+    → Cong P Γ L (Region.case e r s) (Region.case e r' s)
+  | case_right : e.WfD Γ ⟨Ty.coprod A B, ⊥⟩ → r.WfD (⟨A, ⊥⟩::Γ) L → Cong P (⟨B, ⊥⟩::Γ) L s s'
+    → Cong P Γ L (Region.case e r s) (Region.case e r s')
+  | let1 : e.WfD Γ ⟨A, e'⟩ → Cong P (⟨A, ⊥⟩::Γ) L r r'
+    → Cong P Γ L (Region.let1 e r) (Region.let1 e r')
+  | let2 : e.WfD Γ ⟨Ty.prod A B, e'⟩ → Cong P (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L r r'
+    → Cong P Γ L (Region.let2 e r) (Region.let2 e r')
+  | cfg_entry (R : LCtx α) :
+    (hR : R.length = n) →
+    Cong P Γ (R ++ L) β β' →
+    (∀i : Fin n, (G i).WfD (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
+    Cong P Γ L (Region.cfg β n G) (Region.cfg β' n G)
+  | cfg_block (R : LCtx α) :
+    (hR : R.length = n) →
+    β.WfD Γ (R ++ L) →
+    (hG : ∀i : Fin n, (G i).WfD (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
+    (i : Fin n) →
+    Cong P (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L) r r' →
+    Cong P Γ L (Region.cfg β n (Function.update G i r)) (Region.cfg β n (Function.update G i r'))
+
+def Region.WfD.Cong.left {P : Ctx α ε → LCtx α → Region φ → Region φ → Type _} {Γ L r r'}
+  (toLeft : ∀{Γ L r r'}, P Γ L r r' → r.WfD Γ L) : Cong P Γ L r r' → r.WfD Γ L
+  | step p => toLeft p
+  | case_left de pr ds => case de (pr.left toLeft) ds
+  | case_right de dr ps => case de dr (ps.left toLeft)
+  | let1 de pr => WfD.let1 de (pr.left toLeft)
+  | let2 de pr => WfD.let2 de (pr.left toLeft)
+  | cfg_entry R hR pβ dG => WfD.cfg _ R hR (pβ.left toLeft) dG
+  | cfg_block R hR dβ dG i pr => WfD.cfg _ R hR dβ (λk => by
+    if h : k = i then
+      cases h
+      simp only [Function.update_same]
+      exact (pr.left toLeft)
+    else
+      simp only [ne_eq, h, not_false_eq_true, Function.update_noteq]
+      exact dG k
+  )
+
+def Region.WfD.Cong.right {P : Ctx α ε → LCtx α → Region φ → Region φ → Type _} {Γ L r r'}
+  (toRight : ∀{Γ L r r'}, P Γ L r r' → r'.WfD Γ L) : Cong P Γ L r r' → r'.WfD Γ L
+  | step p => toRight p
+  | case_left de pr ds => case de (pr.right toRight) ds
+  | case_right de dr ps => case de dr (ps.right toRight)
+  | let1 de pr => WfD.let1 de (pr.right toRight)
+  | let2 de pr => WfD.let2 de (pr.right toRight)
+  | cfg_entry R hR pβ dG => WfD.cfg _ R hR (pβ.right toRight) dG
+  | cfg_block R hR dβ dG i pr => WfD.cfg _ R hR dβ (λk => by
+    if h : k = i then
+      cases h
+      simp only [Function.update_same]
+      exact (pr.right toRight)
+    else
+      simp only [ne_eq, h, not_false_eq_true, Function.update_noteq]
+      exact dG k
+  )
+
+-- TODO: therefore, a prefunctor to HaveTrg lifts via Cong...
+
 def Region.RewriteD.wfD {Γ : Ctx α ε} {r r' : Region φ} {L}
   : RewriteD r r' → r.WfD Γ L → r'.WfD Γ L
   | let1_op f e r, WfD.let1 (Term.WfD.op hf he) hr

lake-manifest.json

@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "a6fc8cb4fbcda16a2852dd157f9ae85e30d92945",
+   "rev": "8ca314116d1ae0e908c2a57d9840866059536360",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,7 +67,7 @@
   {"url": "https://github.com/imbrem/discretion.git",
    "type": "git",
    "subDir": null,
-   "rev": "a3b862ae6894acfcddbd3326e22822ae53aff36e",
+   "rev": "e0a105f67c5c7551fc17a87903a7ddba9d031233",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",