## 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?

yes

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?

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