TableEval.lean

import FPRDTransfer.PEG.Semantics

namespace FPRD

universe uSym

namespace Expr

/-- A syntax-directed sufficient test: every successful evaluation consumes at
least one symbol.  Nonterminals are deliberately treated conservatively. -/
def guaranteedConsumes : Expr NT Sym → Bool
  | .eps | .fail | .nonterm _ | .notP _ => false
  | .any | .term _ => true
  | .seq left right => guaranteedConsumes left || guaranteedConsumes right
  | .alt left right => guaranteedConsumes left && guaranteedConsumes right

/-- Nonterminal calls which can be reached before this expression has
necessarily consumed input. -/
def samePositionCalls : Expr NT Sym → List NT
  | .eps | .fail | .any | .term _ => []
  | .nonterm name => [name]
  | .seq left right =>
      samePositionCalls left ++
        if guaranteedConsumes left then [] else samePositionCalls right
  | .alt left right => samePositionCalls left ++ samePositionCalls right
  | .notP body => samePositionCalls body

end Expr

/-- Successful PEG evaluation leaves a suffix of its input. -/
theorem eval_remainder_suffix_of_eq {G : Grammar NT Sym}
    {expr : Expr NT Sym} {input : List Sym} {result : Result Sym}
    (h : Eval G expr input result) :
    ∀ {rest}, result = .ok rest → rest <:+ input := by
  induction h with
  | eps => intro rest hr; cases hr; simp
  | fail => intro rest hr; cases hr
  | anyOk => intro rest hr; cases hr; simp
  | anyNil => intro rest hr; cases hr
  | termOk => intro rest hr; cases hr; simp
  | termNe => intro rest hr; cases hr
  | termNil => intro rest hr; cases hr
  | nonterm _ ih => exact ih
  | seqOk _ _ ihLeft ihRight =>
      intro rest hr
      exact (ihRight hr).trans (ihLeft rfl)
  | seqErr => intro rest hr; cases hr
  | altOk _ ih => exact ih
  | altErr _ _ _ ihRight => exact ihRight
  | notOk => intro rest hr; cases hr
  | notErr => intro rest hr; cases hr; simp

theorem eval_remainder_suffix {G : Grammar NT Sym} {expr : Expr NT Sym}
    {input rest : List Sym} (h : Eval G expr input (.ok rest)) :
    rest <:+ input := eval_remainder_suffix_of_eq h rfl

/-- The syntactic consumption test is sound for every successful relational
evaluation. -/
theorem guaranteedConsumes_sound_of_eq {G : Grammar NT Sym}
    {expr : Expr NT Sym} {input : List Sym} {result : Result Sym}
    (h : Eval G expr input result) : ∀ {rest}, result = .ok rest →
    Expr.guaranteedConsumes expr = true → rest.length < input.length := by
  induction h with
  | eps => simp [Expr.guaranteedConsumes]
  | fail => intro rest hr; cases hr
  | anyOk => intro rest hr; cases hr; simp
  | anyNil => intro rest hr; cases hr
  | termOk => intro rest hr; cases hr; simp
  | termNe => intro rest hr; cases hr
  | termNil => intro rest hr; cases hr
  | nonterm => simp [Expr.guaranteedConsumes]
  | seqOk hLeft hRight ihLeft ihRight =>
      intro rest hr hconsumes
      simp only [Expr.guaranteedConsumes, Bool.or_eq_true] at hconsumes
      rcases hconsumes with hleft | hright
      · exact Nat.lt_of_le_of_lt
          (eval_remainder_suffix_of_eq hRight hr).length_le
          (ihLeft rfl hleft)
      · exact Nat.lt_of_lt_of_le (ihRight hr hright)
          (eval_remainder_suffix hLeft).length_le
  | seqErr => intro rest hr; cases hr
  | altOk hLeft ih =>
      intro rest hr hconsumes
      simp only [Expr.guaranteedConsumes, Bool.and_eq_true] at hconsumes
      exact ih hr hconsumes.1
  | altErr _ hRight _ ihRight =>
      intro rest hr hconsumes
      simp only [Expr.guaranteedConsumes, Bool.and_eq_true] at hconsumes
      exact ihRight hr hconsumes.2
  | notOk => intro rest hr; cases hr
  | notErr => simp [Expr.guaranteedConsumes]

