TreePatterns.lean

import Init.Data.ToString.Basic


namespace TreePatterns

variable {γ : Type} [BEq γ] [ToString γ]


abbrev Name := String

inductive TPat (γ : Type) where
  | TVar (var : Name) (children : List (TPat γ)) : TPat γ
  | Node (val : γ) (children : List (TPat γ)) : TPat γ
  deriving Repr, BEq

def TPat.children : TPat γ → List (TPat γ)
  | .TVar _ children => children
  | .Node _ children => children

def TPat.stringHelper [ToString γ] : TPat γ → String
  | .TVar v [] => s!"{v}"
  | .TVar v children => s!"{v}⟨{String.intercalate "," (children.map TPat.stringHelper)}⟩"
  | .Node j [] => s!"{j}"
  | .Node j children => s!"{j}⟨{String.intercalate "," (children.map TPat.stringHelper)}⟩"
instance : ToString (TPat γ) := ⟨TPat.stringHelper⟩


inductive Derivation (γ : Type) where
  | Rule (π₁ π₂ : TPat γ) (rule : Name) (children : List (Derivation γ)) : Derivation γ
  deriving Repr, BEq

def Derivation.stringHelper [ToString γ] : Derivation γ → String
  | .Rule π₁ π₂ rule children => let childStrs := children.map Derivation.stringHelper ; s!"{rule}: {toString π₁} ⊢ {toString π₂} with [{String.intercalate ", " childStrs}]"
instance : ToString (Derivation γ) := ⟨Derivation.stringHelper⟩


structure IndexProjection (n m : Nat) where
  mk ::
    indices : List Nat
    valid : indices.length == n ∧ indices.all (· < m)
  deriving Repr, BEq

instance : ToString (IndexProjection n m) where
  toString ip := "{" ++ String.intercalate "," (List.mapIdx (fun i idx => toString i ++ " ↦ " ++ toString idx) ip.indices) ++ "}"

def indexProjections (n m : Nat) : List (IndexProjection n m) :=
  (increasingLists n m).filterMap fun xs =>
    if h : xs.length == n ∧ xs.all (· < m) then some { indices := xs, valid := h } else none
  where /--
        `increasingLists n m` returns all strictly increasing lists of length `n`
        whose entries are drawn from `0, ..., m - 1`.
        -/
        increasingLists : Nat → Nat → List (List Nat)
        | 0, _ => [[]]
        | _ + 1, 0 => []
        | n + 1, m + 1 =>
            -- Lists that do not use `m`
            increasingLists (n + 1) m
            ++
            -- Lists that do use `m`, appended at the end
            (increasingLists n m).map (fun xs => xs ++ [m])

#eval (indexProjections 2 4)

-- generate index projections
-- iterate over them using for loop in Option monad


/--
`firstSome? xs f` tries `f x` for each `x : α` in `xs`,
  returning the first `some` result if it exists.
-/
def firstSome? : List α → (α → Option β) → Option β
  | [], _ => none
  | x :: xs, f =>
      match f x with
      | some y => some y
      | none   => firstSome? xs f

/--
Try every `x : α` until `f x` returns `some`.

This is the key helper: a `for` loop inside `Option` does *not*
backtrack, so we run the loop in `Id` and store the first successful result.
-/
def firstSomeFor? (xs : List α) (f : α → Option β) : Option β := Id.run do
  let mut result : Option β := none
  for x in xs do
    match result with
    | some _ => pure () -- already found one
    | none =>
      match f x with
      | some y => do result := some y
      | none => pure ()

  return result

def childrenOf : TPat γ → List (TPat γ)
  | .TVar _ children => children
  | .Node _ children => children



namespace SecondAttempt




#eval s!"{(TPat.Node "a" [.Node "g" [],.Node "h" [.Node "b" [], .Node "c" []]])} ◀ {(TPat.TVar "t" [.Node "c" []])}⟩"






end SecondAttempt


namespace Working

