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