theorem guaranteedConsumes_sound {G : Grammar NT Sym}
    {expr : Expr NT Sym} {input rest : List Sym}
    (h : Eval G expr input (.ok rest))
    (hconsumes : Expr.guaranteedConsumes expr = true) :
    rest.length < input.length :=
  guaranteedConsumes_sound_of_eq h rfl hconsumes

/-- An explicit nonterminal order whose prefix contains every call that may be
reached at the same input position. -/
structure RankSchedule {n : Nat} (G : Grammar (Fin n) Sym) where
  order : List (Fin n)
  nodup : order.Nodup
  complete : ∀ name, name ∈ order
  earlier : ∀ {before after caller callee},
    order = before ++ caller :: after →
    callee ∈ Expr.samePositionCalls (G.rule caller) →
    callee ∈ before

namespace TableEval

abbrev Key (n : Nat) (Sym : Type uSym) := List Sym × Fin n
abbrev Table (n : Nat) (Sym : Type uSym) := List (Key n Sym × Result Sym)

def lookup [DecidableEq Sym] (table : Table n Sym)
    (input : List Sym) (name : Fin n) : Option (Result Sym) :=
  match table with
  | [] => none
  | (key, result) :: rest =>
      if key = (input, name) then some result else lookup rest input name

def insert (table : Table n Sym) (input : List Sym) (name : Fin n)
    (result : Result Sym) : Table n Sym :=
  ((input, name), result) :: table

