Define RHS in conv mode

Stream: mathlib4

[Joachim Breitner]

(Sorry for wrong stream, guess conv is actually a lean feature, not a mathlib feature)
Given a goal a * b, I find myself wanting for a concise way of specifying the position of b (without repeating it), saying that I want to prove it to be equal to c, then doing the proof of b = c, and end up with a = c. Of course the terms can be larger and more deeply nested, possibly in binders.
I can do

conv => right; tactic => { show (_ = c)); proof_of_b_eq_c

and conv is certainly nice for navigating there. Is there a better way of than tactic => show (_ = c); …?

If not, would a command like this be a useful addition to conv? Maybe

conv => right; equals c by
  proof_of_b_eq_c

[Joachim Breitner]

This works!

syntax (name := equals) "equals" term "by" tacticSeq : conv
macro_rules
  | `(conv|equals $rhs:term by $t:tacticSeq) => `(conv|tactic => show (_ = $rhs); . $t )

The only annoying thing left is that after the by the goal is not yet updated; I have to type skip or something like that. Is that fixable?
Probably not, this is already a problem with tactic by ….

[Joachim Breitner]

With tacticSeqIndentGt instead of tacticSeq, i.e.,

syntax (name := equals) "equals" term "by" tacticSeqIndentGt : conv

I do get the goal immediately after by, but it means I have to indent the tactic at least this far:

  conv => left; ext k; equals r ^ (n+1) * ((↑n + 1) * r^k + k * r ^ k) by
            ring

Maybe ok, although I would like to be able two write

  conv => left; ext k; equals r ^ (n+1) * ((↑n + 1) * r^k + k * r ^ k) by
    ring

[Mario Carneiro]

that's not really approved style, you shouldn't hang a by after a one-line conv block because it's not one-line anymore

[Mario Carneiro]

prefer

  conv =>
    left; ext k
    equals r ^ (n+1) * ((↑n + 1) * r^k + k * r ^ k) by
      ring

[Joachim Breitner]

I see, thanks! In that style I can even use tacticSeqIdentGt and get the right goal state, which is good.

So maybe if I don't want to get rid of the single-line aesthetics, I should write a macro that takes the convSeq as well…

[Joachim Breitner]

I’m trying

syntax (name := cchange)
  "cchange" Lean.Parser.Tactic.Conv.convSeq " with " term " => " tacticSeq: tactic
macro_rules
  | `(tactic|cchange $conv:convSeq with $rhs:term => $t:tacticSeq) =>
    `(tactic|conv => { $conv; tactic => { show (_ = $rhs); . $t}; done } )

but lean doesn’t like that: $conv is a convSeq, but it expects a conv at this point.
Is there a way to append two convSeq (the one given by the user, and the tactic… ; done) in such rules?

[Kyle Miller]

You can do ($conv) instead of $conv to turn the sequence into a single conv.

[Kyle Miller]

Parentheses can be used for both tactic and conv sequences

[Peter Pfaffelhuber]

(deleted)

[Joachim Breitner]

Thanks! I think tried that, cargo-culting it from somewhere else, but then something else didn’t work… let me have a look again.

With

syntax (name := cchange)
  "cchange" Lean.Parser.Tactic.Conv.convSeq " with " term " => " tacticSeq: tactic
macro_rules
  | `(tactic|cchange $conv:convSeq with $rhs:term => $t:tacticSeq) =>
    `(tactic|conv => { ($conv); tactic => { show (_ = $rhs); ($t)}; done } )

example : 1 = 2 + 3 := by
  cchange { right; right } with 4 => { sorry }

I get “no goals to be solved” where the sorry is.

(This isn’t super important, I am just playing around with the goal of understanding the machinery better.)

[Kyle Miller]

Watch out, { right; right } means (right; right; try rfl) here. Curly braces focus on the first goal and then try rfl at the end to auto-close.

[Kyle Miller]

You can do cchange right; right with 4 => { } or cchange (right; right) with 4 => { } to mean what you expect

[Joachim Breitner]

Ah, indeed, and it’s even prettier. Thanks!
Based on

syntax convSeq := convSeqBracketed <|> convSeq1Indented

I was somehow expecting to have to use brackets or indentation there.

[Joachim Breitner]

Is there a nice trick to make a multi-argument macro work nicely even if it is typed partiall? For example, so that after

cchange right;

I see the conv state, even before I write with and by?

This comes close, not sure if that’s the way to go, though.

syntax (name := cchange)
  "cchange" Lean.Parser.Tactic.Conv.convSeq (" with " (term (" by " tacticSeq)?)?)? : tactic
macro_rules
  | `(tactic|cchange $conv:convSeq with $rhs:term by $t:tacticSeq) =>
    `(tactic|conv => { ($conv); tactic => { show (_ = $rhs); ($t)}; done } )
  | `(tactic|cchange $conv:convSeq with $rhs:term ) =>
    `(tactic|conv => { ($conv); tactic => { show (_ = $rhs) }; done } )
  | `(tactic|cchange $conv:convSeq with) =>
    `(tactic|conv => $conv )
  | `(tactic|cchange $conv:convSeq) =>
    `(tactic|conv => $conv )

[Sebastian Ullrich]

I don't think that's something we've tackled so far. Most of our tactics have an independent meaning without the suffixes

[Joachim Breitner]

Fair. Smaller composable tactics are nicer anyways, so I'll stick to equals maybe

[Kyle Miller]

I like this equals tactic idea. I wonder if the syntax could be equals term => tacticSeq to better match tactic

Maybe this could go into Std.Tactic.Basic?

[Joachim Breitner]

I think I went back and forth between by and => half a dozen times yesterday :-)
I lean towards by, because that’s familiar as “opens a block of tactics to prove something”. I find it odd that tactic doesn’t use it, but maybe because it doesn’t always close a goal?

If you think that this is useful I’ll happily PR it into Std.Tactic.Basicor where.

I think it is a very natural way of interactive proving. Stare at the goal, notice a subexpression where you can make progress, focus, say what you want to rewrite it to, prove the rewriting, all with DRY.
It’s basically the less pretty; less verbose style version of a nice calc proof, without the repetition and the := by congr 3; … before the actual proof steps.
Or the equivalent of the pen-and-paper style of putting curly braces under some subexpression to state that it’s equal to something else.

I found it useful in a lemma dealing with series. If I try to do it with cacl and ∑' _ = _, then I have all the Summable side conditions, and have to show some transformations twice. But if I state the result using HasSum _ _ the summability is part of the goal, and I can use this tactic to freely shuffle things under the sum, or in the value of the sum, without dealing with side conditions.

[Joachim Breitner]

PR at https://github.com/leanprover/std4/pull/204, happy to refine there