# Zulip Chat Archive

## Stream: new members

### Topic: Induction and well-founded recursion

#### Fox Thomson (Oct 14 2020 at 18:35):

'minimum' working example:

```
import data.fintype.basic
universes u v
variable {α : Type u}
structure ε_NFA (alphabet : Type u) :=
[alphabet_fintype : fintype alphabet]
(state : Type v)
[state_fintype : fintype state]
[state_dec : decidable_eq state]
(step : state → option alphabet → finset state)
(start : finset state)
(accept_states : finset state)
namespace ε_NFA
instance dec (M : ε_NFA α) := M.state_dec
instance fin₁ (M : ε_NFA α) : fintype α := M.alphabet_fintype
instance fin₂ (M : ε_NFA α) : fintype M.state := M.state_fintype
def step_set' (M : ε_NFA α) : finset M.state → option α → finset M.state :=
λ Ss a, finset.bind Ss (λ S, M.step S a)
inductive ε_closure_set (M : ε_NFA α) : finset M.state → M.state → Prop
| base : ∀ Ss (S ∈ Ss), ε_closure_set Ss S
| step : ∀ Ss S T, ε_closure_set Ss S → T ∈ M.step S option.none → ε_closure_set Ss T
instance ε_NFA_has_well_founded {β : Type u} [fintype β] [decidable_eq β] : has_well_founded (finset β) :=
{ r := (λ S₁ S₂ : finset β, S₁ᶜ < S₂ᶜ),
wf := inv_image.wf _ finset.lt_wf }
lemma sub_of_compl {β : Type u} [fintype β] [decidable_eq β] : ∀ T U : finset β, Tᶜ ⊆ Uᶜ → U ⊆ T := sorry
def ε_closure (M : ε_NFA α) : finset M.state → finset M.state
| S :=
begin
let S' := S ∪ M.step_set' S none,
by_cases heq : S' = S,
{ exact S },
{ let : S'ᶜ < Sᶜ,
{ sorry },
exact ε_closure S' }
end
using_well_founded {dec_tac := tactic.assumption}
lemma MWE (M : ε_NFA α) :
Π (S : finset M.state) (s : M.state), M.ε_closure_set S s → s ∈ M.ε_closure S
| S :=
begin
intro s,
{ intro h,
rw ε_closure,
dsimp,
split_ifs with heq,
{ sorry },
induction h with S t ht S t' t ht' ht ih,
{ let : (S ∪ M.step_set' S none)ᶜ < Sᶜ,
{ sorry },
let : has_well_founded.r (S ∪ M.step_set' S none) S,
{ assumption },
apply MWE (S ∪ M.step_set' S none), -- failed to prove recursive application
sorry },
{ sorry } }
end
using_well_founded {dec_tac := tactic.assumption}
end ε_NFA
```

At the `apply MWE`

line I am getting a well-founded recursion problem, how come I do not get this in the definition of `ε_closure`

and how do I fix this? I have been able to prove the other direction without the error.

#### Fox Thomson (Oct 14 2020 at 18:48):

I have just realized that I have reused `S`

as a variable name.

#### Fox Thomson (Oct 14 2020 at 18:55):

I think the problem boils down to a situation like this:

```
lemma MWE' : Π n : ℕ, n = n
| n :=
begin
induction n with m ih,
{ refl },
{ let h := MWE' m,
refl }
end
```

How can I show that `m<n`

.

#### Ruben Van de Velde (Oct 14 2020 at 19:54):

In your second case, don't you need to use the induction hypothesis `ih`

instead of trying to apply `MWE'`

manually?

#### Ruben Van de Velde (Oct 14 2020 at 19:55):

In the first case, you seem to be trying to use an induction hypothesis in the base case

#### Fox Thomson (Oct 14 2020 at 20:03):

As `epsilon_closure`

is recursively defined and `epsilon_closure_set`

is inductively defined I am using two forms of induction, the error is happening in the base case generated by the `induction`

tactic on `epsilon_closure_set`

but it occurs in the 'inductive hypothesis' generated by the `split_ifs`

tactic.

#### Fox Thomson (Oct 14 2020 at 20:04):

`MWE'`

is a silly proof to illustrate the problem, there is no need to define `h`

but I should be able to, and I need something like that for my original problem.

#### Mario Carneiro (Oct 14 2020 at 22:35):

The way to write proofs like that is to declare the recursion structure up front in the equations:

```
lemma MWE' : Π n : ℕ, n = n
| 0 := by { refl }
| (m+1) := begin
{ let h := MWE' m,
refl }
end
```

#### Mario Carneiro (Oct 14 2020 at 22:41):

The problem with your original MWE is that there is a shadowed variable in the middle, you are referencing the wrong `S`

#### Mario Carneiro (Oct 14 2020 at 22:44):

You have two conflicting inductions in this proof

#### Mario Carneiro (Oct 14 2020 at 22:49):

aha, the issue is that `ε_closure_set`

unnecessarily takes `Ss`

as an index to the inductive family, so it is allowed to vary in the induction and then you lose track of the original `S`

. Use

```
inductive ε_closure_set (M : ε_NFA α) (Ss : finset M.state) : M.state → Prop
| base : ∀ (S ∈ Ss), ε_closure_set S
| step : ∀ S T, ε_closure_set S → T ∈ M.step S option.none → ε_closure_set T
```

and then

```
induction h with t ht t' t ht' ht ih,
{ let : (S ∪ M.step_set' S none)ᶜ < Sᶜ,
{ sorry },
let : has_well_founded.r (S ∪ M.step_set' S none) S,
{ assumption },
apply MWE (S ∪ M.step_set' S none), -- works
sorry },
{ sorry } }
```

#### Mario Carneiro (Oct 14 2020 at 22:49):

@Fox Thomson

Last updated: May 08 2021 at 10:12 UTC