my first minimum proof - did I do it right?

Stream: new members

[rzeta0]

This is my attempt at writing a lean 4 proof - for the simplest problem I can think of, which is to show

$$(a = b) \land (b=c) \implies (a=c)$$

Here's my first ever lean 4 proof created from scratch (ie not adding code to a partially complete proof as per Mechanics of Proof chapter 1)

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

example {a b : ℝ} (h1 : a = b) (h2 : b = c) : a = c := by
  calc
    a = b := by rw [h1]
    _ = c := by rw[h2]

Questions:

1. Could this be simpler?
2. Is calc the right way to show $(a = b) \land (b=c) \implies (a=c)$ ?
3. The very first line a=b := by rw [h1] suggests I am substituting $b$ for $a$ in a previous line, but there isn't a previous line .. so is this bending how lean 4 should be used?
4. Deleting the line import Mathlib.Data.Real.Basic causes no apparent problems.... is it needed?

[Logan Murphy]

1. Could this be simpler?

Yep! There is nothing special about real numbers here, this is just the transitive property of = :

example {a b : ℝ} (h1 : a = b) (h2 : b = c) : a = c :=
  Eq.trans h1 h2

2. Is calc the right way to show ...

If by "right" you mean "simplest", then using Eq.trans may be simplest

On the other hand, if you still wanted a simpler tactic proof, you could do without calc via

example {a b : ℝ} (h1 : a = b) (h2 : b = c) : a = c :=
 by rw [h1,h2]

3. The very first line a=b := by rw [h1] suggests I am substituting b for a in a previous line, but there isn't a previous line .. so is this bending how lean 4 should be used?

Not at all. If you put your cursor in front of the first rw, you'll see that the goal is a = b. When you write rw [h1], it replaces the a in the goal with b, leaving you with b = b, which Lean can close. The substitution is occurring in the goal (of that line), not in any previous line.

4. Deleting the line import Mathlib.Data.Real.Basic causes no apparent problems.... is it needed?

I think the only thing needing to be imported here is real numbers ℝ. In this case, you could get it from either of those two imports. But since (I believe) Mathlib.Tactic transitively imports Mathlib.Data.Real.Basic, the latter is probably redundant.

[rzeta0]

Thanks Logan - this idea of "current goal" is helpful.

[rzeta0]

I'm still learning ..and have found an even simpler lean program. The idea is to find a suitable "first proof" with minimal code suitable for introducing lean proofs to other beginners like myself.

import Mathlib.Tactic

example {a: ℕ} (h1: a = 4) : a > 1 := by linarith

To me this seems correct, good even, but I'd welcome more experienced views perhaps explaining why this might be a bad first example.

[Damiano Testa]

I would consider True or 0 = 0 as simpler still to prove.