Zulip Chat Archive

Stream: new members

Topic: zero_max a rfl lemma


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 23 2019 at 03:34):

yes

view this post on Zulip Mario Carneiro (Oct 23 2019 at 03:49):

no

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 23 2019 at 03:52):

the given proof is insensitive to such details

view this post on Zulip Lucas Allen (Oct 23 2019 at 21:49):

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

view this post on Zulip 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

view this post on Zulip Wojciech Nawrocki (Oct 23 2019 at 22:42):

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

view this post on Zulip Mario Carneiro (Oct 23 2019 at 23:02):

yes

view this post on Zulip 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

view this post on Zulip 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."

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 24 2019 at 17:23):

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

view this post on Zulip 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

view this post on Zulip Lucas Allen (Oct 25 2019 at 21:50):

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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:03):

by norm_num


Last updated: May 14 2021 at 06:16 UTC