idiom for using calc to rewrite the goal

Stream: lean4

[Joachim Breitner]

I am a big fan of calc proofs. If the goal is itself an equality (or other relation), I just just start with calc.

But what if I want to rewrite the goal p1 with calc p1 =… ; _ = p2 := … to get goal p2? Like in this example

example (n : Nat) (P : Nat → Prop) (h : P n): P (0 + 1 * n * 1) := by
  apply
    Eq.mpr <|
      calc
        P (0 + 1 * n * 1)
        _ = P (0 + n * 1) := (congrArg (fun x => P (0 + x * 1)) (Nat.one_mul n))
        _ = P (0 + n) := (congrArg (fun x => P (0 + x)) (Nat.mul_one n))
        _ = P n := congrArg P (Nat.zero_add n)
  exact h

Is there an even nicer idiom than apply Eq.mpr |> calc … that I can use here?

[Floris van Doorn]

I sometimes use have := calc ... and then you can do rw [this] afterwards. But that's perhaps just as cumbersome.

[Johan Commelin]

Would this be a job for convert_to + calc-block afterwards?

[Johan Commelin]

convert_to h
calc ...

[Joachim Breitner]

Context: I am prototyping a tactic that will take a proof goal as produced by simp or rw and turn it into a small-step calc block:

example (n : Nat) : 0 + n = 0 + (n * 1) := by
  calcify rw [Nat.mul_one, Nat.zero_add]
/--
info: Try this: calc
  0 + n
  _ = n := (Nat.zero_add n)
  _ = 0 + n := (Eq.symm (Nat.zero_add n))
  _ = 0 + n * 1 := congrArg (fun _a => 0 + _a) (Eq.symm (Nat.mul_one n))
-/

[Joachim Breitner]

hmm, no convert_to in Core :-)

Maybe the idiom that should work is

conv => calc …

Already I can write

example (n : Nat) (P : Nat → Prop) (h : P n): P (0 + 1 * n * 1) := by
  conv => tactic => calc
    P (0 + 1 * n * 1)
    _ = P (0 + n * 1) := (congrArg (fun x => P (0 + x * 1)) (Nat.one_mul n))
    _ = P (0 + n) := (congrArg (fun x => P (0 + x)) (Nat.mul_one n))
    _ = P n := congrArg P (Nat.zero_add n)
  exact h

but no reason not to lift calc to a conv tactic like other tactics?

[Johan Commelin]

That seems a good idea, yes

[Joachim Breitner]

Issue at https://github.com/leanprover/lean4/issues/3557

[Andrés Goens]

Joachim Breitner said:

Context: I am prototyping a tactic that will take a proof goal as produced by simp or rw and turn it into a small-step calc block:

example (n : Nat) : 0 + n = 0 + (n * 1) := by
  calcify rw [Nat.mul_one, Nat.zero_add]
/--
info: Try this: calc
  0 + n
  _ = n := (Nat.zero_add n)
  _ = 0 + n := (Eq.symm (Nat.zero_add n))
  _ = 0 + n * 1 := congrArg (fun _a => 0 + _a) (Eq.symm (Nat.mul_one n))
-/

oh, that looks really neat! would that live in core or somewhere outside (e.g. std)?

[Joachim Breitner]

Probably in my separate repo, labeled “this is an experiment”, for a while :-D

[Andrés Goens]

hehe, fair enough

[Joachim Breitner]

Although I hope it’ll be easier to use “dev dependencies”, i.e. commands that you don’t plan to commit (so they don’t need to be a dependency) and just want to add to your toolkit. then separate repo doesn’t sound too bad.

[Joachim Breitner]

Of course, if it turns out to be reliable and useful, it can be upstreamed. But it’s not on any roadmap as of now.

[Andrés Goens]

I'll be looking out for that

[Andrés Goens]

just curious, in the context of these experiments: do you think it might make sense to keep the rewrite list as passed to rw or simp in a single list and still have the declarative list of rewrites in calc? Something like (not talking about the concrete syntax here):

example (n : Nat) : 0 + n = 0 + (n * 1) := by
  calcify rw [Nat.mul_one, Nat.zero_add]
