# Zulip Chat Archive

## Stream: new members

### Topic: zero_max a rfl lemma

#### Lucas Allen (Oct 23 2019 at 03:30):

Hello,

I was messing around with `suggest`

just now and I found that `zero_max`

in `data.nat.basic`

can be proved by `rfl`

, i.e. the following code works for me:

lemma zero_max {m : nat} : max 0 m = m := rfl

But the proof of this lemma in my version of mathlib is

lemma zero_max {m : nat} : max 0 m = m := max_eq_right (zero_le _)

Should this be changed?

#### Kenny Lau (Oct 23 2019 at 03:34):

yes

#### Mario Carneiro (Oct 23 2019 at 03:49):

no

#### Mario Carneiro (Oct 23 2019 at 03:52):

refl proofs are more brittle. This adds an unneeded dependence on the fact that the decidable instance of `0 <= m`

reduces to true, as well as the fact that the definition of `max a b`

is `if a <= b then b else a`

instead of `if b <= a then a else b`

#### Mario Carneiro (Oct 23 2019 at 03:52):

the given proof is insensitive to such details

#### Lucas Allen (Oct 23 2019 at 21:49):

Oh... so `rfl`

isn't always the best possible proof? That's really weird.

#### Mario Carneiro (Oct 23 2019 at 22:10):

another example of a theorem that can be proven by rfl but really shouldn't is `100 * 100 = 10000`

#### Wojciech Nawrocki (Oct 23 2019 at 22:42):

Is the reason that tactics can use binary reprs while kernel does unary, or something else?

#### Mario Carneiro (Oct 23 2019 at 23:02):

yes

#### Mario Carneiro (Oct 23 2019 at 23:03):

the kernel is forced to use the definition of `nat`

, which is unary and horrible for computation

#### Scott Morrison (Oct 24 2019 at 01:30):

I'm starting to come around to the idea that `rfl`

is the worst possible proof. It's the ultimate "Mathematician A: the proof is obvious. Mathematician B [several hours later]: yes, it is obvious."

#### Scott Morrison (Oct 24 2019 at 01:31):

It says: well, if you go an unfold definitions, possibly all the way down to the beginnings, you will eventually see that these two things really are the same thing. No one likes to do that, and quite reasonably the kernel sometimes does a terrible job at it.

#### Wojciech Nawrocki (Oct 24 2019 at 16:14):

I'm not convinced this is true in general. One can construct efficient decision procedures, in which case a proof by `rfl`

does not have to carry out a long computation.

#### Mario Carneiro (Oct 24 2019 at 17:23):

There are proofs where `rfl`

is the appropriate way to prove it. `dec_trivial`

is like this, in that you are expected to be able to reduce a term of type `decidable p`

to one of its constructors

#### Mario Carneiro (Oct 24 2019 at 17:23):

that doesn't mean it's the fastest proof though

#### Mario Carneiro (Oct 24 2019 at 17:25):

kernel reductions are constrained by a certain approach to the problem that relies on the definition of the inductive types. You have to really write things carefully if you want kernel reduction to not suck. Even using the equation compiler isn't a great idea because it generates huge terms that slow down reduction

#### Lucas Allen (Oct 25 2019 at 21:50):

Is there a way to prove `100*100 = 10000`

using binary instead of unary?

#### Mario Carneiro (Oct 25 2019 at 22:03):

`by norm_num`

Last updated: May 14 2021 at 06:16 UTC