Proving Decidable on inductive Prop

Stream: new members

[Filip Hovorka]

Hello, I recently started learning Lean and this is my first post here.

I am trying to prove some things about εNFA currently and I got stuck on this definition.

import Mathlib.Data.FinEnum
import Mathlib.Data.Option.Basic

structure εNFA (σ : Type _) where
  q : Type _                    -- states
  init : q                      -- initial state
  fs : Finset q                 -- accepting states
  δ : q → Option σ → Finset q   -- transition function
  [fq : FinEnum q]
  [fσ : FinEnum σ]

variable {σ : Type _} [FinEnum σ] (tn : εNFA σ)

inductive εclosure (a : tn.q) : tn.q → Prop where
  | base (_ : tn.q) : εclosure a a
  | step (b : tn.q) : εclosure a b → ∀ c : (tn.δ b none) , εclosure a (c.1)

instance : DecidableRel (εclosure tn) := sorry

I am fairly sure that the inductive relationship should be Decidable, but I'm not sure how to prove it.

So far I tried separating it into a = b, a ≠ b as well as using that tn.q is FinEnum and doing induction on List or Finset of tn.q
but I got stuck on the former and I'm not sure the latter would be of much help and if it was, I think it wouldn't be a nice solution.

What would be a good way of proving Decidable (εclosure tn a b) or should I change the definition of εclosure? Is it even truly Decidable?

[Eric Wieser]

Can you make that a #mwe with imports?

[Filip Hovorka]

Eric Wieser said:

Can you make that a #mwe with imports?

Oh sorry, I'll edit it now

[Eric Wieser]

Usually the best way to prove this type of thing is write a lemma of the form εclosure tn a b ↔ _, where the _ is some obviously enumerable expression

[Eric Wieser]

Your base (_ : tn.q) : εclosure a a constructor looks wonky to me; what's the point in the _ variable?

[Eric Wieser]

Your [FinEnum α] is also suspicious, as you don't ever use α

[Filip Hovorka]

I see, so I can just leave | base : εclosure a a?
I used α in a different part of the code so now I realize that I shouldn't probably include that, sorry.
I also tried doing the ↔ lemma and I came up with lemma εclosure_iff_exists (a b : tn.q) : εclosure tn a b ↔ (∃ c : tn.q , εclosure tn a c ∧ b ∈ tn.δ c none) ∨ a = b but I suppose I just have to come up with something better.

[Eric Rodriguez]

that doesn't seem very decidable to me, that lemma

[Eric Wieser]

To answer your earlier question, here's an example of how to case on a = b:

instance [DecidableEq tn.q] : DecidableRel (εclosure tn) := fun a b =>
  if h : a = b then
    .isTrue (h ▸ .base b)
  else
    sorry

[Eric Wieser]

But it seems like this is useless because your construction doesn't look like it ever is going to use a ≠ b

[Eric Wieser]

Perhaps the easier thing to do is write a function that computes as a Bool whether εclosure is true, and then prove it agrees with the inductive definition

[Filip Hovorka]

Eric Rodriguez said:

that doesn't seem very decidable to me, that lemma

Do you mean that the εclosure doesn't seem decidable to you or the lemma doesn't imply decidable? I don't think the lemma is very useful so that's why I said I need something better.

[Eric Wieser]

One algorithm is:

• Compute the transitive closure of q → Finset q starting at a (which you can do in at most Fintype.card q iterations)
• εclosure a b is true if b is in this set (which is decidable)

[Eric Wieser]

Do we have DFS/BFS of directed graphs?

[Filip Hovorka]

Eric Wieser said:

One algorithm is:

• Compute the transitive closure of q → Finset q starting at a (which you can do in at most Fintype.card q iterations)
• εclosure a b is true if b is in this set (which is decidable)

I see, thanks. I was thinking about these sort of solutions and I guess I was mainly asking to see whether there is some way to use the fact that εclosure is inductive. I was thinking that perhaps I could somehow prove for the base case that it is Decidable and then for step which would mean it is Decidable

[Filip Hovorka]

It's just that I didn't anticipate this part (the fact that εclosure is Decidable) to be troublesome but it is more tricky than I expected