Zulip Chat Archive

Stream: new members

Topic: Induction and well-founded recursion


view this post on Zulip 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.

view this post on Zulip Fox Thomson (Oct 14 2020 at 18:48):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 14 2020 at 22:44):

You have two conflicting inductions in this proof

view this post on Zulip 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 } }

view this post on Zulip Mario Carneiro (Oct 14 2020 at 22:49):

@Fox Thomson


Last updated: May 08 2021 at 10:12 UTC