-- def proveChildrenCont
--   (π₁s π₂s : List (TPat γ))
--   (μ : IndexProjection π₂s.length π₁s.length)
--   (prove : TPat γ → TPat γ → Option (Derivation γ))
--   : Option (List (Derivation γ)) := Id.run do
--     μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
--     let π₁ᵢ ← π₁s[idx]?
--     prove π₁ᵢ π₂ᵢ

def proveChildrenContFor
  (π₁s π₂s : List (TPat γ))
  (μ : IndexProjection π₂s.length π₁s.length)
  (proveF : TPat γ → TPat γ → Option (Derivation γ))
  : Option (List (Derivation γ)) := Id.run do
    let mut derivations : List (Derivation γ) := []
    for (π₂ᵢ,idx) in π₂s.zip μ.indices do     -- for (idx, π₂ᵢ) in μ.indices.zip π₂s do
    -- for (idx, π₂ᵢ) in μ.indices.zip π₂s do
      let π₁ᵢ ← π₁s[idx]?
      match π₁ᵢ with
        | none => do

          pure ()
        | some π₁ᵢ => do
          match proveF π₁ᵢ π₂ᵢ with
          | none => pure ()
          | some d => derivations := derivations ++ [d]

    -- try1
    -- some derivations

    -- try2
    if derivations.length == μ.indices.length && derivations.length == π₂s.length then
      some derivations
    else
      none

    -- reference
    -- μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
    -- let π₁ᵢ ← π₁s[idx]?
    -- prove π₁ᵢ π₂ᵢ




