LMR.lean

/-
Loff-Moreira-Reis scaffolding automata.

Definitions 10-15 of "The computational power of Parsing Expression Grammars",
arXiv:1902.08272v2, transcribed at the operational level used by the transfer.
In particular:

* nodes are `0, 1, ..., top`, and node `0` is the unlabelled base;
* the degree `d` and distance `k` are free parameters of the automaton;
* `N_k` is a *partial d-ary labelled tree* -- the unfolding, carrying no node
  identity, so no transition can test whether two port words alias;
* exactly one node is appended per input symbol;
* a new edge is named by a port word of length at most `k` from the old top,
  or by `SELF`, or is missing;
* acceptance is membership of the final control state in `F`.

The carriers are polymorphic Lean types. Finiteness of the input alphabet,
control, and scaffold alphabet is imposed when applying the published finite
automaton theorem, rather than by `Fintype` fields on these operational
definitions. Auxiliary predicates such as `Backward`, `DistanceOk`, and
`SelfFree` state properties consumed by the transfer proof; they do not
strengthen the ambient automaton datatype.
-/

namespace FPRD

universe u

/-- Definition 12's edge-naming syntax: `[d)^{<=k} u {SELF, \emptyset}`.  The
length restriction is imposed separately, by `Automaton.DistanceOk`, so that
this datatype stays free of proof carrying. -/
inductive Target (d : Nat) where
  | path : List (Fin d) → Target d
  | self : Target d
  | missing : Target d

/-- Definition 10's operational carrier for a `(d, Γ)`-scaffold.

The ambient function representation can contain data above `top`. `base`
starts without such data, `append` preserves its absence on generated runs,
and the transfer's `Sim.aboveLabel` and `Sim.aboveEdge` fields record that
reachable invariant explicitly. -/
structure Scaffold (d : Nat) (Gamma : Type u) where
  top : Nat
  label : Nat → Option Gamma
  edge : Nat → Fin d → Option Nat

namespace Scaffold

variable {d : Nat} {Gamma : Type u}

/-- Definition 10's "edges point backwards", as a predicate.  A scaffold built
without `SELF` satisfies the strict form recorded here. -/
def Backward (S : Scaffold d Gamma) : Prop :=
  ∀ v i m, S.edge v i = some m → m < v

/-- Definition 10's path following.  `follow v p` is `v_k`, or `none` if `p` is
an invalid path from `v`. -/
def follow (S : Scaffold d Gamma) : Nat → List (Fin d) → Option Nat
  | v, [] => some v
  | v, i :: p =>
    match S.edge v i with
    | none => none
    | some u => S.follow u p

theorem follow_nil (S : Scaffold d Gamma) (v : Nat) : S.follow v [] = some v := rfl

theorem follow_cons (S : Scaffold d Gamma) (v : Nat) (i : Fin d) (p : List (Fin d)) :
    S.follow v (i :: p) =
      match S.edge v i with
      | none => none
      | some u => S.follow u p := rfl

theorem follow_cons_none (S : Scaffold d Gamma) (v : Nat) (i : Fin d)
    (p : List (Fin d)) (h : S.edge v i = none) : S.follow v (i :: p) = none := by
  rw [follow_cons, h]

theorem follow_cons_some (S : Scaffold d Gamma) (v : Nat) (i : Fin d)
    (p : List (Fin d)) (u : Nat) (h : S.edge v i = some u) :
    S.follow v (i :: p) = S.follow u p := by
  rw [follow_cons, h]

theorem follow_single (S : Scaffold d Gamma) (v : Nat) (i : Fin d) :
    S.follow v [i] = S.edge v i := by
  cases he : S.edge v i with
  | none => rw [S.follow_cons_none v i [] he]
  | some u => rw [S.follow_cons_some v i [] u he, S.follow_nil u]

/-- Under `Backward`, following a path never moves forward. -/
theorem follow_le (S : Scaffold d Gamma) (hb : S.Backward) :
    ∀ (p : List (Fin d)) (v u : Nat), S.follow v p = some u → u ≤ v := by
  intro p
  induction p with
  | nil =>
    intro v u h
    simp [follow_nil] at h
    omega
  | cons i p ih =>
    intro v u h
    rw [follow_cons] at h
    cases hv : S.edge v i with
    | none => rw [hv] at h; simp at h
    | some w =>
      rw [hv] at h
      have hw : w < v := hb v i w hv
      have := ih w u h
      omega

