what does Eq.trans apply to?

Stream: new members

[Shanghe Chen]

In the example of https://leanprover.github.io/theorem_proving_in_lean4/tactics.html, there is an example:

example : ∀ a b c : Nat, a = b → a = c → c = b := by
  intros
  apply Eq.trans
  apply Eq.symm
  assumption
  assumption

I don't quite understand what Eq.trans apply to, and why it follows with a Eq.symm, rather than an assumption?

[Notification Bot]

This topic was moved here from #general > what does Eq.trans apply to? by Yury G. Kudryashov.

[Yury G. Kudryashov]

@Coriver Chen I moved this question to the #new members stream. Did you try this example in an environment that shows current goals?

[Shanghe Chen]

Yeah thank you. I tried a wrong version of it

[Shanghe Chen]

E9BB532E-95C3-4DD3-B72C-2532DE64771A.jpg

[Yury G. Kudryashov]

apply Eq.trans should generate 3 goals:

• c = ?a
• ?a = b
• Nat,

where the last goal is an unknown intermediate number.

[Yury G. Kudryashov]

apply Eq.symm turns c = ?a into ?a = c, and we have an assumption of this form.

[Yury G. Kudryashov]

Once you call assumption, Lean figures out that ?a is a, and you have to prove a = b, which is done by the second assumption.

[Yury G. Kudryashov]

That's exactly what happens on your screenshot (though you renamed variables)

[Yury G. Kudryashov]

Lean tries to find an assumption b = ?b (here ?b is a placeholder for a number it doesn't know yet) and fails because the relevant assumption is a = b, not b = a.

[Shanghe Chen]

Thank you I think I get it now

[Shanghe Chen]

Let me debug into the corect example step by step. Hence the applied tactic is applied to the goals? It turns the original goals into new one. And when I read the proof, I should read it from the bottom to the top?

[Yury G. Kudryashov]

When you write apply, then it uses backward reasoning, yes.

[Yury G. Kudryashov]

Quite often we write proofs using a combination of backward and forward reasoning, mixing haves, applys etc

[Yury G. Kudryashov]

Also, the most readable way to write this proof is

  intro a b c hab hac
  calc
    c = a := hac.symm
    _ = b := hab

[Shanghe Chen]

Thank you for the detailed explanation and additional examples

[Yury G. Kudryashov]

But mathlib code is not always optimized for readability, so I would write this as hac.symm.trans hab in Mathlib.

[Kevin Buzzard]

In fact one could even argue that most of the time mathlib code is optimised for unreadability, with the principle being "if the lemma is obvious, then nobody wants to read the proof so let's make it as compact as possible".