partial def prove' (π₁ π₂ : TPat γ) : Option (Derivation γ) := do

  let intro :=
    -- ◀-Intro
    if π₁ == π₂ then
      some <| Derivation.Rule π₁ π₂ "◀-Intro" []
    else
      none

  let dispatchNotYet := do
    -- ◀-Dispatch_R/∃ / ◀-NotYet
    -- firstSome? π₁.children (prove' · π₂)
    firstSome? π₁.children <| fun πᵢ => do
      let notYetDeriv ← prove' πᵢ π₂
      pure <| Derivation.Rule πᵢ π₂ "◀-D_R/∃//◀-NotYet" [notYetDeriv]


  let dispatchChildren := do
    match π₁, π₂ with
    -- ◀-DispatchChildren_3/Alternative, Disjunction LHS (ρ₁ = ρ₂ ∈ Judge)
    | .Node j₁ children₁, .Node j₂ children₂ => do
      if j₁ == j₂ then do
        firstSomeFor? (indexProjections children₂.length children₁.length) <| fun μ => do
          let childDerivs ← proveChildrenContFor children₁ children₂ μ prove'
          pure <| Derivation.Rule π₁ π₂ s!"◀-DC/3altLHS " /- {j₁} {j₂} {μ}" -/ childDerivs
      else do
        none

    -- ◀-DispatchChildren_3/Alternative, Disjunction RHS v1 (ρ₁ ∈ Judge, ρ₂ ∉ Judge)
    | .Node j₁ children₁, .TVar ρ₂ children₂ => do
      firstSomeFor? (indexProjections children₂.length children₁.length) <| fun μ => do
        let childDerivs ← proveChildrenContFor children₁ children₂ μ prove'
        pure <| Derivation.Rule π₁ π₂ s!"◀-DC/3altRHS1 {j₁} {ρ₂} {μ}" childDerivs

    -- ◀-DispatchChildren_3/Alternative, Disjunction RHS v2 (ρ₁ ∉ Judge, ρ₂ ∉ Judge)
    | .TVar ρ₁ children₁, .TVar ρ₂ children₂ => do
      firstSomeFor? (indexProjections children₂.length children₁.length) <|fun μ => do
        let childDerivs ← proveChildrenContFor children₁ children₂ μ prove'
        pure <| Derivation.Rule π₁ π₂ s!"◀-DC/3altRHS2" /- {ρ₁} {ρ₂} {μ}" -/ childDerivs

    | _, _ => none


  intro <|> dispatchNotYet <|> dispatchChildren <|> dispatchNotYet <|> none

def Derivation.show (p : Option (Derivation γ)) :=
  match p with
  | none => IO.println "No proof found."
  | some d => IO.println <| toString d

#eval Derivation.show <| prove' (.Node "a" [.Node "g" [],.Node "h" [.Node "b" [], .Node "c" []]]) (.TVar "τ" [.Node "c" []])
#eval Derivation.show <| prove' (.Node "a" [.Node "g" [],.Node "h" [.Node "b" [], .Node "c" []]]) (.TVar "τ" [.Node "b" [], .Node "c" []])
#eval Derivation.show <| prove' (.Node "a" [.Node "g" [],.Node "h" [.Node "b" [], .Node "c" []]]) (.TVar "τ" [])



namespace NotationTest


/-! ## Concrete syntax for tree patterns

The paper writes tree patterns as `ρ⟨π₁,…,πₙ⟩`, distinguishing a `Judge`
root (capital letters like `A`, `B`, `J`) from a `TreeVar` root (`τ`, `τ₁`, …)
purely by typographic convention. Lean identifiers don't preserve that
convention, so we use a `?` sigil:

* `A`           ↦ `TPat.Node "A" []`
* `?t`          ↦ `TPat.TVar "t" []`
* `A⟨π₁,…,πₙ⟩`  ↦ `TPat.Node "A" [π₁,…,πₙ]`
* `?t⟨π₁,…,πₙ⟩` ↦ `TPat.TVar "t" [π₁,…,πₙ]`

The entry point is `tp! π`. The category `tpat` is parsed in isolation, so
the angle brackets do not collide with Lean's anonymous-constructor `⟨…⟩`.

`?` is a fresh prefix token here; identifiers carrying subscripts or Greek
letters work transparently (`?τ₁`, `?ρ`, `?foo'`).
-/
namespace Notation

open Lean

declare_syntax_cat tpat

-- Leaves: bare `A` is a Judge; `?t` is a TreeVar.
syntax:max ident                       : tpat
syntax:max "?" ident                   : tpat

-- Internal nodes with children.
syntax:max ident "⟨" tpat,* "⟩"        : tpat
syntax:max "?" ident "⟨" tpat,* "⟩"    : tpat

-- Grouping.
syntax "(" tpat ")"                    : tpat

/-- `tp! π` elaborates a tree-pattern expression in `tpat` syntax to a
`TPat String` term. -/
syntax (name := tpatBang) "tp!" tpat : term

macro_rules
  | `(tp! ($p:tpat))               => `(tp! $p)
  | `(tp! $i:ident)                => `(TPat.Node $(quote i.getId.toString) [])
  | `(tp! ?$i:ident)               => `(TPat.TVar $(quote i.getId.toString) [])
  | `(tp! $i:ident ⟨ $args,* ⟩)    => do
        let argTerms ← args.getElems.mapM (fun a => `(tp! $a))
        `(TPat.Node $(quote i.getId.toString) [ $argTerms,* ])
  | `(tp! ?$i:ident ⟨ $args,* ⟩)   => do
        let argTerms ← args.getElems.mapM (fun a => `(tp! $a))
        `(TPat.TVar $(quote i.getId.toString) [ $argTerms,* ])

/-- `π₁ ◀ π₂` is sugar for `Working.prove' π₁ π₂`, returning the optional
derivation that witnesses `π₁ ◀ π₂` (a matching proof). -/
infix:50 " ◀ " => TreePatterns.Working.prove'

end Notation


/-! ## Demonstration -/

open Notation
open Working (Derivation.show)

-- The three examples from the original file, rewritten in concrete syntax.
-- (Each `tp! …` elaborates to the same constructor calls as before.)

#eval Derivation.show <| (tp! a⟨g, h⟨b, c⟩⟩) ◀ (tp! ?t⟨c⟩)
#eval Derivation.show <| (tp! a⟨g, h⟨b, c⟩⟩) ◀ (tp! ?t⟨b, c⟩)
#eval Derivation.show <| (tp! a⟨g, h⟨b, c⟩⟩) ◀ (tp! ?t)

-- Subscripts and Greek letters in variable names work:
#eval Derivation.show <| (tp! A⟨B, C⟩) ◀ (tp! ?τ₁⟨B⟩)

-- Sanity check that elaboration produces exactly the underlying ctor form.
example :
    (tp! a⟨g, h⟨b, c⟩⟩) =
      (.Node "a" [.Node "g" [], .Node "h" [.Node "b" [], .Node "c" []]] : TPat String) :=
  rfl

example :
    (tp! ?t⟨c⟩) = (.TVar "t" [.Node "c" []] : TPat String) :=
  rfl



end NotationTest



#eval Derivation.show <| (tp! a⟨g, h⟨b, c⟩⟩) ◀ (tp! ?t⟨c⟩)
#eval Derivation.show <| (tp! a⟨g, h⟨b, c⟩⟩) ◀ (tp! ?t⟨b, c⟩)
#eval Derivation.show <| (tp! a⟨g, h⟨b, c⟩⟩) ◀ (tp! ?t)

#eval Derivation.show <| (tp! τ₁⟨τ₂⟨⟩⟩ ) ◀ (tp! ?τ₃⟨⟩)



end Working



















-- namespace FirstAttempt
-- -- -- def proveChildrenContFor
-- -- --   (π₁s π₂s : List (TPat γ))
-- -- --   (μ : IndexProjection π₂s.length π₁s.length)
-- -- --   (prove : TPat γ → TPat γ → Option (Derivation γ))
-- -- --   : Option (∃ D : List (Derivation γ), D.length == μ.indices.length)

-- -- def proveChildrenCont
-- --   (π₁s π₂s : List (TPat γ))
-- --   (μ : IndexProjection π₂s.length π₁s.length)
-- --   (prove : TPat γ → TPat γ → Option (Derivation γ))
-- --   : Option (List (Derivation γ)) := Id.run do
-- --     μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
-- --     let π₁ᵢ ← π₁s[idx]?
-- --     prove π₁ᵢ π₂ᵢ

-- def proveChildrenContFor
--   (π₁s π₂s : List (TPat γ))
--   (μ : IndexProjection π₂s.length π₁s.length)
--   (proveF : TPat γ → TPat γ → Option (Derivation γ))
--   : Option (List (Derivation γ)) := Id.run do
--     let mut derivations : List (Derivation γ) := []
--     for (π₂ᵢ,idx) in π₂s.zip μ.indices do     -- for (idx, π₂ᵢ) in μ.indices.zip π₂s do
--       let π₁ᵢ ← π₁s[idx]?
--       match π₁ᵢ with
--         | none => pure ()
--         | some π₁ᵢ => do
--           match proveF π₁ᵢ π₂ᵢ with
--           | none => pure ()
--           | some d => derivations := derivations ++ [d]

--     -- try1
--     -- some derivations

--     -- try2
--     if -- derivations.length == μ.indices.length &&
--     derivations.length == π₂s.length then
--       some derivations
--     else
--       none

--     -- reference
--     -- μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
--     -- let π₁ᵢ ← π₁s[idx]?
--     -- prove π₁ᵢ π₂ᵢ

-- #check proveChildrenContFor
-- #eval toString <|
--   proveChildrenContFor
--     [.Node "a" [], .Node "b" []]
--     [.Node "x" [], .Node "y" []]
--     { indices := [1, 0],
--       valid := ⟨by decide, by decide⟩
--     }
--     (fun π₁ π₂ => if π₁ == π₂ then some (Derivation.Rule π₁ π₂ "reflexivity" []) else none)




-- partial def prove' (π₁ π₂ : TPat γ) : Option (Derivation γ) := do

--   let intro :=
--     -- ◀-Intro
--     if π₁ == π₂ then
--       some <| Derivation.Rule π₁ π₂ "Intro" []
--     else
--       none

--   let dispatchChildren := do
--     match π₁, π₂ with
--     -- ◀-DispatchChildren_3/Alternative, Disjunction LHS (ρ₁ = ρ₂ ∈ Judge)
--     | .Node j₁ children₁, .Node j₂ children₂ => do
--       if j₁ == j₂ then do
--         firstSomeFor? (indexProjections children₂.length children₁.length) <| fun μ => do
--           let childDerivs ← proveChildrenContFor children₁ children₂ μ prove'
--           pure <| Derivation.Rule π₁ π₂ s!"DispatchChildren/node {μ}" childDerivs
--       else do
--         none

--     -- ◀-DispatchChildren_3/Alternative, Disjunction RHS v1 (ρ₁ ∈ Judge, ρ₂ ∉ Judge)
--     | .Node j₁ children₁, .TVar ρ₂ children₂ => do
--       firstSomeFor? (indexProjections children₂.length children₁.length) <| fun μ => do
--         let childDerivs ← proveChildrenContFor children₁ children₂ μ prove'
--         pure <| Derivation.Rule π₁ π₂ s!"DispatchChildren/3altRHS1 {ρ₂} {μ}" childDerivs

--     -- ◀-DispatchChildren_3/Alternative, Disjunction RHS v2 (ρ₁ ∉ Judge, ρ₂ ∉ Judge)
--     | .TVar ρ₁ children₁, .TVar ρ₂ children₂ => do
--       firstSomeFor? (indexProjections children₂.length children₁.length) <|fun μ => do
--         let childDerivs ← proveChildrenContFor children₁ children₂ μ prove'
--         pure <| Derivation.Rule π₁ π₂ s!"DispatchChildren/3altRHS2 {ρ₂} {μ}" childDerivs

--     | .TVar _ _, .Node _ _ => none

--   let dispatchNotYet := do
--     -- ◀-Dispatch_R/∃ / ◀-NotYet
--     firstSome? π₁.children (prove' · π₂)

--   intro <|> dispatchChildren <|> dispatchNotYet <|> none
-- #check firstSome?



-- /--
-- `firstSome? xs f` tries `f x` for each `x : α` in `xs`,
--   returning the first `some` result if it exists.
-- -/
-- def firstSome? : List α → (α → Option β) → Option β
--   | [], _ => none
--   | x :: xs, f =>
--       match f x with
--       | some y => some y
--       | none   => firstSome? xs f


--   -- | _, _ =>
--   --   if π₁ == π₂ then
--   --     pure <| Derivation.Rule π₁ π₂ "Intro" []
--   --   else
--   --     none

-- #eval toString <| prove' (.Node "a" [.Node "g" [],.Node "h" [.Node "b" [], .Node "c" []]]) (.TVar "t" [.Node "c" []])



-- /-
-- def prove' (π₁ π₂ : TPat γ) : Option (Derivation γ) := do
--   match π₁, π₂ with
--   | .Node j₁ children₁, .Node j₂ children₂ =>
--           if j₁ == j₂ then
--             firstSomeFor? (indexProjections children₂.length children₁.length) fun μ => do
--               let childDerivs ← proveChildrenContFor children₁ children₂ μ prove'
--               pure <| Derivation.Rule π₁ π₂ s!"DispatchChildren/node {μ}" childDerivs

--           else
--             none
--   | _, .TVar ρ₂ children₂ =>
--           firstSomeFor? (indexProjections children₂.length (childrenOf π₁).length) fun μ => do
--             let childDerivs ← proveChildrenContFor (childrenOf π₁) children₂ μ prove'
--             pure <|
--               Derivation.Rule π₁ π₂ s!"DispatchChildren/treevar {ρ₂} {μ}" childDerivs

--   | π₁, π₂ =>
--     if π₁ == π₂ then
--       pure <| Derivation.Rule π₁ π₂ "Intro" []
--     else
--       none
-- -/


-- def prove (π₁ π₂ : TPat γ) : Option (Derivation γ) :=
--   if π₁ == π₂ then
--     pure <| Derivation.Rule π₁ π₂ "Intro" []
--   else
--     match π₁, π₂ with
--     | .Node j₁ children₁, .Node j₂ children₂ =>
--         if j₁ == j₂ then
--           firstSomeFor? (indexProjections children₂.length children₁.length) fun μ => do
--             let childDerivs ← proveChildrenContFor children₁ children₂ μ prove
--             pure <| Derivation.Rule π₁ π₂ s!"DispatchChildren/node {μ}" childDerivs

--             -- (not working)
--             -- let childDerivs ← proveChildren children₁ children₂ μ
--             -- pure <|
--             --   Derivation.Rule π₁ π₂ s!"DispatchChildren/node {μ}" childDerivs

--             -- (promising)
--             -- let childDerivs ← do μ.indices.zip children₂ |>.mapM fun (idx, c₂ᵢ) => do
--             --   let c₁ᵢ ← children₁[idx]?
--             --   prove c₁ᵢ c₂ᵢ

--         else
--           none

--     | _, .TVar ρ₂ children₂ =>
--         firstSomeFor? (indexProjections children₂.length (childrenOf π₁).length) fun μ => do
--           let childDerivs ← proveChildrenContFor (childrenOf π₁) children₂ μ prove
--           pure <|
--             Derivation.Rule π₁ π₂ s!"DispatchChildren/treevar {ρ₂} {μ}" childDerivs


--           -- (not working)
--           -- let childDerivs ← proveChildren (childrenOf π₁) children₂ μ
--           -- pure <|
--           --   Derivation.Rule π₁ π₂ s!"DispatchChildren/treevar {ρ₂} {μ}" childDerivs
--           -- sorry
--     | _, _ =>
--         none



-- -- def proveChildrenCont
-- --   (π₁s π₂s : List (TPat γ))
-- --   (μ : IndexProjection π₂s.length π₁s.length)
-- --   (prove : TPat γ → TPat γ → Option (Derivation γ))
-- --   : Option (List (Derivation γ)) := Id.run do
-- --     μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
-- --     let π₁ᵢ ← π₁s[idx]?
-- --     prove π₁ᵢ π₂ᵢ


-- mutual

--   def proveChildren'
--       (π₁s π₂s : List (TPat γ))
--       (μ : IndexProjection π₂s.length π₁s.length)
--       : Option (List (Derivation γ)) := Id.run do
--         μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
--         let π₁ᵢ ← π₁s[idx]?
--         prove π₁ᵢ π₂ᵢ


--   def proveChildren''
--       (children₁ children₂ : List (TPat γ))
--       (μ : IndexProjection children₂.length children₁.length) :
--       Option (List (Derivation γ)) := do
--     μ.indices.zip children₂ |>.mapM fun (idx, π₂ᵢ) => do
--       let π₁ᵢ ← children₁[idx]?
--       prove π₁ᵢ π₂ᵢ


--   def prove (π₁ π₂ : TPat γ) : Option (Derivation γ) := do
--     if π₁ == π₂ then
--       pure <| Derivation.Rule π₁ π₂ "Intro" []
--     else
--       match π₁, π₂ with
--       | .Node j₁ children₁, .Node j₂ children₂ =>
--           if j₁ == j₂ then
--             firstSomeFor?
--               (indexProjections children₂.length children₁.length)
--               fun μ => do
--                 let childDerivs ← proveChildren children₁ children₂ μ prove
--                 pure <|
--                   Derivation.Rule
--                     π₁
--                     π₂
--                     s!"DispatchChildren/node {μ}"
--                     childDerivs
--           else
--             none

--       | _, .TVar ρ₂ children₂ =>
--           firstSomeFor?
--             (indexProjections children₂.length (childrenOf π₁).length)
--             fun μ => do
--               let childDerivs ← proveChildren (childrenOf π₁) children₂ μ prove
--               pure <|
--                 Derivation.Rule
--                   π₁
--                   π₂
--                   s!"DispatchChildren/treevar {ρ₂} {μ}"
--                   childDerivs

--       | _, _ =>
--           none
--       where
--         proveChildren
--           (π₁s π₂s : List (TPat γ))
--           (μ : IndexProjection π₂s.length π₁s.length)
--           : Option (List (Derivation γ)) := Id.run do
--             μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
--             let π₁ᵢ ← π₁s[idx]?
--             prove π₁ᵢ π₂ᵢ






-- end






-- ------------------
-- namespace Tmp
-- def proveChildren
--     (π₁s π₂s : List (TPat γ))
--     (μ : IndexProjection π₂s.length π₁s.length)
--     : Option (List (Derivation γ)) := Id.run do
--       μ.indices.zip π₂s |>.mapM fun (idx, π₂ᵢ) => do
--       let π₁ᵢ ← π₁s[idx]?
--       prove π₁ᵢ π₂ᵢ


-- def prove (π₁ π₂ : TPat γ) : Option (Derivation γ) := do
--   if π₁ == π₂ then
--     pure <| Derivation.Rule π₁ π₂ "reflexivity" []
--   else do
--     match π₁, π₂ with
--     -- DispatchChildren_3/Alternative, Disjunction LHS
--     | .Node j₁ children₁, .Node j₂ children₂ =>
--       if j₁ == j₂ then
--         firstSomeFor? (indexProjections children₂.length children₁.length) fun μ => do

--           let childDerivs ← proveChildren children₁ children₂ μ
--           pure <| Derivation.Rule π₁ π₂ s!"node {μ}" childDerivs
--         -- firstSome? (indexProjections children₂.length children₁.length) fun μ => do
--         --   let childDerivs ← proveChildren children₁ children₂ μ
--         --   pure <| Derivation.Rule π₁ π₂ s!"node {μ}" childDerivs
--         -- for μ in indexProjections n m do
--         --   let childDerivs ← List.zipWithM prove children₁ children₂
--         --   pure <| Derivation.Rule π₁ π₂ "node" childDerivs
--       else
--         none

--     -- DispatchChildren_3/Alternative, Disjunction RHS
--     | _, .TVar ρ₂ children₂ =>
--       sorry
--     | _, _ => sorry

-- end Tmp



-- -- mutual

-- -- def proveChildren
-- --     (children₁ children₂ : List (TPat γ))
-- --     (μ : IndexProjection children₂.length children₁.length)
-- --     : Option (List (Derivation γ)) := do
-- --   μ.indices.zip children₂ |>.mapM fun (idx, π₂ᵢ) => do
-- --     let π₁ᵢ ← children₁.get? idx
-- --     prove π₁ᵢ π₂ᵢ

-- -- def prove (π₁ π₂ : TPat γ) : Option (Derivation γ) := do
-- --   if π₁ == π₂ then
-- --     pure <| Derivation.Rule π₁ π₂ "reflexivity" []
-- --   else do
-- --     match π₁, π₂ with
-- --     -- DispatchChildren_3/Alternative, Disjunction LHS
-- --     | .Node j₁ children₁, .Node j₂ children₂ =>
-- --       if j₁ == j₂ then
-- --         firstSome? (indexProjections children₂.length children₁.length) fun μ => do
-- --           let childDerivs ← proveChildren children₁ children₂ μ
-- --           pure <| Derivation.Rule π₁ π₂ s!"node {μ}" childDerivs
-- --         -- for μ in indexProjections n m do
-- --         --   let childDerivs ← List.zipWithM prove children₁ children₂
-- --         --   pure <| Derivation.Rule π₁ π₂ "node" childDerivs
-- --       else
-- --         none

-- --     -- DispatchChildren_3/Alternative, Disjunction RHS
-- --     | _, .TVar ρ₂ children₂ =>
-- --       sorry
-- --     | _, _ => sorry

-- -- end


-- -- /--
-- -- def prove (π₁ π₂ : TPat γ) : Option (Derivation γ) := do
-- --   if π₁ == π₂ then
-- --     pure <| Derivation.Rule π₁ π₂ "reflexivity" []
-- --   else do
-- --     match π₁, π₂ with
-- --     -- DispatchChildren_3/Alternative, Disjunction LHS
-- --     | .Node j₁ children₁, .Node j₂ children₂ =>
-- --       if j₁ == j₂ then
-- --         for μ in indexProjections n m do
-- --           let childDerivs ← List.zipWithM prove children₁ children₂
-- --           pure <| Derivation.Rule π₁ π₂ "node" childDerivs
-- --       else
-- --         none

-- --     -- DispatchChildren_3/Alternative, Disjunction RHS
-- --     | _, .TVar ρ₂ children₂ =>
-- --       if
-- --     | _, _ => none
-- -- --/
-- end FirstAttempt


end TreePatterns