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

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

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,

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 :=

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 ne_from_not_eq, -- this line is useless
split,
{ rintro ⟨⟨u, hu⟩, h_right⟩,
use [u, hu],
push_neg at H,
interval_cases u,
{ 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,