Making NFA language membership decidable by dec_trivial

Stream: general

[Arthur Correnson]

Hi all,
I am currently working on formalizing results on finite word automaton (also with @Laurent Bartholdi ) and, ideally, we would like to be able to compute with automata to prove language membership automatically (by dec_trivial for example).

The current definition (provided by @Fox Thomson ) of NFAs in mathlib uses sets and does not make any assumption on the decidability of the underlying types:

/-- An NFA is a set of states (`σ`), a transition function from state to state labelled by the
  alphabet (`step`), a starting state (`start`) and a set of acceptance states (`accept`).
  Note the transition function sends a state to a `set` of states. These are the states that it
  may be sent to. -/
structure NFA (α : Type u) (σ : Type v) :=
(step : σ → α → set σ)
(start : set σ)
(accept : set σ)

Therefore, if we want to prove a statement of the form my_word \in NFA.accepts my_automata, we have to unfold all the definitions and do the proof manually where we ideally would like to just do a dec_trivial.

In a proof assistant like Coq, I would start with a definition of automata based on lists of elements of a decidable type rather than sets
and simply compute. I am a complete beginner with Lean butI I feel like it's not the idiomatic Lean way to achieve this goal and that I should try to use type classes instead. Any idea/advice on how to do that the Lean way without changing the definitions ?

[Yaël Dillies]

Salut ! The idiomatic way to do this would be to show that A.accepts is decidable if ∀ a b, decidable_pred (∈ A.step a b), decidable_pred (∈ A.start), decidable_pred (∈ A.accept)

[Yaël Dillies]

Then whenever you have a "decidable automata", you can prove the three starting instances step, start, accept and Lean will provide you the accepts one. That might sound like you need to write three times the number of automata you want to evaluate, but in practice I assume you will write a NFA constructor starting from a list (as your message alludes to), in which case you can write three generic decidability instances that will take care of everything for you.

[Martin Dvořák]

Do you have a repository?

[Arthur Correnson]

Yaël Dillies said:

Salut ! The idiomatic way to do this would be to show that A.accepts is decidable if ∀ a b, decidable_pred (∈ A.step a b), decidable_pred (∈ A.start), decidable_pred (∈ A.accept)

Thanks for the answer ! Proving these lemmas if the sets are built from lists should be straightforward. I'm not sure how to tell lean to exploit these lemmas tho.

[Arthur Correnson]

Martin Dvořák said:

Do you have a repository?

Only a local one ^^ (for now)

[Martin Dvořák]

If I were you, I wouldn't aim for full automation. Instead, I'd let the programmer provide the non-deterministic choices and automate making a proof from that.

[Eric Wieser]

I think the instance that @Yaël Dillies suggests is still a good idea

[Yaël Dillies]

instance [fintype A.accept] (A : NFA α σ) [Π a b, decidable_pred (∈ A.step a b)]
  [decidable_pred (∈ A.start)] [decidable_pred (∈ A.accept)] : decidable_pred (∈ A.accepts) :=
λ l, decidable_of_iff some_equivalent_thing_here your_proof_that_it_is_equivalent

is how I would start.

[Eric Wieser]

docs#NFA.accepts is a language not a predicate

[Yaël Dillies]

Fixed!

[Reid Barton]

Also σ needs to be finite

[Eric Wieser]

Only A.accept does

[Eric Wieser]

This might be a good start:

instance decidable_pred_mem_eval_from (A : NFA α σ)
  [Π a b, decidable_pred (∈ A.step a b)] [decidable_pred (∈ A.start)]
  (S l) : decidable_pred (∈ A.eval_from S l) :=
begin
  delta eval_from,
  sorry
end

instance decidable_pred_mem_eval (A : NFA α σ) [Π a b, decidable_pred (∈ A.step a b)] [decidable_pred (∈ A.start)]
  [decidable_pred (∈ A.accept)] (x) : decidable_pred (∈ A.eval x) :=
NFA.decidable_pred_mem_eval_from _ _ _

instance decidable_pred_mem_accepts (A : NFA α σ) [Π a b, decidable_pred (∈ A.step a b)] [decidable_pred (∈ A.start)]
  [decidable_pred (∈ A.accept)] [fintype (A.accept)] : decidable_pred (∈ A.accepts) :=
begin
  dsimp [accepts],
  sorry
end

[Yaël Dillies]

Isn't dsimp in a decidability instance bad because the eq.recs won't reduce?

