New conv => … equals tactic

Stream: mathlib4

[Joachim Breitner]

Advertisement New tactic landed in mathlib for your convenience!

When explaining a proof to a human on a blackboard, surely you have often underbraced some subterm, written a different, but equal term below it, explained to your audience why they are equal, and then continued the proof with the changed term?

You can now do the same when explaining a proof to lean. Have a large proof goal, and somewhere inside an expression that you’d like to replace with something else that provably equal? Write

conv => …; equals e =>
  tactics

to do so. After conv => you can use the usual conv tactics to focus the expression you care about (e.g. using left; right; left; left, or in (_ + _) to find a matching expression). Then you write the expression you want that to be equal to, and after the => an (indented) proof of the equality.

It’s a bit like using convert_to, but without having to repeat all the context of the expression you want to change.

It's also related to the rw conv tactic, which you would use if you know the lemma to rewrite with and don't want to type in the new term. Afterequals, in contrast, the subgoal is fully known, so a good start for closing tactics like ring or simp etc.

The tactic was added to std4 in std4#204.
Mathlib docs PR at mathlib4#6747

[Scott Morrison]

Very helpful thank you, I have wanted exactly this in the past!

[Kyle Miller]

Joachim Breitner said:

It’s a bit like using convert_to, but without having to repeat all the context of the expression you want to change.

In particular, convert_to e; tactics... is like doing conv => equals e => congr!; tactics...

[Kyle Miller]

(Re the self-note, those are the mathlib3 docs. I think you mean https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html)

[Joachim Breitner]

Ah, right. Sometimes google sends me the wrong way. Maybe the mathlib3 docs could use a banner on top saying warning that one is looking at old stuff?

[Filippo A. E. Nuccio]

Joachim Breitner said:

Advertisement New tactic landed in mathlib for your convenience!

When explaining a proof to a human on a blackboard, surely you have often underbraced some subterm, written a different, but equal term below it, explained to your audience why they are equal, and then continued the proof with the changed term?

You can now do the same when explaining a proof to lean. Have a large proof goal, and somewhere inside an expression that you’d like to replace with something else that provably equal? Write

conv => …; equals e =>
  tactics

to do so. After conv => you can use the usual conv tactics to focus the expression you care about (e.g. using left; right; left; left, or in (_ + _) to find a matching expression). Then you write the expression you want that to be equal to, and after the => an (indented) proof of the equality.

It’s a bit like using convert_to, but without having to repeat all the context of the expression you want to change.

It's also related to the rw conv tactic, which you would use if you know the lemma to rewrite with and don't want to type in the new term. Afterequals, in contrast, the subgoal is fully known, so a good start for closing tactics like ring or simp etc.

The tactic was added to std4 in std4#204.
Mathlib docs PR at mathlib4#6747

Can you provide a small mwe, perhaps also in the docs?

[Joachim Breitner]

My creativity so far failed to come up with something small, but plausible and convincing. Once I have an idea (or someone else provides a nice example), sure!

[Kyle Miller]

@Filippo A. E. Nuccio The tactic at least has an example in its docstring:

example (P : (Nat → Nat) → Prop) : P (fun n ↦ n - n) := by
  conv in (_ - _) => equals 0 =>
    -- current goal: ⊢ n - n = 0
    apply Nat.sub_self
  -- current goal: P (fun n => 0)

[Mario Carneiro]

there is also a test file: https://github.com/leanprover/std4/blob/main/test/conv_equals.lean

[Joachim Breitner]

Maybe the list of tactics in https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html should all include links to the corresponding tactic’s docstring, i.e. to https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/Basic.html#Std.Tactic.Conv.equals

[Kyle Miller]

If you put Std.Tactic.Conv.equals into the Conv.Guide docs then it should auto-link. It's resilient against future refactorings unfortunately though

[Joachim Breitner]

Can I link to it while controlling the link text? Users shouldn’t have to see that module prefix.
(Also the rfl tactic links to Prelude.rfl…)

[Kyle Miller]

I wish there were different syntax classes for the docs, so for example tactic`exact foo` might be how you keep the linkifier from trying to turn all the identifiers into links

[Kyle Miller]

I don't know of a way to control the text for an link to an identifier, short of giving a full URL...