one-line proof of triviality

Stream: maths

[Kevin Buzzard]

The following is a bit annoying from a pedagogical perspective. Is there any workaround short of "don't introduce epsilon" or "remove epsilon by writing show (b - a) / 2 > 0 before linarith"? I'm completely happy to make local modifications to linarith; I'm thinking about making a real number game but obviously I want to make everything as easy as possible for the mathematician end-user (I'm targetting UGs who are learning about limits right now at my university).

import data.real.basic

example (a b : ℝ) (h : a < b) : (b - a) / 2 > 0 := by linarith -- works

example (a b : ℝ) (h : a < b) : true :=
begin
  let ε := (b - a) / 2,
  have h : ε > 0,
    linarith, -- fails

end

[Chris Hughes]

Does dsimp [ε]; linarith work?

[Kevin Buzzard]

Aah it does. I tried unfold \e and that didn't work but your trick does.

[Kevin Buzzard]

I'd still rather have a tactic which didnt mention epsilon at all though, so I could just attach it to linarith.

[Kevin Buzzard]

dsimp *, linarith works

[Chris Hughes]

If you used generalize instead of let it would work.

[Kevin Buzzard]

although it might well have side effects.

[Chris Hughes]

generalize makes more sense for learners.

[Chris Hughes]

because you get the hypothesis that epsilon = (a - b) / 2

[Kevin Buzzard]

but epsilon isn't in the target until after the have

[Kevin Buzzard]

you're right though in that if I add h1 : ε = (m - l) / 2 to the local context then linarith works again. What does this ε : ℝ := (m - l) / 2, mean then? linarith can't see through it but it's not a hypothesis either?

[Kevin Buzzard]

I could hack let so that let A := B adds h : A = B to the local context :-)

[Kevin Buzzard]

In fact if let A := B changed the local context by adding A : real and hA : A = B rather than doing what it currently does, I wouldn't be in this situation.

[Chris Hughes]

generalize is exactly your hacked let. generalise h : (a - b) / 2 = epsilon does what you want I think.

[Kevin Buzzard]

Oh you're absolutely right! I tried it and it didn't work but I think I got the equality the wrong way around. Thanks! I misunderstood the man page -- it talking about replacing things in the "target" which I incorrectly assumed meant "the goal"

[Chris Hughes]

I think it does mean the goal. If there is an (a - b) /2 in the goal it will be replaced with epsilon

[Rob Lewis]

I thought I added the set tactic because you asked exactly this question before. set ε := (b - a) / 2 with h or something like that should work.

[Rob Lewis]

you're right though in that if I add h1 : ε = (m - l) / 2 to the local context then linarith works again. What does this ε : ℝ := (m - l) / 2, mean then? linarith can't see through it but it's not a hypothesis either?

It means epsilon is "locally defined" to be (m - l)/2. You shouldn't expect linarith to see through it any more than if it were a function epsilon m l you defined separately.

[Rob Lewis]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linarith.20failure/near/157057941

[Mario Carneiro]

Would it make sense for linarith [ε] to unfold epsilon as a preprocessing step?

[Rob Lewis]

That syntax is taken for adding to/restricting the list of inequalities it uses, but yes, something like that could be done. But linarith unfolding [epsilon] would just be sugar for unfold epsilon; linarith, it's barely different.

[Kevin Buzzard]

I tried unfold epsilon and it didn't work iirc

[Kevin Buzzard]

I like the set solution best! Thanks Rob

[Mario Carneiro]

Not all unfolding tactics know how to unfold let expressions in the context, they are a bit special

[Mario Carneiro]

dsimp does, but AFAIK dunfold and unfold don't

[Rob Lewis]

I like the set solution best! Thanks Rob

I'm not surprised, since it was added in response to you asking this exact question in January!

[Kevin Buzzard]

January was a long time ago for my brain :D

[Mario Carneiro]

the gift that keeps on giving

[Kevin Buzzard]

I'll try to remember to ask again next August or so.

[Kevin Buzzard]

In fact I'm more likely to remember it this time, because probably in Jan I just needed it to show off Lean in some informal seminars I was giving to analysis students, whereas this time I am trying to make some real number game using it so now I have to think about how to teach it, and teaching is always a good way of learning stuff.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linarith.20failure/near/157057941

In practice I have some positive real eps := (b - a) / 2

rofl

[Johan Commelin]

As a bit of solace... at some point I found a really interesting question on mathoverflow about the Mumford–Tate conjecture. I was so excited that someone was thinking about these questions in the exact same way as I was... well you can figure out the rest (-;

[Kevin Buzzard]

Oh that happens to me all the time! :D