conv tactic sometimes solves goal

Stream: new members

[Tobias Grosser]

I have a use of the pattern conv in (\Gamma { val := (_ : Nat), property := _ }) => skip;to identify if pattern arises. The only behavior is expect that the tactic does nothing if the pattern exists and fails if the pattern does not exist. However, for some simple pattern the tactic also solves the proof-state which is undesirable to me. Does anyone have an idea how to avoid this?

The reason I use this tactic is that I try to guard a call to generalize \Gamma { val := _, property := _ } = e; which does not fail in case the pattern cannot be matched, but instead just introduces a new meta variable. An alternative solution for me would be something that makes generalize fail if a pattern cannot be found.

[Kyle Miller]

Right now, conv tries rfl, but in the next release of Lean, @Joachim Breitner made it so that conv will use just reducible rfl (lean4#3763). That's not a complete solution to your problem. I wonder if conv should have a flag or variant that doesn't try rfl at all, like how there's rw and rewrite.

[Tobias Grosser]

I would be in favor of such a flag, indeed.

[Tobias Grosser]

Would you like me to open a PR?

[Tobias Grosser]

Or even submit a patch?

[Kyle Miller]

Maybe it would be best to create a bug issue saying how you use conv for pattern matching purposes, with a #mwe of what you want to do.

I'm not sure whether it's best to modify conv, or to extract the pattern matching capabilities into a separate tactic. Or maybe generalize could have a variant that fails.

[Joachim Breitner]

Don't we have a guard_goal tactic or similar that asserts that a state has a certain shape? Maybe that would be the natural thing to extend to “assert that some subexpression of the goal matches this patterns”?

[Tobias Grosser]

https://github.com/leanprover/lean4/issues/3889

[Damiano Testa]

I have not really tested what is below, but you can try if this works for you:

import Lean.Meta.KAbstract
import Lean.Elab.Tactic.ElabTerm

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

[Tobias Grosser]

unknown identifier 'kabstract'

AliveAutoGenerated.lean:3172:23

unknown identifier 'elabTerm'

AliveAutoGenerated.lean:3172:54

unknown identifier 'logInfo'
?

[Tobias Grosser]

I guess I miss an include.

[Tobias Grosser]

import

[Damiano Testa]

I made what is above a #mwe, sorry!

[Tobias Grosser]

This works. How can I change contains? to fail if the pattern is not found.

[Damiano Testa]

throwError instead of logWarning.

[Damiano Testa]

(I edited the code above with the error)

[Tobias Grosser]

Perfect. Thank you so much.

[Damiano Testa]

kabstract is what rw uses, if I remember correctly: it should be very robust.

[Kyle Miller]

kabstract is also what generalize uses

[Tobias Grosser]

Right.

[Tobias Grosser]

I think this is the right direction. I am currently trying to integrate this into our actual code and it seems to be a bit more fragile than I hoped.

[Tobias Grosser]

Let me play around with it for a moment and see if I can get a handle of it.

[Tobias Grosser]

I am afraid in my setting, the new contains? is still fragile:

     -- aa : Valuation [Ty.int]
     -- ⊢ aa { val := 0, property := ⋯ } + BitVec.ofInt 32 0 = aa { val := 0, property := ⋯ }
      conv in (aa (_ : Var ..)) => skip -- does not throw an error as it matches
      contains? (aa (_ : Var ..)) -- unknown identifier 'aa', pattern not found

[Tobias Grosser]

I am particularly surprised by the unknown identifier 'aa'.

[Tobias Grosser]

I am unsure how to extract a #mwe here.

[Tobias Grosser]

If someone wants to try, our code is here: https://github.com/opencompl/ssa/pull/224

[Damiano Testa]

This also does not work:

example : ∀ a, a + 0 = 0 := by
  contains? _ + 0 = 0

[Tobias Grosser]

Interesting.

[Damiano Testa]

The example that I wrote may be related to the fact that rw does not enter much into binders. Yours seems to be pointing to a missing withContext, but honestly I do not see where that would go...

[Tobias Grosser]

For your example, generalize also does not work.

[Tobias Grosser]

example : ∀ a, a + 0 = 0 := by
  generalize (_ + 0) = x
  -- x : ℕ
  -- ⊢ ∀ (a : ℕ), a + 0 = 0

[Tobias Grosser]

Meaning, it does not match but introduces this funny unconstrained variable.

[Tobias Grosser]

So contains? not matching here either is acceptable for me.

[Kyle Miller]

(Untested) It seems to be missing withMainContext

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

[Damiano Testa]

I tried that, but it does not fix my example. However, my example might be expected (but undesired) behaviour.

[Damiano Testa]

Anyway, see if Kyle's suggestion works for you (I probably won't be at a computer for a while).

[Tobias Grosser]

Kyle Miller said:

(Untested) It seems to be missing withMainContext

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

This works for me and does exactly what I need.

[Tobias Grosser]

Thank you @Kyle Miller