Confusing recursion error message

Stream: new members

[Fox Thomson]

I am getting the error equation compiler failed to create auxiliary declaration 'MWE._main._pack' nested exception message: infer type failed, unknown variable hwf in the following code:

import data.fintype.basic
import tactic.nth_rewrite.default

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 α) (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

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), s ∈ M.ε_closure S ↔ M.ε_closure_set S s
| S :=
begin
  intro s,
  split,
  { intro h,
    rw ε_closure at h,
    dsimp at h,
    split_ifs at h with heq,
    { sorry },
    { let hwf : (S ∪ M.step_set' S none)ᶜ < Sᶜ,
      { sorry },

      have h' : M.ε_closure_set (S ∪ M.step_set' S none) s,
        rwa ←MWE (S ∪ M.step_set' S none),

      induction h' with t ht t' t d e ih,
      { sorry },
      { apply ε_closure_set.step t' t,
        { apply ih,
          rwa MWE (S ∪ M.step_set' S none) },
        assumption } } },
  { intro h,
    rw ε_closure,
    dsimp,
    split_ifs with heq;
    induction h with t ht t' t ht' ht ih,
    { sorry },
    { sorry },
    all_goals
    { let : (S ∪ M.step_set' S none)ᶜ < Sᶜ,
      sorry },
    { sorry },
    { rw MWE (S ∪ M.step_set' S none),
      apply ε_closure_set.step t' t,
      rwa ←MWE (S ∪ M.step_set' S none),
      assumption } }
end
using_well_founded {dec_tac := tactic.assumption}

end ε_NFA

There is some weird dependence with the ← direction, the error is coming from the → direction but if I sorry out all recursive terms in the ← proof the error disappears.

[Bryan Gin-ge Chen]

Not sure if this is the cause of your issues, but it seems to me like many of your lets should be haves, particularly those whose type is (something) < (something else).

[Mario Carneiro]

if you change the let hwf to hwf the error goes away, being replaced with a more sensible one about the rwa

[Fox Thomson]

If I make them haves then they aren't visible to the dec_tac

[Mario Carneiro]

you have to put them in the same term

[Mario Carneiro]

in fact it's probably best to do it only once at the start of the proof

[Mario Carneiro]

lemma MWE (M : ε_NFA α) :
  Π (S : finset M.state) (s : M.state), s ∈ M.ε_closure S ↔ M.ε_closure_set S s
| S :=
begin
  have IH := λ T (h : Tᶜ < Sᶜ), MWE T,
  intro s,
  split,
  { intro h,
    rw ε_closure at h,
    dsimp at h,
    split_ifs at h with heq,
    { sorry },
    { have hwf : (S ∪ M.step_set' S none)ᶜ < Sᶜ,
      { sorry },
      have h' : M.ε_closure_set (S ∪ M.step_set' S none) s,
        rwa ← IH (S ∪ M.step_set' S none) hwf,
      induction h' with t ht t' t d e ih,
      { sorry },
      { apply ε_closure_set.step t' t,
        { apply ih,
          rwa IH (S ∪ M.step_set' S none) hwf },
        assumption } } },
  { intro h,
    rw ε_closure,
    dsimp,
    split_ifs with heq;
    induction h with t ht t' t ht' ht ih,
    { sorry },
    { sorry },
    all_goals
    { have : (S ∪ M.step_set' S none)ᶜ < Sᶜ,
      sorry },
    { sorry },
    { rw IH (S ∪ M.step_set' S none) this,
      apply ε_closure_set.step t' t,
      rwa ←IH (S ∪ M.step_set' S none) this,
      assumption } }
end
using_well_founded {dec_tac := tactic.assumption}