failure to synthesize decidable eq

Stream: lean4

[Paige Thomas]

I was wondering if anyone might know why these errors are occurring at symbol_arrow_fun := symbol_arrow_list_to_fun [⟨0, c, 1⟩]?

failed to synthesize instance
  OfNat (State α (char c)) 0

failed to synthesize instance
  OfNat (State α (char c)) 1

failed to synthesize instance
  DecidableEq (State α (char c))

def RegExp.State
  (α : Type)
  [DecidableEq α] :
  RegExp α → Type
| char _ => ℕ
| epsilon => ℕ
| zero => ℕ
| union R S => R.State ⊕ S.State
| concat R S => R.State ⊕ S.State
| closure R => Option R.State


def RegExp.toEpsilonNFA
  {α : Type}
  [DecidableEq α]
  (R : RegExp α) :
  EpsilonNFA α R.State :=
  match R with
  | char c =>
    {
      symbol_arrow_fun := symbol_arrow_list_to_fun [⟨0, c, 1⟩]
      epsilon_arrow_list := []
      starting_state_list := [0]
      accepting_state_list := [1]
    }

[Chris Bailey]

What is symbol_arrow_list_to_fun?

[Paige Thomas]

structure SymbolArrow
  (α : Type)
  (σ : Type) :
  Type :=
  (start_state : σ)
  (symbol : α)
  (stop_state : σ)
  deriving Repr


/--
  The accumulated stop states of all of the arrows in the list that have a start state and symbol matching the given state and symbol.
-/
@[simp]
def symbol_arrow_list_to_fun
  {α : Type}
  [DecidableEq α]
  {σ : Type}
  [DecidableEq σ]
  (symbol_arrow_list : List (SymbolArrow α σ))
  (start_state : σ)
  (symbol : α) :
  List σ :=
  (symbol_arrow_list.filterMap (fun (arrow : SymbolArrow α σ) =>
    if arrow.start_state = start_state ∧ arrow.symbol = symbol
    then Option.some arrow.stop_state
    else Option.none)).dedup

[Paige Thomas]

structure EpsilonNFA
  (α : Type)
  (σ : Type) :
  Type :=
  (symbol_arrow_fun : σ → α → List σ)
  (epsilon_arrow_list : List (σ × σ))
  (starting_state_list : List σ)
  (accepting_state_list : List σ)

[Paige Thomas]

Lean 4 Web instance

[Chris Bailey]

I didn't look at this super deeply since it's complicated, but it appears that you need to make RegExp.State reducible or an abbrev like so:

@[reducible]
  def RegExp.State
  (α : Type)
  [DecidableEq α] :
  RegExp α → Type
| char _ => ℕ
| epsilon => ℕ
| zero => ℕ
| union R S => R.State ⊕ S.State
| concat R S => R.State ⊕ S.State
| closure R => Option R.State

You're trying to get Lean to recognize that State α (char c)) is Nat, but it's not unfolding State to look at the definition since it's not reducible.

[Paige Thomas]

I see. Thank you!