Zulip Chat Archive

Stream: new members

Topic: Confusing recursion error message


view this post on Zulip Fox Thomson (Oct 18 2020 at 16:07):

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.

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2020 at 16:11):

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).

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:13):

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

view this post on Zulip Fox Thomson (Oct 18 2020 at 16:13):

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:13):

you have to put them in the same term

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:14):

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:16):

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}

Last updated: May 11 2021 at 22:14 UTC