def Sound [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (table : Table n Sym) : Prop :=
  ∀ input name result, lookup table input name = some result →
    Eval G (.nonterm name) input result

def Filled [DecidableEq Sym] (table : Table n Sym)
    (input : List Sym) (name : Fin n) : Prop :=
  ∃ result, lookup table input name = some result

/-- Structural expression evaluation reads nonterminals only from the table.
`none` is an internal missing-cell signal, never PEG rejection. -/
def evalExpr [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (table : Table n Sym) : Expr (Fin n) Sym → List Sym → Option (Result Sym)
  | .eps, input => some (.ok input)
  | .fail, _ => some .err
  | .any, [] => some .err
  | .any, _ :: rest => some (.ok rest)
  | .term _, [] => some .err
  | .term expected, actual :: rest =>
      some (if expected = actual then .ok rest else .err)
  | .nonterm name, input => lookup table input name
  | .seq left right, input => do
      match ← evalExpr G table left input with
      | .err => pure .err
      | .ok middle => evalExpr G table right middle
  | .alt left right, input => do
      match ← evalExpr G table left input with
      | .ok rest => pure (.ok rest)
      | .err => evalExpr G table right input
  | .notP body, input => do
      match ← evalExpr G table body input with
      | .ok _ => pure .err
      | .err => pure (.ok input)

theorem evalExpr_sound [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (table : Table n Sym) (htable : Sound G table)
    {expr : Expr (Fin n) Sym} {input : List Sym} {result : Result Sym}
    (hresult : evalExpr G table expr input = some result) :
    Eval G expr input result := by
  induction expr generalizing input result with
  | eps =>
      have hr : result = .ok input := by simpa [evalExpr] using hresult.symm
      cases hr
      exact .eps
  | fail =>
      have hr : result = .err := by simpa [evalExpr] using hresult.symm
      cases hr
      exact .fail
  | any =>
      cases input with
      | nil =>
          have hr : result = .err := by simpa [evalExpr] using hresult.symm
          cases hr
          exact .anyNil
      | cons symbol rest =>
          have hr : result = .ok rest := by simpa [evalExpr] using hresult.symm
          cases hr
          exact .anyOk
  | term expected =>
      cases input with
      | nil =>
          have hr : result = .err := by simpa [evalExpr] using hresult.symm
          cases hr
          exact .termNil
      | cons actual rest =>
          by_cases hsame : expected = actual
          · subst actual
            have hr : result = .ok rest := by
              simpa [evalExpr] using hresult.symm
            cases hr
            exact .termOk
          · have hr : result = .err := by
              simpa [evalExpr, hsame] using hresult.symm
            cases hr
            exact .termNe hsame
  | nonterm name => exact htable input name result hresult
  | seq left right ihLeft ihRight =>
      cases hleft : evalExpr G table left input with
      | none => simp [evalExpr, hleft] at hresult
      | some leftResult =>
          cases leftResult with
          | err =>
              have hr : result = .err := by simpa [evalExpr, hleft] using hresult.symm
              cases hr
              exact .seqErr (ihLeft hleft)
          | ok middle =>
              have hright : evalExpr G table right middle = some result := by
                simpa [evalExpr, hleft] using hresult
              exact .seqOk (ihLeft hleft) (ihRight hright)
  | alt left right ihLeft ihRight =>
      cases hleft : evalExpr G table left input with
      | none => simp [evalExpr, hleft] at hresult
      | some leftResult =>
          cases leftResult with
          | ok rest =>
              have hr : result = .ok rest := by
                simpa [evalExpr, hleft] using hresult.symm
              cases hr
              exact .altOk (ihLeft hleft)
          | err =>
              have hright : evalExpr G table right input = some result := by
                simpa [evalExpr, hleft] using hresult
              exact .altErr (ihLeft hleft) (ihRight hright)
  | notP body ih =>
      cases hbody : evalExpr G table body input with
      | none => simp [evalExpr, hbody] at hresult
      | some bodyResult =>
          cases bodyResult with
          | ok rest =>
              have hr : result = .err := by
                simpa [evalExpr, hbody] using hresult.symm
              cases hr
              exact .notOk (ih hbody)
          | err =>
              have hr : result = .ok input := by
                simpa [evalExpr, hbody] using hresult.symm
              cases hr
              exact .notErr (ih hbody)

/-- If every proper-suffix cell and every syntactically same-position call is
present, structural evaluation cannot encounter an absent table entry. -/
theorem evalExpr_present [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (table : Table n Sym) (htable : Sound G table)
    {expr : Expr (Fin n) Sym} {input : List Sym}
    (shorter : ∀ suffix, suffix <:+ input → suffix.length < input.length →
      ∀ name, Filled table suffix name)
    (same : ∀ name, name ∈ Expr.samePositionCalls expr →
      Filled table input name) :
    ∃ result, evalExpr G table expr input = some result := by
  induction expr generalizing input with
  | eps => exact ⟨.ok input, rfl⟩
  | fail => exact ⟨.err, rfl⟩
  | any =>
      cases input with
      | nil => exact ⟨.err, rfl⟩
      | cons symbol rest => exact ⟨.ok rest, rfl⟩
  | term expected =>
      cases input with
      | nil => exact ⟨.err, rfl⟩
      | cons actual rest =>
          by_cases hsame : expected = actual
          · subst actual
            exact ⟨.ok rest, by simp [evalExpr]⟩
          · exact ⟨.err, by simp [evalExpr, hsame]⟩
  | nonterm name => exact same name (by simp [Expr.samePositionCalls])
  | seq left right ihLeft ihRight =>
      obtain ⟨leftResult, hleft⟩ := ihLeft shorter (fun name hname =>
        same name (by simp [Expr.samePositionCalls, hname]))
      cases leftResult with
      | err => exact ⟨.err, by simp [evalExpr, hleft]⟩
      | ok middle =>
          have hleftEval : Eval G left input (.ok middle) :=
            evalExpr_sound G table htable hleft
          have hmiddleSuffix : middle <:+ input := eval_remainder_suffix hleftEval
          have hrightShorter : ∀ suffix, suffix <:+ middle →
              suffix.length < middle.length → ∀ name, Filled table suffix name := by
            intro suffix hsuffix hlength name
            exact shorter suffix (hsuffix.trans hmiddleSuffix)
              (Nat.lt_of_lt_of_le hlength hmiddleSuffix.length_le) name
          have hrightSame : ∀ name,
              name ∈ Expr.samePositionCalls right → Filled table middle name := by
            intro name hname
            rcases Nat.lt_or_eq_of_le hmiddleSuffix.length_le with hlt | heq
            · exact shorter middle hmiddleSuffix hlt name
            · have hm : middle = input := hmiddleSuffix.eq_of_length heq
              subst middle
              by_cases hconsumes : Expr.guaranteedConsumes left = true
              · exact (Nat.ne_of_lt
                  (guaranteedConsumes_sound hleftEval hconsumes) rfl).elim
              · exact same name (by
                  simp [Expr.samePositionCalls, hconsumes, hname])
          obtain ⟨rightResult, hright⟩ :=
            ihRight hrightShorter hrightSame
          exact ⟨rightResult, by simp [evalExpr, hleft, hright]⟩
  | alt left right ihLeft ihRight =>
      obtain ⟨leftResult, hleft⟩ := ihLeft shorter (fun name hname =>
        same name (by simp [Expr.samePositionCalls, hname]))
      cases leftResult with
      | ok rest => exact ⟨.ok rest, by simp [evalExpr, hleft]⟩
      | err =>
          obtain ⟨rightResult, hright⟩ := ihRight shorter (fun name hname =>
            same name (by simp [Expr.samePositionCalls, hname]))
          exact ⟨rightResult, by simp [evalExpr, hleft, hright]⟩
  | notP body ih =>
      obtain ⟨bodyResult, hbody⟩ := ih shorter (fun name hname =>
        same name (by simpa [Expr.samePositionCalls] using hname))
      cases bodyResult with
      | ok rest => exact ⟨.err, by simp [evalExpr, hbody]⟩
      | err => exact ⟨.ok input, by simp [evalExpr, hbody]⟩

theorem sound_empty [DecidableEq Sym] (G : Grammar (Fin n) Sym) :
    Sound G [] := by
  intro input name result h
  simp [lookup] at h

theorem sound_insert [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (table : Table n Sym) (htable : Sound G table)
    (input : List Sym) (name : Fin n) (result : Result Sym)
    (hresult : Eval G (.nonterm name) input result) :
    Sound G (insert table input name result) := by
  intro input' name' result' hlookup
  simp only [insert, lookup] at hlookup
  split at hlookup
  next hkey =>
    have hresult_eq : result = result' := Option.some.inj hlookup
    have hinput : input = input' := congrArg (fun key => key.1) hkey
    have hname : name = name' := congrArg (fun key => key.2) hkey
    subst input'
    subst name'
    subst result'
    exact hresult
  next => exact htable input' name' result' hlookup

theorem filled_insert_same [DecidableEq Sym] (table : Table n Sym)
    (input : List Sym) (name : Fin n) (result : Result Sym) :
    Filled (insert table input name result) input name := by
  exact ⟨result, by simp [insert, lookup]⟩

theorem filled_insert_of_filled [DecidableEq Sym] (table : Table n Sym)
    (input : List Sym) (name : Fin n) (result : Result Sym)
    {input' : List Sym} {name' : Fin n}
    (hfilled : Filled table input' name') :
    Filled (insert table input name result) input' name' := by
  by_cases hkey : (input, name) = (input', name')
  · cases hkey
    exact filled_insert_same table input name result
  · obtain ⟨oldResult, hold⟩ := hfilled
    exact ⟨oldResult, by simp [insert, lookup, hkey, hold]⟩

def fillNames [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (table : Table n Sym) (input : List Sym) : List (Fin n) → Table n Sym
  | [] => table
  | name :: names =>
      match evalExpr G table (G.rule name) input with
      | none => fillNames G table input names
      | some result => fillNames G (insert table input name result) input names

theorem sound_fillNames [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (table : Table n Sym) (htable : Sound G table) (input : List Sym)
    (names : List (Fin n)) : Sound G (fillNames G table input names) := by
  induction names generalizing table with
  | nil => exact htable
  | cons name names ih =>
      simp only [fillNames]
      cases hresult : evalExpr G table (G.rule name) input with
      | none => exact ih table htable
      | some result =>
          exact ih _ (sound_insert G table htable input name result
            (.nonterm (evalExpr_sound G table htable hresult)))

theorem filled_fillNames_of_filled [DecidableEq Sym]
    (G : Grammar (Fin n) Sym) (table : Table n Sym) (input input' : List Sym)
    (name' : Fin n) (names : List (Fin n))
    (hfilled : Filled table input' name') :
    Filled (fillNames G table input names) input' name' := by
  induction names generalizing table with
  | nil => exact hfilled
  | cons name names ih =>
      simp only [fillNames]
      cases hresult : evalExpr G table (G.rule name) input with
      | none => exact ih table hfilled
      | some result =>
          simpa [fillNames, hresult] using
            ih (insert table input name result)
              (filled_insert_of_filled table input name result hfilled)

theorem fillNames_complete [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) (table : Table n Sym) (htable : Sound G table)
    (input : List Sym)
    (shorter : ∀ suffix, suffix <:+ input → suffix.length < input.length →
      ∀ name, Filled table suffix name)
    (before after : List (Fin n))
    (horder : schedule.order = before ++ after)
    (hbefore : ∀ name, name ∈ before → Filled table input name) :
    ∀ name, name ∈ before ++ after →
      Filled (fillNames G table input after) input name := by
  induction after generalizing table before with
  | nil =>
      intro name hname
      exact hbefore name (by simpa using hname)
  | cons caller after ih =>
      have hpresent : ∃ result,
          evalExpr G table (G.rule caller) input = some result :=
        evalExpr_present G table htable shorter (fun callee hcall =>
          hbefore callee (schedule.earlier horder hcall))
      obtain ⟨result, hresult⟩ := hpresent
      have hnewSound : Sound G (insert table input caller result) :=
        sound_insert G table htable input caller result
          (.nonterm (evalExpr_sound G table htable hresult))
      have hnewShorter : ∀ suffix, suffix <:+ input →
          suffix.length < input.length →
          ∀ name, Filled (insert table input caller result) suffix name := by
        intro suffix hsuffix hlength name
        exact filled_insert_of_filled table input caller result
          (shorter suffix hsuffix hlength name)
      have hnewBefore : ∀ name, name ∈ before ++ [caller] →
          Filled (insert table input caller result) input name := by
        intro name hname
        rcases List.mem_append.mp hname with hold | hcaller
        · exact filled_insert_of_filled table input caller result
            (hbefore name hold)
        · have : name = caller := by simpa using hcaller
          subst name
          exact filled_insert_same table input caller result
      have hnewOrder : schedule.order = (before ++ [caller]) ++ after := by
        simpa [List.append_assoc] using horder
      have hrec := ih (table := insert table input caller result)
        (before := before ++ [caller]) hnewSound hnewShorter hnewOrder hnewBefore
      intro name hname
      have hmembership : name ∈ (before ++ [caller]) ++ after := by
        simpa [List.append_assoc] using hname
      simpa [fillNames, hresult] using hrec name hmembership

/-- Process the empty suffix first, then extend outward one input symbol at a
time.  At each suffix, process the certified nonterminal order. -/
def fillSuffixes [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) : List Sym → Table n Sym
  | [] => fillNames G [] [] schedule.order
  | symbol :: rest =>
      fillNames G (fillSuffixes G schedule rest) (symbol :: rest) schedule.order

theorem sound_fillSuffixes [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) (input : List Sym) :
    Sound G (fillSuffixes G schedule input) := by
  induction input with
  | nil => exact sound_fillNames G [] (sound_empty G) [] schedule.order
  | cons symbol rest ih => exact sound_fillNames G _ ih _ schedule.order

theorem suffix_of_proper_suffix_cons {suffix rest : List Sym} {symbol : Sym}
    (hsuffix : suffix <:+ symbol :: rest)
    (hlength : suffix.length < (symbol :: rest).length) :
    suffix <:+ rest := by
  obtain ⟨before, hbefore⟩ := hsuffix
  cases before with
  | nil =>
      simp only [List.nil_append] at hbefore
      subst suffix
      simp at hlength
  | cons head tail =>
      simp only [List.cons_append] at hbefore
      injection hbefore with _ htail
      exact ⟨tail, htail⟩

theorem fillSuffixes_complete [DecidableEq Sym]
    (G : Grammar (Fin n) Sym) (schedule : RankSchedule G) (input : List Sym) :
    ∀ suffix, suffix <:+ input → ∀ name,
      Filled (fillSuffixes G schedule input) suffix name := by
  induction input with
  | nil =>
      have hcurrent := fillNames_complete G schedule [] (sound_empty G) []
        (fun suffix _ hlength => by simp at hlength) [] schedule.order
        (by simp) (by simp)
      intro suffix hsuffix name
      have hsuffixNil : suffix = [] := hsuffix.eq_of_length (by
        exact Nat.eq_zero_of_le_zero hsuffix.length_le)
      subst suffix
      exact hcurrent name (by simp [schedule.complete name])
  | cons symbol rest ih =>
      let previous := fillSuffixes G schedule rest
      have hpreviousSound : Sound G previous := sound_fillSuffixes G schedule rest
      have hshorter : ∀ suffix, suffix <:+ symbol :: rest →
          suffix.length < (symbol :: rest).length →
          ∀ name, Filled previous suffix name := by
        intro suffix hsuffix hlength name
        exact ih suffix (suffix_of_proper_suffix_cons hsuffix hlength) name
      have hcurrent := fillNames_complete G schedule previous hpreviousSound
        (symbol :: rest) hshorter [] schedule.order (by simp) (by simp)
      intro suffix hsuffix name
      by_cases heq : suffix = symbol :: rest
      · subst suffix
        exact hcurrent name (by simp [schedule.complete name])
      · have hlength : suffix.length < (symbol :: rest).length := by
          have hle := hsuffix.length_le
          exact Nat.lt_of_le_of_ne hle (fun hlen =>
            heq (hsuffix.eq_of_length hlen))
        have hold : Filled previous suffix name :=
          ih suffix (suffix_of_proper_suffix_cons hsuffix hlength) name
        exact filled_fillNames_of_filled G previous (symbol :: rest)
          suffix name schedule.order hold

end TableEval

/-- The public evaluator has no fuel or missing-entry outcome.  Its internal
table lookup is unwrapped only with the rank/suffix completeness proof. -/
def evalTable [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) (input : List Sym) : Result Sym :=
  let table := TableEval.fillSuffixes G schedule input
  let present := TableEval.fillSuffixes_complete G schedule input input
    (by simp) G.start
  (TableEval.lookup table input G.start).get
    (Option.isSome_iff_exists.mpr present)

theorem evalTable_sound [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) (input : List Sym) :
    Eval G (.nonterm G.start) input (evalTable G schedule input) := by
  let table := TableEval.fillSuffixes G schedule input
  let present := TableEval.fillSuffixes_complete G schedule input input
    (by simp) G.start
  let isSome : (TableEval.lookup table input G.start).isSome = true :=
    Option.isSome_iff_exists.mpr present
  have hlookup : TableEval.lookup table input G.start =
      some ((TableEval.lookup table input G.start).get isSome) :=
    (Option.some_get isSome).symm
  exact TableEval.sound_fillSuffixes G schedule input input G.start
    (evalTable G schedule input) (by
      simpa only [evalTable, table, present, isSome] using hlookup)

theorem evalTable_eq_of_eval [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (schedule : RankSchedule G) (input : List Sym) (result : Result Sym)
    (hresult : Eval G (.nonterm G.start) input result) :
    evalTable G schedule input = result :=
  eval_deterministic (evalTable_sound G schedule input) hresult

theorem no_self_schedule [DecidableEq Sym] (G : Grammar (Fin n) Sym)
    (name : Fin n) (hrule : G.rule name = .nonterm name) :
    RankSchedule G → False := by
  intro schedule
  obtain ⟨before, after, horder⟩ := List.mem_iff_append.mp (schedule.complete name)
  have hcall : name ∈ Expr.samePositionCalls (G.rule name) := by
    rw [hrule]
    simp [Expr.samePositionCalls]
  have hbefore : name ∈ before := schedule.earlier horder hcall
  have hnodup : (before ++ name :: after).Nodup := by
    simpa [horder] using schedule.nodup
  have hcross := (List.nodup_append.mp hnodup).2.2
  exact hcross name hbefore name (by simp) rfl

end FPRD