Induction and well-founded recursion

Stream: new members

[Fox Thomson]

'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]

I have just realized that I have reused S as a variable name.

[Fox Thomson]

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]

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]

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

[Fox Thomson]

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]

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]

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]

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

[Mario Carneiro]

You have two conflicting inductions in this proof

[Mario Carneiro]

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]

@Fox Thomson