## Stream: general

### Topic: Crazy rewrite

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


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

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

#### Patrick Massot (Mar 02 2020 at 14:12):

Yes, exactly. I feel betrayed by Lean!

#### Kevin Buzzard (Mar 02 2020 at 14:13):

Well spotted Chris :-)

#### Patrick Massot (Mar 02 2020 at 14:14):

Sorry, I don't buy this explanation.

#### Patrick Massot (Mar 02 2020 at 14:15):

Oooh, maybe I see.

This is evil.

#### Chris Hughes (Mar 02 2020 at 14:15):

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

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

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

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

#### Chris Hughes (Mar 02 2020 at 14:19):

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

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

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

#### Rob Lewis (Mar 02 2020 at 14:27):

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

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