/-- The empty scaffold `S_0` of Definition 12: one unlabelled base node. -/
def base (d : Nat) (Gamma : Type u) : Scaffold d Gamma where
  top := 0
  label := fun _ => none
  edge := fun _ _ => none

theorem base_backward (d : Nat) (Gamma : Type u) : (base d Gamma).Backward := by
  intro v i m h
  simp [base] at h

/-- Definition 13's target resolution: a port word is followed from the old
top `t`, `SELF` names the node being created, and `missing` stays missing. -/
def resolve (S : Scaffold d Gamma) (t new : Nat) : Target d → Option Nat
  | .path p => S.follow t p
  | .self => some new
  | .missing => none

/-- Definition 13's `Step` on the scaffold: append one node, labelled `g`,
whose edges are named by `tgt`. -/
def append (S : Scaffold d Gamma) (g : Gamma) (tgt : Fin d → Target d) :
    Scaffold d Gamma where
  top := S.top + 1
  label := fun v => if v = S.top + 1 then some g else S.label v
  edge := fun v i =>
    if v = S.top + 1 then S.resolve S.top (S.top + 1) (tgt i) else S.edge v i

@[simp] theorem append_top (S : Scaffold d Gamma) (g : Gamma) (tgt : Fin d → Target d) :
    (S.append g tgt).top = S.top + 1 := rfl

@[simp] theorem append_label_new (S : Scaffold d Gamma) (g : Gamma)
    (tgt : Fin d → Target d) : (S.append g tgt).label (S.top + 1) = some g := by
  simp [append]

theorem append_label_old (S : Scaffold d Gamma) (g : Gamma) (tgt : Fin d → Target d)
    {v : Nat} (h : v ≠ S.top + 1) : (S.append g tgt).label v = S.label v := by
  simp [append, h]

@[simp] theorem append_edge_new (S : Scaffold d Gamma) (g : Gamma)
    (tgt : Fin d → Target d) (i : Fin d) :
    (S.append g tgt).edge (S.top + 1) i = S.resolve S.top (S.top + 1) (tgt i) := by
  simp [append]

theorem append_edge_old (S : Scaffold d Gamma) (g : Gamma) (tgt : Fin d → Target d)
    {v : Nat} (h : v ≠ S.top + 1) (i : Fin d) :
    (S.append g tgt).edge v i = S.edge v i := by
  simp [append, h]

/-- `append` preserves strict backwardness provided no target is `SELF`. -/
theorem append_backward (S : Scaffold d Gamma) (hb : S.Backward) (g : Gamma)
    (tgt : Fin d → Target d) (hself : ∀ i, tgt i ≠ .self) :
    (S.append g tgt).Backward := by
  intro v i m h
  by_cases hv : v = S.top + 1
  · subst hv
    rw [append_edge_new] at h
    cases htg : tgt i with
    | path p =>
      rw [htg] at h
      simp [resolve] at h
      have := follow_le S hb p S.top m h
      omega
    | self => exact absurd htg (hself i)
    | missing => rw [htg] at h; simp [resolve] at h
  · rw [append_edge_old S g tgt hv i] at h
    exact hb v i m h

end Scaffold

/-- Definition 11's `N_k(d, Γ)`: the partial `d`-ary `Γ`-labelled trees.

`missing` is the paper's `N_k(S, \emptyset) = \emptyset`; it is a separate
constructor rather than an `Option` wrapper because Lean forbids nesting an
inductive under a parameterised type whose parameter mentions the inductive.
The three cases at depth zero -- `missing`, `leaf none`, `leaf (some g)` --
keep "absent", "present but unlabelled", and "present and labelled" distinct,
exactly as the paper's `Γ ∪ {∅}` with a separate `∅` for a missing child. -/
inductive Unfold (d : Nat) (Gamma : Type u) : Nat → Type u where
  | missing : {k : Nat} → Unfold d Gamma k
  | leaf : Option Gamma → Unfold d Gamma 0
  | node : {k : Nat} → Option Gamma → (Fin d → Unfold d Gamma k) →
      Unfold d Gamma (k + 1)

namespace Unfold

variable {d : Nat} {Gamma : Type u} {k : Nat}

/-- Whether the root of an unfolding is a present node at all. -/
def present : Unfold d Gamma k → Bool
  | .missing => false
  | .leaf _ => true
  | .node _ _ => true

