Strange typing failure

Stream: new members

[Ching-Tsun Chou]

Consider the following definitions:

import Mathlib.Data.Set.Card

class Automata (A : Type*) where
  State : Type*
  init : Set State
  next : State → A → Set State

class DetAutomata (A : Type*) extends Automata A where
  get_init : State
  get_next : State → A → State
  det_init : init = {get_init}
  det_next : ∀ s a, next s a = {get_next s a}

variable {A : Type*}

def AutomataPSet (M : Automata A) : DetAutomata A where
  State := Set M.State
  init := {M.init}
  next := fun ps a ↦ { ⋃ s ∈ ps, M.next s a }
  get_init := M.init
  get_next := fun ps a ↦ ⋃ s ∈ ps, M.next s a
  det_init := by simp
  det_next := by simp

variable (M : Automata A) (s : M.State) (p : (AutomataPSet M).State)
#check (p : Set M.State)
#check (s ∈ p)

The last #check above produces this error message:

failed to synthesize
  Membership (Automata.State A) (Automata.State A)

Why? The penultimate #check verifies that p is a set of M.State. Why doesn't s ∈ p type-check?

[Aaron Liu]

Although the type of p is defeq to Set M.State, it is not reducibly defeq, and so typeclass inference will not see through.

[Ching-Tsun Chou]

How do I make ∈ work here?

[Aaron Liu]

You can make AutomataPSet reducible or you can write an instance of Membership (Automata.State A) (Automata.State A).

[Aaron Liu]

Probably a better way would be to not bundle the state, so you don't have this problem in the first place.

[Ching-Tsun Chou]

Thanks! What do you mean by "not bundling the state"?

[Aaron Liu]

class Automata (A : Type*) (State : Type*) where

[Ching-Tsun Chou]

I see. Actually I started with that approach. However, I wanted to have a definition like the following one, which becomes messier if I don't bundle the state.

def AutomataSum (M : I → Automata A) : Automata A where
  State := Σ i : I, (M i).State
  init := ⋃ i : I, Sigma.mk i '' (M i).init
  next := fun ⟨i, s⟩ a ↦ Sigma.mk i '' (M i).next s a

[Aaron Liu]

How does this become messier?

[Ching-Tsun Chou]

AutomataSum will need an additonal argument of an indexed family of states.

[Ching-Tsun Chou]

For another example, suppose I want to define AutomataSum of only 2 automata M1 amd M2. With the bundled approach, I need three arguments: A, M1, M2. With the unbundled approach, I need five arguments: A, S1, S2, M1, M2, where S1 and S2 are the state types of M1 and M2.

[Aaron Liu]

That can be implicit argument?

[Ching-Tsun Chou]

There is also the problem of how you define the State of AutomataSum and AutomataPSet, if State is an input instead of an output.

[Ching-Tsun Chou]

You end up with two parallel sets of definitions, one working on the state types and the other working on the automata classes.