## Stream: maths

### Topic: lean absurd proof

#### 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?

#### 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.

#### Valentin Tolmer (Apr 13 2020 at 09:32):

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

#### 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?

#### 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.

#### Valentin Tolmer (Apr 13 2020 at 09:37):

Thanks for the tip!

#### 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"?

#### Chris Hughes (Apr 13 2020 at 09:38):

I think it's by_contradiction

#### Shing Tak Lam (Apr 13 2020 at 09:38):

So proof by contardiction? by_contra (or by_contradiction)

#### 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

#### Valentin Tolmer (Apr 13 2020 at 09:42):

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

#### 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.

#### Valentin Tolmer (Apr 13 2020 at 09:44):

Well, you have the state in the error :)

#### 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

#### 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,


#### Kevin Buzzard (Apr 13 2020 at 09:45):

Quote code using  lean  at the top and    at the bottom

#### Kevin Buzzard (Apr 13 2020 at 09:46):

Just use exfalso here though

#### Mario Carneiro (Apr 13 2020 at 09:46):

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

#### Kevin Buzzard (Apr 13 2020 at 09:46):

And remember that not X just means X implies false

#### Kenny Lau (Apr 13 2020 at 09:47):

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


#### Mario Carneiro (Apr 13 2020 at 09:47):

sorry, by_contra! isn't an identifier

PR!

#### Valentin Tolmer (Apr 13 2020 at 09:47):

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

#### Kevin Buzzard (Apr 13 2020 at 09:48):

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

#### Valentin Tolmer (Apr 13 2020 at 09:48):

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

#### Kevin Buzzard (Apr 13 2020 at 09:48):

Exfalso is what you need

It helps

#### 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

#### 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)

#### Shing Tak Lam (Apr 13 2020 at 09:53):

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

This is fine

#### Kevin Buzzard (Apr 13 2020 at 09:54):

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

#### Kevin Buzzard (Apr 13 2020 at 09:54):

It's easy to prove using h

#### Kevin Buzzard (Apr 13 2020 at 09:54):

This is exactly the way to proceed

Oh sorry

:-(

#### Valentin Tolmer (Apr 13 2020 at 09:56):

Ah, thanks, with cases d` it works fine

:-)

#### Kevin Buzzard (Apr 13 2020 at 09:57):

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

#### Valentin Tolmer (Apr 13 2020 at 09:57):

Thanks everyone!

Last updated: May 19 2021 at 03:22 UTC