## Stream: new members

### Topic: Proving Decidable on inductive Prop

#### Filip Hovorka (Aug 09 2023 at 14:41):

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 (Aug 09 2023 at 14:42):

Can you make that a #mwe with imports?

#### Filip Hovorka (Aug 09 2023 at 14:46):

Eric Wieser said:

Can you make that a #mwe with imports?

Oh sorry, I'll edit it now

#### Eric Wieser (Aug 09 2023 at 15:05):

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 (Aug 09 2023 at 15:07):

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

#### Eric Wieser (Aug 09 2023 at 15:08):

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

#### Filip Hovorka (Aug 09 2023 at 15:28):

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 (Aug 09 2023 at 15:32):

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

#### Eric Wieser (Aug 09 2023 at 15:34):

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 (Aug 09 2023 at 15:34):

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

#### Eric Wieser (Aug 09 2023 at 15:36):

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 (Aug 09 2023 at 15:36):

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 (Aug 09 2023 at 15:39):

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 (Aug 09 2023 at 15:40):

Do we have DFS/BFS of directed graphs?

#### Filip Hovorka (Aug 09 2023 at 15:44):

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 (Aug 09 2023 at 15:48):

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

Last updated: Dec 20 2023 at 11:08 UTC