(Relations MoP ch9) example proofs feel unsatisfactory

Stream: new members

[rzeta0]

MoP Chapter 9 is on Relations and begins with some simple examples including:

import Mathlib.Tactic

example : Reflexive ((·:ℝ) = ·) := by
  dsimp [Reflexive]
  intro x
  ring

The goal state just before ring is

x : ℝ
⊢ x = x

It feels unsatisfactory the property we're trying to prove is not actually proved in this proof, but is done by ring. Question: Is this cheating?

---

Here is another example:

import Mathlib.Tactic

example : Symmetric ((·:ℝ) = ·) := by
  dsimp [Symmetric]
  intro x y h
  rw [h]

Here the goal state just before rw is

x y : ℝ
h : x = y
⊢ y = x

So here rw is rewriting the x in y=x as y to leave y=y which is (I guess?) true. But I'm not sure we've actually proven that x=y implies y=x.

Question: Am I the only one who feels there's something funny going on here?

The same applies to the remaining two mini examples in MoP 10.1.2

[Matt Diamond]

Using ring in the first example isn't suspicious, though IMHO it's overkill. Consider that it can also be proved like this:

import Mathlib.Tactic

example : Reflexive ((·:ℝ) = ·) := by
  dsimp [Reflexive]
  intro x
  exact Eq.refl x

All we're doing is constructing a term of the type x = x using the constructor docs#Eq.refl with a suitable argument (x). Put another way, the Prop x = x can be proved (constructed) whenever you have a term x because that's all the constructor needs... there's no need for an additional fact to help us out.

[Aaron Liu]

What you have in the Symmetric example is almost exactly how I would write the proof, and is also almost exactly how it is done in docs#Eq.symm.

[rzeta0]

thanks @Matt Diamond

This is all beyond my capability but I'll give it a go.

Are we saying that the term x is a proof of Prop x=x because of the definition of =, and we're using one of the constructors of the definition of = to resolve the goal.

Have I got it right?

[Matt Diamond]

to be clear, I'm not saying the term x is a proof of Prop x=x... I'm saying that Eq.refl x is a proof of Prop x=x

[Matt Diamond]

similar to the way that Nonempty.intro 3 is a proof of Nonempty ℕ

[Matt Diamond]

or in the way that Nat.succ 0 is a term of type ℕ... remember that a proof is just a term of a specific Prop, and when you write Nat.succ 0 you're just using the Nat.succ constructor to create a term of ℕ, much like you use the Eq.refl constructor to create a term of x = x (for some x)

[Eric Paul]

As some more info, the symbol = is defined in Lean and is not builtin. It's a type like any other which has specific ways of constructing elements for it.

In Lean, = is notation for the type Eq and you can see its definition here. So writing x = x is the same as writing Eq x x.

The way that Eq is defined, there is only one way to create elements of it. For any term a of type α, the constructor Eq.refl a is an element of type Eq a a (aka a = a).

[rzeta0]

Thanks again Matt and Eric and Aaron - this is helpful.

And thanks or your patience, I am a bit slow with learning this.