Zulip Chat Archive

Stream: maths

Topic: lean absurd proof


view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:26):

Hi! I'm playing around with https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/, and I'm at level 15 of the inequality world.
I have a hypothesis h : ¬∃ (c : mynat), a = b + c and I'm not really sure how to use it. What I'd do outside of lean is "assume there is such a c, let's show we get to a contradiction", but I don't know how to express that.
Could anybody help?

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:28):

You have a hypothesis that such a c gives you a contradiction, so your argument outside of Lean just gives you another proof of that hypothesis. I don't understand your logic here.

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:32):

Point taken. How would I do that with the goal, then?

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:34):

and let's say I have a specific d such as a = b + d, how do I get to false with h?

view this post on Zulip Shing Tak Lam (Apr 13 2020 at 09:36):

Is your goal false? If so,

apply h,
use d,

Should do, if your goal is not false, then you could use exfalso to turn it into false.

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:37):

Thanks for the tip!

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:38):

so how can I turn a proof into the absurd? i.e. I'm trying to prove p, how do I get to "given not p, prove false"?

view this post on Zulip Chris Hughes (Apr 13 2020 at 09:38):

I think it's by_contradiction

view this post on Zulip Shing Tak Lam (Apr 13 2020 at 09:38):

So proof by contardiction? by_contra (or by_contradiction)

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:41):

I tried that, but I'm getting this:
tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable) state: a b d : mynat, h : b = a + d, h1 : ¬∃ (c : mynat), a = b + c ⊢ succ a ≤ b

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:42):

it works when my goal is a negation, though, but not like this

view this post on Zulip Shing Tak Lam (Apr 13 2020 at 09:42):

Can you post what you have so far? It's a bit hard to work out what is happening only looking at goals and error mesages.

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:44):

Well, you have the state in the error :)

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:45):

Oh! I did not put a decidable equality on mynat so this tactic might not work if I didn't put classical mode on

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:45):

lemma lt_aux_one (a b : mynat) : a  b  ¬ (b  a)  succ a  b :=
intro h,
  cases h with h h1,
  cases h with d h,
  rw le_iff_exists_add at h1,

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:45):

Quote code using ```lean at the top and ``` at the bottom

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:46):

Just use exfalso here though

view this post on Zulip Mario Carneiro (Apr 13 2020 at 09:46):

Anyone up to PR by_contra! and by_contradiction! to skip the decidable check?

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:46):

And remember that not X just means X implies false

view this post on Zulip Kenny Lau (Apr 13 2020 at 09:47):

meta def «by_contra!» := `[classical; by_contra]

view this post on Zulip Mario Carneiro (Apr 13 2020 at 09:47):

sorry, by_contra! isn't an identifier

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:47):

PR!

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:47):

yeah, I remember the equivalence with the implication, but it's kinda hard to use

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:48):

You can use apply if you have a hypothesis which is an implication

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:48):

and exfalso doesn't really help here, it's not true AFAICT

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:48):

Exfalso is what you need

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:48):

It helps

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:49):

Use exfalso and now your goal is Y (= false) and you have a hypothesis X-> Y so you can apply it

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:53):

Sure, but I end up with:

a b d : mynat,
h : b = a + d,
h1 : ¬∃ (c : mynat), a = b + c
  (c : mynat), a = b + c

which is not true (you can put c = 0 and it would be true for d = 0, but not for all d)

view this post on Zulip Shing Tak Lam (Apr 13 2020 at 09:53):

Try cases d first? Then use exfalso for the first goal.

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:53):

This is fine

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:54):

What do you mean it's not true? You can prove it

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:54):

It's easy to prove using h

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:54):

This is exactly the way to proceed

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:55):

Oh sorry

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:55):

I've misread

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:55):

:-(

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:56):

Ah, thanks, with cases d it works fine

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:56):

:-)

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:57):

Sorry, I misread h. A lot of what I said was nonsense

view this post on Zulip Valentin Tolmer (Apr 13 2020 at 09:57):

Thanks everyone!


Last updated: May 19 2021 at 03:22 UTC