Applying a lemma up to commutativity

Stream: general

[Harry Goldstein]

Hi all, I'm working on some proof automation, and I'd like a straightforward way to apply a lemma up to some commutativity laws. For example, in the example below I'd like to prove something about a proposition containing 3 = x but I have a hypothesis talking about x = 3:

example
    {P : Prop}
    {Q : Prop → Prop}
    (h1 : Q (P ∧ x = 3)) :
    Q (P ∧ 3 = x) := by
  apply h1 -- Fails

If I was doing the proof manually, I'd use conv to drill into the goal and rewrite the equation with Eq.comm:

example
    {P : Prop}
    {Q : Prop → Prop}
    (h1 : Q (P ∧ x = 3)) :
    Q (P ∧ 3 = x) := by
  conv in _ = _ => rw [Eq.comm]
  apply h1

Is there a way to do this with automation? I'd like to have a tactic like

apply_up_to [Eq.comm] h1

that just tries to apply Eq.comm during unification.

[Zhang Qinchuan]

For you example, you can use convert:

import Mathlib

example
    {P : Prop}
    {Q : Prop → Prop}
    (h1 : Q (P ∧ x = 3)) :
    Q (P ∧ 3 = x) := by
  convert h1 using 2
  rw [eq_comm]

[Ruben Van de Velde]

Or maybe simpa [eq_comm], or aesop. But I'm not sure how any of these would work with your use case

[Harry Goldstein]

Oh interesting! I need to play around with convert a bit. The using 2 is telling it to select the righthand side of the ∧ right? Ideally I don't want to have to specify what to rewrite at that level of granularity.

I guess I oversimplified my example a bit, because as you mentioned simpa [eq_comm] does work for the toy example but not the more realistic version:

example
    {f : α → Nat → Prop}
    (h : (x : Nat) → {s // ∀ v, f s v ↔ v = x}) :
    {s // ∀ v, f s v ↔ 2 = v} := by
  conv in _ = _ => rw [eq_comm]
  apply h

I'm happy to use aesop, I just don't know how to tell it to do the rewriting under all of the constructors.

[Eric Wieser]

In this example you are constructing data so you probably should not be using a tactic in the first place

[Harry Goldstein]

Hmm. I realize that I'm bending this automation a bit beyond what it's usually used for, but as far as I can tell there's no reason this couldn't work in principle. In a dependent type theory there isn't a huge gap between proofs and data, after all.

I'm sure there's a way to formulate my question fully within Prop — plenty of proofs rely on applying lemmas up to some administrative rewriting, and it's natural to ask how to automate that kind of reasoning.

[Harry Goldstein]

Unless you're suggesting that there are better tools within Lean to automatically build up data alongside a proof about that data?

[Eric Wieser]

It works fine in principle; but in practice, you never care what proof you found, but you almost always care about what data you produced. So using tactics makes it much easier to generate the "wrong" data by accident.

[Eric Wieser]

Here you could use := Subtype.map id (by sorry) (h 2), where you can restrict your tactic use to where the sorry is

[Harry Goldstein]

In my use case, I really am just looking for any program that satisfies the specification. I’d be happy to share more details with you privately if you want (this is active research, so I don’t feel comfortable talking about all of the details publicly yet), but those details aren’t necessarily relevant to the original question

[Eric Wieser]

If that's the case then indeed tactics are ok for you to use; but it's not the typical use case, so things will be less polished than usual

[Harry Goldstein]

Yes, totally understood. And I’m happy to write my own tactics if necessary. I was just asking to see if things are already implemented

[Daniel Weber]

Using Mathlib you can use simp_rw if you don't care about what data you produce (simp_rw [eq_comm]; apply h). You can also use convert, like convert h _ using 4; rw [eq_comm]

[Harry Goldstein]

Oh that seems useful too! Ok, I bet I can cook something up with a combination of simp_rw and convert. I still really want something that explicitly tries to use the rewrite lemma while applying the target hypothesis, but it seems like that might just not exist yet