lean absurd proof

Stream: maths

[Valentin Tolmer]

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]

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]

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

[Valentin Tolmer]

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]

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]

Thanks for the tip!

[Valentin Tolmer]

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]

I think it's by_contradiction

[Shing Tak Lam]

So proof by contardiction? by_contra (or by_contradiction)

[Valentin Tolmer]

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]

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

[Shing Tak Lam]

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]

Well, you have the state in the error :)

[Kevin Buzzard]

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]

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,

[Kevin Buzzard]

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

[Kevin Buzzard]

Just use exfalso here though

[Mario Carneiro]

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

[Kevin Buzzard]

And remember that not X just means X implies false

[Kenny Lau]

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

[Mario Carneiro]

sorry, by_contra! isn't an identifier

[Kevin Buzzard]

PR!

[Valentin Tolmer]

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

[Kevin Buzzard]

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

[Valentin Tolmer]

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

[Kevin Buzzard]

Exfalso is what you need

[Kevin Buzzard]

It helps

[Kevin Buzzard]

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

[Valentin Tolmer]

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]

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

[Kevin Buzzard]

This is fine

[Kevin Buzzard]

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

[Kevin Buzzard]

It's easy to prove using h

[Kevin Buzzard]

This is exactly the way to proceed

[Kevin Buzzard]

Oh sorry

[Kevin Buzzard]

I've misread

[Kevin Buzzard]

:-(

[Valentin Tolmer]

Ah, thanks, with cases d it works fine

[Kevin Buzzard]

:-)

[Kevin Buzzard]

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

[Valentin Tolmer]

Thanks everyone!