tactic 'cases' failed nested error

Stream: lean4

[David Renshaw]

I'm struggling to understand why the baz proof does not work here:

import Mathlib.Tactic.CasesM

-- This works:
theorem foo {p q r : Prop} (h : p ∧ q ∨ p ∧ r) : p ∧ p :=
by cases h
   · casesm (_ ∧ _)
     constructor <;> assumption
   · casesm (_ ∧ _)
     constructor <;> assumption


variable {p q r : Prop}
variable (h : p ∧ q ∨ p ∧ r)

-- This works too:
theorem bar : p ∧ p :=
by cases h with
   | inl h1 => cases h1
               constructor <;> assumption
   | inr h2 => cases h2
               constructor <;> assumption


-- This does not work:
theorem baz : p ∧ p :=
by cases h
   · casesm (_ ∧ _)
     -- tactic 'cases' failed, nested error:
     -- failed to revert baz, it is an auxiliary declaration created to represent recursive definitions
   · casesm (_ ∧ _)
     -- tactic 'cases' failed, nested error:
     -- failed to revert baz, it is an auxiliary declaration created to represent recursive definitions

[David Renshaw]

Like, is this a bug in casesm, or a bug in Lean 4 core, or I am doing something wrong?

[Sebastian Ullrich]

Looks like a missing isAuxDecl check in casesm

[David Renshaw]

what should happen if ldecl.isAuxDecl is true?

[Sebastian Ullrich]

It should not try to match that hypothesis as it is merely an internal helper

[David Renshaw]

The context at the casesm call is

case inl
p q r : Prop
h : p ∧ q
⊢ p ∧ p

[David Renshaw]

where that h is italic

[David Renshaw]

I'm guessing it considers that h to be auxiliary? It was generated by the preceding cases h line.

[David Renshaw]

I don't want to ignore that h, because it's exactly what I need to proceed with the proof.

[Sebastian Ullrich]

No, the auxiliary decl is baz itself for use in recursion. Which I assume you don't want to case on.

[David Renshaw]

yep, that seems to fix it. Thanks!

[David Renshaw]

I'll submit a PR to fix this in mathlib4.

[David Renshaw]

https://github.com/leanprover-community/mathlib4/pull/991