Zulip Chat Archive

Stream: general

Topic: Crazy rewrite


view this post on Zulip Patrick Massot (Mar 02 2020 at 14:10):

My students explore Lean by typing random commands. Does anyone understand how the following proof works?

import data.real.basic

def injective (f :   ) :=  x x', f x = f x'  x = x'

example (f g :   ) :
  injective f  injective g  injective (g  f) :=
begin
  intros hf hg x x' gof,
  rw hf x,
  rw hg (f x),
  exact gof,
end

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 14:12):

The issue being that it should be apply not rw. This is a common issue with mathematicians, they can't tell the difference between == and     \implies, and indeed in work of schoolkids I've seen the terms used interchangeably. It's very surprising to me that this works!

view this post on Zulip Chris Hughes (Mar 02 2020 at 14:12):

The first rw hf x closes the first goal, but creates a new one for the assumption to injective

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:12):

Yes, exactly. I feel betrayed by Lean!

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 14:13):

Well spotted Chris :-)

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:14):

Sorry, I don't buy this explanation.

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:15):

Oooh, maybe I see.

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:15):

This is evil.

view this post on Zulip Chris Hughes (Mar 02 2020 at 14:15):

When you do rw it creates new goals for assumptions to the lemmas you used.

view this post on Zulip Donald Sebastian Leung (Mar 02 2020 at 14:15):

Chris Hughes said:

The first rw hf x closes the first goal, but creates a new one for the assumption to injective

I was interested enough by this to pause my work on formalizing incidence geometry in Lean and step through this proof, and was wondering why the heck rw was acting like apply :rofl:

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:16):

Can you imagine the random walk that led to this? Note that rw hf won't do the trick.

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:18):

But I don't have a choice. I promised I would give full credit for Lean proofs that work and don't use the mathlib version of the statement. But I also asked for a pen and paper proof of the same result, and there I can remove credit.

view this post on Zulip Chris Hughes (Mar 02 2020 at 14:19):

The follow-your-nose approach often leads to proofs you don't really understand.

view this post on Zulip Johan Commelin (Mar 02 2020 at 14:19):

Maybe they used hint? And maybe hint ranked rw higher than apply. (It's shorter after all. Do they get points for golfing?)

view this post on Zulip Donald Sebastian Leung (Mar 02 2020 at 14:20):

Johan Commelin said:

Maybe they used hint? And maybe hint ranked rw higher than apply. (It's shorter after all. Do they get points for golfing?)

Ooh ... proof golfing ... :thinking:

view this post on Zulip Rob Lewis (Mar 02 2020 at 14:27):

I don't think hint suggests tactics like rw and apply that take parameters.

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:28):

Their mathlib was frozen at the beginning of the term in early January, so they don't have hint.


Last updated: May 06 2021 at 22:13 UTC