# Zulip Chat Archive

## Stream: new members

### Topic: Proving Something is False

#### Dev-Indra (Mar 22 2020 at 18:11):

def greater (a b: ℕ): Prop := a ≥ b ∧ a ≠ b theorem g_iff_exists_add (a b: ℕ): greater a b ↔ ∃ (c: ℕ), a = b + c ∧ c ≥ 1:= begin rw greater, rw ge_iff_exists_add, rw ne_from_not_eq, split, { intro h, have h_left: ∃ (c : ℕ), a = b + c, from and.left h, have h_right: ¬a = b, from and.right h, cases h_left with u hu, use u, split, apply hu, by_contradiction, sorry } end

After I use `by_contradiction`

I have the following tactic state:

1 goal a b : ℕ, h : (∃ (c : ℕ), a = b + c) ∧ ¬a = b, h_right : ¬a = b, u : ℕ, hu : a = b + u, a_1 : ¬u ≥ 1 ⊢ false

So how to I use a_1 to conclude that u = 0. And how do I substitute this into hu to show a = b. And then how to I show a = b and h_right gives me false?

#### Daniel Keys (Mar 22 2020 at 18:30):

Your example is difficult to replicate. Can you try `push_neg at a_1`

and see what you get?

#### Dev-Indra (Mar 22 2020 at 18:31):

This is my tactic state afterwards:

1 goal a b : ℕ, h_right : ¬a = b, u : ℕ, hu : a = b + u, a_1 : u < 1, h : (∃ (c : ℕ), a = b + c) ∧ a ≠ b ⊢ false

#### Dev-Indra (Mar 22 2020 at 18:32):

Then what? Does a_1 now mean u = 0, or do I have to do something else for Lean to understand this?

#### Daniel Keys (Mar 22 2020 at 18:33):

You should be able to get `u=0`

now.

example (u : ℕ) (hu : u < 1) : u = 0 := begin linarith, end

#### Dev-Indra (Mar 22 2020 at 18:35):

And then how to I substitute u = 0 into hu? Would hu and h_right = false after the substitution?

#### Patrick Massot (Mar 22 2020 at 18:38):

@Dev-Indra if you want efficient help, you should post a MWE: one code block containing everything needed to replicate your problem (including import lines) and not more.

#### Bryan Gin-ge Chen (Mar 22 2020 at 18:38):

If `H : u = 0`

you can write `subst H`

to replace all occurrences of `u`

with `0`

, or you can rewrite specific hypotheses `h1`

, `h2`

, `h3`

using `rw H at h1 h2 h3`

.

#### Patrick Massot (Mar 22 2020 at 18:38):

This allows people to copy-paste your code and immediately see the problem.

#### Mario Carneiro (Mar 22 2020 at 18:40):

it also allows people to respond with fully formed examples as responses, so that you don't have to guess about things like where to put the `subst H`

or what punctuation to put around it

#### Dev-Indra (Mar 22 2020 at 18:41):

So here is my code:

import tactic import data.nat.prime open classical --Important theorems adapted from the Natural Number Game------------------------------ theorem ge_iff_exists_add (a b: ℕ): a ≥ b ↔ ∃ (c: ℕ), a = b + c := begin apply le_iff_exists_add, -- Ok, maybe this theorem was a little bit silly :) end def greater (a b: ℕ): Prop := a ≥ b ∧ a ≠ b theorem g_iff_exists_add (a b: ℕ): greater a b ↔ ∃ (c: ℕ), a = b + c ∧ c ≥ 1:= begin rw greater, rw ge_iff_exists_add, rw ne_from_not_eq, split, { intro h, have h_left: ∃ (c : ℕ), a = b + c, from and.left h, have h_right: ¬a = b, from and.right h, cases h_left with u hu, use u, split, apply hu, by_contradiction, push_neg at a_1, sorry }, { intro h2, cases h2 with u hu, have hu_left: a = b+u, from and.left hu, split, use u, apply hu_left, by_contradiction, have wrong: a = b, apply a_1, sorry } end

#### Daniel Keys (Mar 22 2020 at 18:42):

Dev-Indra said:

And then how to I substitute u = 0 into hu? Would hu and h_right = false after the substitution?

For this kind of tasks, it is a good idea to go through the Natural Numbers Game.

#### Dev-Indra (Mar 22 2020 at 18:51):

Here is my tactic state:

1 goal a b : ℕ, h_right : ¬a = b, h : (∃ (c : ℕ), a = b + c) ∧ a ≠ b, hu : a = b, h_right : a ≠ b ⊢ false

Is there a way to take the disjunction of hu and h_right?

#### Daniel Keys (Mar 22 2020 at 18:54):

`exact h_right hu`

#### Dev-Indra (Mar 22 2020 at 18:54):

and finally is there a theorem that states p and not p implies false? If so, what is the theorem name?

#### Mario Carneiro (Mar 22 2020 at 18:55):

if `hnp : not p`

and `hp : p`

then `hnp hp : false`

#### Mario Carneiro (Mar 22 2020 at 18:55):

because `not p`

is defined to be `p -> false`

#### Patrick Massot (Mar 22 2020 at 18:56):

You need to learn about negation in the foundations used by Lean.

#### Patrick Massot (Mar 22 2020 at 19:03):

The following is probably what you wanted to do (although it's not the optimal road). You can read what library_search says and put it instead of library_search.

import tactic --Important theorems adapted from the Natural Number Game------------------------------ theorem ge_iff_exists_add (a b: ℕ): a ≥ b ↔ ∃ (c: ℕ), a = b + c := le_iff_exists_add -- this is only defining an alias to le_iff_exists_add def greater (a b: ℕ): Prop := a ≥ b ∧ a ≠ b theorem g_iff_exists_add (a b: ℕ): greater a b ↔ ∃ (c: ℕ), a = b + c ∧ c ≥ 1:= begin rw greater, rw ge_iff_exists_add, --rw ne_from_not_eq, -- this line is useless split, { rintro ⟨⟨u, hu⟩, h_right⟩, use [u, hu], by_contradiction H, push_neg at H, interval_cases u, contradiction }, { rintro ⟨u, hu_left, hu_right⟩, split, use [u, hu_left], -- linarith would finish here assume wrong: a = b, rw wrong at hu_left, have : u = 0, by library_search, have : u ≠ 0, by library_search, contradiction } end

Last updated: May 16 2021 at 20:13 UTC