Zulip Chat Archive

Stream: maths

Topic: one-line proof of triviality


view this post on Zulip 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

view this post on Zulip Chris Hughes (Nov 16 2019 at 00:24):

Does dsimp [ε]; linarith work?

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 00:24):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 00:25):

dsimp *, linarith works

view this post on Zulip Chris Hughes (Nov 16 2019 at 00:26):

If you used generalize instead of let it would work.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 00:26):

although it might well have side effects.

view this post on Zulip Chris Hughes (Nov 16 2019 at 00:26):

generalize makes more sense for learners.

view this post on Zulip Chris Hughes (Nov 16 2019 at 00:27):

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

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 00:27):

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

view this post on Zulip 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?

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Nov 16 2019 at 08:58):

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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 09:06):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 10:07):

I tried unfold epsilon and it didn't work iirc

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 10:08):

I like the set solution best! Thanks Rob

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 10:11):

dsimp does, but AFAIK dunfold and unfold don't

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 10:51):

January was a long time ago for my brain :D

view this post on Zulip Mario Carneiro (Nov 16 2019 at 10:52):

the gift that keeps on giving

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 10:53):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 (-;

view this post on Zulip 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