Zulip Chat Archive

Stream: general

Topic: equation compiler failing


Sky Wilshaw (Jun 25 2022 at 17:35):

The equation compiler keeps on giving me the same error message:

equation compiler failed to create auxiliary declaration 'f_map_core._main._pack'
nested exception message:
infer type failed, unknown variable
  H

This error happens in a variety of cases, and I can't find a good minimal example. In the simplest case, I have a hypothesis hy which exactly matches the goal, and replacing a sorry with exact hy causes this error to be emitted. Does anyone know some general tips for helping the equation compiler understand what I've written?

Mario Carneiro (Jun 25 2022 at 17:51):

this needs a #mwe

Mario Carneiro (Jun 25 2022 at 17:52):

it might have something to do with mutual recursion, it is difficult to understand what is happening without an example

Sky Wilshaw (Jun 25 2022 at 17:53):

Yeah, unfortunately whenever I try to minify my example the problem goes away - the strange thing is that I never use the variable H at all so it must be internal to the equation compiler

Mario Carneiro (Jun 25 2022 at 18:06):

then minify everything else?

Sky Wilshaw (Jun 25 2022 at 18:28):

Thanks for your help, the issue's fixed now. It turns out that the equation compiler was also failing due to issues related to a well-founded relation - I thought the errors were independent but after solving the latter, the former went away.

Mario Carneiro (Jun 25 2022 at 18:45):

I still would like to see an example, because it sounds like a bug

Sky Wilshaw (Jun 25 2022 at 18:53):

noncomputable def test :   
| x := have this : {i :  |  y (hyx : y < x), have y < x, from hyx, test y  i}.nonempty, begin
    by_contradiction,
    have hfinite : {i :  |  y < x, have y < x := _›, test y = i}.finite := sorry,
    rw  cardinal.lt_aleph_0_iff_finite at hfinite,
    have : ℵ₀ = #{i :  |  y < x, have y < x := _›, test y = i}
      + #{i :  |  y < x, have y < x := _›, test y  i},
    { rw  cardinal.mk_nat,
      rw  cardinal.mk_univ,
      rw  cardinal.mk_union_of_disjoint,
      congr',
      rw set.union_def,
      refine (set.eq_univ_of_forall (λ z, _)).symm,
      dsimp,
      by_cases  (y : ) (H : y < x), test y = z,
      { left, exact h },
      { right, push_neg at h, exact h },
      sorry },
    rw set.not_nonempty_iff_eq_empty at h,
    rw h at this,
    simp at this, rw this at hfinite,
    simp at hfinite, exact hfinite
  end, this.some

This has an incorrect proof that recursive applications are decreasing - the important thing is that the first error emitted by lean is the equation compiler one.

Sky Wilshaw (Jun 25 2022 at 18:53):

It can probably still be reduced, but I don't have time for that right now

Mario Carneiro (Jun 25 2022 at 20:29):

what are the imports?

Sky Wilshaw (Jun 25 2022 at 20:33):

I think

import data.set.basic
import set_theory.cardinal.basic

open_locale cardinal

should suffice


Last updated: Dec 20 2023 at 11:08 UTC