# Zulip Chat Archive

## 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