generalize not failing when match fails

tobiasgrosser commented 5 months ago

Prerequisites

[x] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

I am trying to write a tactic that generalizes patterns in a program. My tactic calls generalize_or_fail in repeat until all occurrences of the pattern are generalized. I cannot just use generalize as it does not fail, but just keeps creating meta-variables in case the match pattern cannot be found. I managed to create a workaround, as shown below. However, this workaround is also not working for us as conv seems to solve goals by reflection, as visible in test_solved_but_should_not. In this specific case, this leads to generalize failing, which I can work around with try. While this resolves the error it leads to a solved goal state while I just wanted to generalize. In our framework, I would much prefer if our tactic does not start solving the goal.

local macro "generalize_or_fail" : tactic =>
  `(tactic|
   (
       conv in ((_ : ℕ) + (_ : ℕ)) => skip
       generalize h : ((_ : ℕ) + (_ : ℕ)) = c
    )
  )

def test_succeed (a b c : ℕ): a + b + c = c + (a + b) := by
  generalize_or_fail
  -- a b c c✝ : ℕ
  -- h✝ : a + b + c = c✝
  -- ⊢ c✝ = c + (a + b)
  sorry

def test_fail (a b c : ℕ): a * b * c = c * (a * b) := by
  generalize_or_fail
  -- 'pattern' conv tactic failed, pattern was not found
  -- fun x_0 x_1 => x_0 + x_1
  sorry

def test_solved_but_should_not (a b c : ℕ): a + b = a + b := by
  generalize_or_fail
  -- no goals to be solved

Steps to Reproduce

Run the code above.

Expected behavior:

generalize should fail if it cannot match a pattern or
conv should not simplify by refl
Actual behavior:
generalize introduces a new meta-variable even if no pattern is found
conv simplifies by reflection

Versions

"4.7.0"

tobiasgrosser commented 5 months ago

There is a corresponding zulip thread where we investigate this further: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/conv.20tactic.20sometimes.20solves.20goal/near/432918099

tobiasgrosser commented 5 months ago

I meanwhile use the following tactic:

elab "contains? " ts:term : tactic => withMainContext do
  let tgt ← getMainTarget
  if (← kabstract tgt (← elabTerm ts none)) == tgt then throwError "pattern not found"

which does what I need. Thanks goes to Kyle Miller.

I am happy for this to be closed, but also wanted to record this in case someone feels these issues should be addressed within lean core.

semorrison commented 5 months ago

I agree generalize should fail if the pattern doesn't match. If someone would like to PR a fix, that would be welcome.

leanprover / lean4