Crazy rewrite

Stream: general

[Patrick Massot]

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]

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]

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

[Patrick Massot]

Yes, exactly. I feel betrayed by Lean!

[Kevin Buzzard]

Well spotted Chris :-)

[Patrick Massot]

Sorry, I don't buy this explanation.

[Patrick Massot]

Oooh, maybe I see.

[Patrick Massot]

This is evil.

[Chris Hughes]

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

[Donald Sebastian Leung]

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]

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

[Patrick Massot]

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]

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

[Johan Commelin]

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]

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]

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

[Patrick Massot]

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