Stream: maths

Topic: one-line proof of triviality

Kevin Buzzard (Nov 16 2019 at 00:18):

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 (Nov 16 2019 at 00:24):

Does dsimp [ε]; linarith work?

Kevin Buzzard (Nov 16 2019 at 00:24):

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

Kevin Buzzard (Nov 16 2019 at 00:25):

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

Kevin Buzzard (Nov 16 2019 at 00:25):

dsimp *, linarith works

Chris Hughes (Nov 16 2019 at 00:26):

If you used generalize instead of let it would work.

Kevin Buzzard (Nov 16 2019 at 00:26):

although it might well have side effects.

Chris Hughes (Nov 16 2019 at 00:26):

generalize makes more sense for learners.

Chris Hughes (Nov 16 2019 at 00:27):

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

Kevin Buzzard (Nov 16 2019 at 00:27):

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

Kevin Buzzard (Nov 16 2019 at 00:30):

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 (Nov 16 2019 at 00:31):

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

Kevin Buzzard (Nov 16 2019 at 00:32):

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 (Nov 16 2019 at 00:35):

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

Kevin Buzzard (Nov 16 2019 at 00:38):

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 (Nov 16 2019 at 00:46):

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 (Nov 16 2019 at 08:52):

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 (Nov 16 2019 at 08:56):

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 (Nov 16 2019 at 08:58):

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

Mario Carneiro (Nov 16 2019 at 09:06):

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

Rob Lewis (Nov 16 2019 at 09:11):

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 (Nov 16 2019 at 10:07):

I tried unfold epsilon and it didn't work iirc

Kevin Buzzard (Nov 16 2019 at 10:08):

I like the set solution best! Thanks Rob

Mario Carneiro (Nov 16 2019 at 10:10):

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

Mario Carneiro (Nov 16 2019 at 10:11):

dsimp does, but AFAIK dunfold and unfold don't

Rob Lewis (Nov 16 2019 at 10:12):

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 (Nov 16 2019 at 10:51):

January was a long time ago for my brain :D

Mario Carneiro (Nov 16 2019 at 10:52):

the gift that keeps on giving

Kevin Buzzard (Nov 16 2019 at 10:53):

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

Kevin Buzzard (Nov 16 2019 at 10:55):

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 (Nov 16 2019 at 11:00):

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 (Nov 16 2019 at 11:06):

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 (Nov 16 2019 at 11:45):

Oh that happens to me all the time! :D

Last updated: May 09 2021 at 09:11 UTC