/--
info: Try this: calc'
  0 + n
  _ = n
  _ = 0 + n
  _ = 0 + n * 1 := by rw [Nat.mul_one, Nat.zero_add]
-/

[Joachim Breitner]

While I am at it: What are my options to eliminate the congrArg (fun …) wrappers around these equality proofs?

We have the ▸ macro which does most of that works, and I can write

((Nat.one_mul n).symm ▸ rfl)

instead, but that’s a mouthful. Is there some other syntax?

[Andrés Goens]

context for the question above: we prototyped something along those lines for this paper for something a bit stronger than simp and it would be nice to do something much more full-fledged from it, where the declarative calc proof is easier to read and maintain, but can still be reconstructed with automation

[Joachim Breitner]

Hmm, not sure. One good thing about calc proofs is that each step has its own proof, so that they break individually when you refactor.

If the goal is just to explain the simp, but keeping the simp, then something inspired like from says might work:

example (n : Nat) : 0 + n = 0 + (n * 1) := by
 rw [Nat.mul_one, Nat.zero_add] performs
   0 + n
    _ = n
    _ = 0 + n
    _ = 0 + n * 1

Or, turning it around, roughly your syntax. Ok, that might be useful indeed.

At this point, I wonder, is it useful to have this in the code, or would it suffice to be able to point at the proof and see it in the info view or so.

[Andrés Goens]

is your primary goal readibility or performance?

[Andrés Goens]

Joachim Breitner said:

While I am at it: What are my options to eliminate the congrArg (fun …) wrappers around these equality proofs?

We have the ▸ macro which does most of that works, and I can write

((Nat.one_mul n).symm ▸ rfl)

instead, but that’s a mouthful. Is there some other syntax?

for readibility I guess you could also just use the individual rw step here, no?

[Joachim Breitner]

Experimentation :-D

And next explanation, mostly for people wanting to learn what simp does.

[Joachim Breitner]

Yes, rw or simp only are also options. The tactic should probably check if it works and fall back to the proof term if it doesn’t. Another variant could be

          calc
            P (0 + 1 * n * 1)
            _ = P (0 + n * 1) := by congr; exact (Nat.one_mul n)
            _ = P (0 + n) := by congr; exact (Nat.mul_one n)
            _ = P n := by congr; exact (Nat.zero_add n));

(rw might fail once I do stuff underneath binders; not supported yet, but might come. Maybe simp_rw only is better.)

[Andrés Goens]

Joachim Breitner said:

Hmm, not sure. One good thing about calc proofs is that each step has its own proof, so that they break individually when you refactor.

If the goal is just to explain the simp, but keeping the simp, then something inspired like from says might work:

example (n : Nat) : 0 + n = 0 + (n * 1) := by
 rw [Nat.mul_one, Nat.zero_add] performs
   0 + n
    _ = n
    _ = 0 + n
    _ = 0 + n * 1

Or, turning it around, roughly your syntax. Ok, that might be useful indeed.

At this point, I wonder, is it useful to have this in the code, or would it suffice to be able to point at the proof and see it in the info view or so.

right, I think with rw that doesn't work as easily, but if it's simp then that would still be the case, i.e. if the same simp set is used for every individual proof in calcthen in a refactor you would still have the individual step break the same way

[Andrés Goens]

i.e. thinking of the performs as some sort of <;>instead

[Joachim Breitner]

I put my prototype on https://github.com/nomeata/lean-calcify

[Mario Carneiro]

Joachim Breitner said:

hmm, no convert_to in Core :-)

Maybe we should fix that :wink: I think it has no prerequisites; the main one that was missing originally was congr but this has since moved to core.

[Kim Morrison]

Yes, I agree convert should be moved. It is super useful for everyone.

[Kim Morrison]

If someone would like to make the PR and ping me I can merge it. If you know how to do the @[builtin_tactic] dance, great, if you don't, just note that you haven't done that in the PR description.

[Joachim Breitner]

PR for conv => calc at https://github.com/leanprover/lean4/pull/3659

[Kim Morrison]

@Joachim Breitner looks good. CI seems to have got stuck. Can you push an empty commit or similar?

[Joachim Breitner]

I have seen CI getting stuck when I create a PR with gh pr create and add a label at that time.