fin_cases gives (kernel) declaration has metavariables

Stream: mathlib4

[Luis Berlioz]

The following code gives a (kernel) declaration has metavariables 'cc' messages:

 import Mathlib

theorem cc : {x ∈ Finset.range 5 | IsSquare x} = {0, 1, 4} := by
  ext k
  apply Iff.intro
  · intro hk
    fin_cases hk
    simp
  · intro hk
    fin_cases hk
    repeat simp
    use 2

Sorry if this is repeated topic. How to prove this result while avoiding this type of messages?

[Bhavik Mehta]

If you use a version of Lean before v4.19.0-rc1, this works:

import Mathlib

theorem cc : {x ∈ Finset.range 5 | IsSquare x} = {0, 1, 4} := by
  decide +kernel

[Bhavik Mehta]

For instance, on v4.18.0, this works: https://live.lean-lang.org/#project=mathlib-stable&codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQO0Cm0BIcAxmXAFxwDeAHnIBBEcAYsAHYDOBMAdFCQcA5gTgBWOAB84ASS4BlAI4BXJFDH0AvnAC8dAAwAaOAEYTAFh1V9WAJ444cACYEywV3ADUAawJQOAnQcIA

[Kevin Buzzard]

Wooah was this breakage in 4.19rc intentional?

[Kim Morrison]

I would guess this is a consequence of making well-founded proofs opaque, so the kernel can't reduce them (which very often goes badly wrong).

See lean#5182, which advises adding @[semireducible] (although I think it is often not obvious where).

@Joachim Breitner is on holiday at the moment this week.

[Kevin Buzzard]

I guess this is an independent issue to the broken proof above

[Patrick Massot]

Yes, it is. The broken proof starting this thread is clearly a bug in fin_cases.

[Patrick Massot]

This error message means some tactic dropped some goals. You can get the same message with

elab "bad_tactic" : tactic => do
  Lean.Elab.Tactic.replaceMainGoal []

theorem cc : {x ∈ Finset.range 5 | IsSquare x} = {0, 1, 4} := by
  ext k
  apply Iff.intro
  · intro hk
    bad_tactic
  · intro hk
    bad_tactic

[Patrick Massot]

And in the original proof you can see how fin_cases creates only one goal.

[Patrick Massot]

You can avoid the fin_cases failure while keeping the same spirit with

theorem cc : {x ∈ Finset.range 5 | IsSquare x} = {0, 1, 4} := by
  ext k
  rw [Finset.mem_filter]
  apply Iff.intro
  · intro hk
    rcases hk with ⟨hk, hk'⟩
    fin_cases hk
    all_goals sorry
  · intro hk
    fin_cases hk
    all_goals simp
    use 2

[Bhavik Mehta]

Yes, it's independent of the issue above but still answers the question of how to prove the result without errors. The semireducible fix in this case is a change to batteries: https://github.com/leanprover-community/batteries/pull/1194#issuecomment-2782006920. But decide+kernel should ignore reducibility settings, so it still feels like something else has gone wrong.