zero_max a rfl lemma

Stream: new members

[Lucas Allen]

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]

yes

[Mario Carneiro]

no

[Mario Carneiro]

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]

the given proof is insensitive to such details

[Lucas Allen]

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

[Mario Carneiro]

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

[Wojciech Nawrocki]

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

[Mario Carneiro]

yes

[Mario Carneiro]

the kernel is forced to use the definition of nat, which is unary and horrible for computation

[Scott Morrison]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

Is there a way to prove 100*100 = 10000 using binary instead of unary?

[Mario Carneiro]

by norm_num