/-- The label at the root, `none` when the node is missing *or* unlabelled.

A transition is free to use `present` as well; the compiler in `Compile`
deliberately uses only `labelOf`, which is strictly less information. -/
def labelOf : Unfold d Gamma k → Option Gamma
  | .missing => none
  | .leaf l => l
  | .node l _ => l

/-- The child unfolding along one port; `missing` propagates. -/
def child : Unfold d Gamma (k + 1) → Fin d → Unfold d Gamma k
  | .missing, _ => .missing
  | .node _ ch, i => ch i

end Unfold

namespace Scaffold

variable {d : Nat} {Gamma : Type u}

/-- Definition 11's `N_k(S, v)` for a present node. -/
def viewAt (S : Scaffold d Gamma) : (k : Nat) → Nat → Unfold d Gamma k
  | 0, v => .leaf (S.label v)
  | k + 1, v =>
    .node (S.label v) fun i =>
      match S.edge v i with
      | none => .missing
      | some u => S.viewAt k u

@[simp] theorem viewAt_labelOf (S : Scaffold d Gamma) (k v : Nat) :
    (S.viewAt k v).labelOf = S.label v := by
  cases k <;> rfl

@[simp] theorem viewAt_child (S : Scaffold d Gamma) (k v : Nat) (i : Fin d) :
    (S.viewAt (k + 1) v).child i =
      match S.edge v i with
      | none => .missing
      | some u => S.viewAt k u := rfl

end Scaffold

/-- Definition 12's operational automaton. `Sym` is the input alphabet and `Q`
the control carrier; their finiteness is an external specialization. -/
structure Automaton (Sym : Type) (Q : Type) (Gamma : Type u) (d k : Nat) where
  delta : Q → Sym → Unfold d Gamma k → Q × Gamma × (Fin d → Target d)
  init : Q
  accept : Q → Bool

namespace Automaton

variable {Sym Q : Type} {Gamma : Type u} {d k : Nat}

/-- Definition 12's typing constraint on port words, stated separately. -/
def DistanceOk (A : Automaton Sym Q Gamma d k) : Prop :=
  ∀ q x n j p, (A.delta q x n).2.2 j = .path p → p.length ≤ k

/-- Definition 12's requirement that no target is `SELF` is *not* part of the
model; this predicate records automata that happen not to use it. -/
def SelfFree (A : Automaton Sym Q Gamma d k) : Prop :=
  ∀ q x n j, (A.delta q x n).2.2 j ≠ .self

/-- Definition 13's single step of computation. -/
def step (A : Automaton Sym Q Gamma d k) (c : Q × Scaffold d Gamma) (x : Sym) :
    Q × Scaffold d Gamma :=
  let r := A.delta c.1 x (c.2.viewAt k c.2.top)
  (r.1, c.2.append r.2.1 r.2.2)

/-- Definition 14's computation on a word. -/
def run (A : Automaton Sym Q Gamma d k) (w : List Sym) : Q × Scaffold d Gamma :=
  w.foldl A.step (A.init, Scaffold.base d Gamma)

/-- Definition 15.  `A(x)` is accepting iff `q_n ∈ F`. -/
def decides (A : Automaton Sym Q Gamma d k) (w : List Sym) : Bool :=
  A.accept (A.run w).1

@[simp] theorem run_nil (A : Automaton Sym Q Gamma d k) :
    A.run [] = (A.init, Scaffold.base d Gamma) := rfl

theorem run_append (A : Automaton Sym Q Gamma d k) (w : List Sym) (x : Sym) :
    A.run (w ++ [x]) = A.step (A.run w) x := by
  simp [run, List.foldl_append]

/-- Every input symbol appends exactly one scaffold node. Since the base node
has index zero, the final top index is the input length. -/
theorem run_top (A : Automaton Sym Q Gamma d k) (w : List Sym) :
    (A.run w).2.top = w.length := by
  have fold_top :
      ∀ (u : List Sym) (c : Q × Scaffold d Gamma),
        (u.foldl A.step c).2.top = c.2.top + u.length := by
    intro u
    induction u with
    | nil =>
      intro c
      rfl
    | cons x xs ih =>
      intro c
      simp only [List.foldl_cons, List.length_cons]
      rw [ih (A.step c x)]
      simp only [step, Scaffold.append]
      omega
  simpa [run, Scaffold.base] using
    fold_top w (A.init, Scaffold.base d Gamma)

end Automaton

end FPRD