[Eric Wieser]

dsimp doesn't use eq.rec, it uses id

[Yaël Dillies]

Martin Dvořák said:

If I were you, I wouldn't aim for full automation. Instead, I'd let the programmer provide the non-deterministic choices and automate making a proof from that.

Just to explain the difference with this approach, non-deterministic choices would involve writing tactic code, probably in the form of a tactic#norm_num extension. This is probably the best solution long term (because Lean is so bad at computing), but much harder to implement and we want the decidability instances either way. So as long as you're not evaluating automata with 100 states or something, I would recommend against it.

[Eric Wieser]

But also, it's usually easiest to write these instances using bad defeqs, and then clean them up once you've worked out what you need

[Yaël Dillies]

Yes, absolutely.

[Arthur Correnson]

Thanks a lot for all the helpful advices ! I'll work on it ^^

[Yaël Dillies]

Decidability is finicky so keep asking questions if you have more!

[Eric Wieser]

Eric Wieser said:

Only A.accept does

I take it back, this causes annoying typeclass problems.

[Eric Wieser]

I got sniped by this:

instance fintype.decidable_mem_bUnion {α β} [fintype α] (p : α → Prop) [decidable_pred p]
  (s : α → set β) (b : β) [Π a, decidable (b ∈ s a)] :
  decidable (b ∈ ⋃ a (h : p a), s a) :=
decidable_of_iff' (∃ a (h : p a), b ∈ s a) set.mem_Union₂

instance decidable_pred_mem_step_set [fintype σ] (A : NFA α σ)
  [Π a b, decidable_pred (∈ A.step a b)]
  (S l) [decidable_pred (∈ S)] : decidable_pred (∈ A.step_set S l) :=
λ _, fintype.decidable_mem_bUnion _ _ _

instance decidable_pred_mem_eval_from [fintype σ] (A : NFA α σ)
  [Π a b, decidable_pred (∈ A.step a b)] (S) [decidable_pred (∈ S)] (l) :
  decidable_pred (∈ A.eval_from S l) :=
begin
  unfreezingI {induction l with x xs ih generalizing S},
  { exact ‹decidable_pred (∈ S)› },
  { exact ih (A.step_set S x), },
end

instance decidable_pred_mem_eval [fintype σ] (A : NFA α σ)
  [Π a b, decidable_pred (∈ A.step a b)] [decidable_pred (∈ A.start)] (x) :
  decidable_pred (∈ A.eval x) :=
NFA.decidable_pred_mem_eval_from _ _ _

instance decidable_pred_mem_accepts [fintype σ] (A : NFA α σ)
  [Π a b, decidable_pred (∈ A.step a b)] [decidable_pred (∈ A.start)]
  [decidable_pred (∈ A.accept)] :
  decidable_pred (∈ A.accepts) :=
λ _, fintype.decidable_exists_fintype

[Eric Wieser]

I suspect that decidable_of_iff' (∃ i ∈ S, x ∈ A.step i l) set.mem_Union₂ should be a lemma along the lines of fintype.decidable_mem_bUnion

[Yaël Dillies]

Doesn't seem to exist.

[Eric Wieser]

instance fintype.decidable_mem_bUnion {α β} [fintype α] (p : α → Prop) [decidable_pred p]
  (s : α → set β) (b : β) [Π a, decidable (b ∈ s a)] :
  decidable (b ∈ ⋃ a (h : p a), s a) :=
decidable_of_iff' (∃ a (h : p a), b ∈ s a) set.mem_Union₂

[Yaël Dillies]

And could we have the same for finset.sup/finset.inf/finset.bUnion?

[Yaël Dillies]

Can you also not have s : Π a (h : p a), set β in fintype.decidable_mem_bUnion?

[Eric Wieser]

I think that behaves poorly if s is non-dependent

[Eric Wieser]

Yaël Dillies said:

And could we have the same for finset.sup/finset.inf/finset.bUnion?

Or even for list.foldl, which appeared above:

instance fintype.decidable_pred_mem_list_foldl {α β} (l : list α) (s : set β)
  (sf : set β → α → set β)
  [decidable_pred (∈ s)] [Π s a, decidable_pred (∈ sf s a)] :
  decidable_pred (∈ l.foldl sf s) :=
begin
  unfreezingI {induction l with x xs ih generalizing s},
  { exact ‹decidable_pred (∈ s)› },
  { exact ih (sf _ _), },
end