Proving Something is False

Stream: new members

[Dev-Indra]

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]

Your example is difficult to replicate. Can you try push_neg at a_1 and see what you get?

[Dev-Indra]

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]

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

[Daniel Keys]

You should be able to get u=0 now.

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

[Dev-Indra]

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

[Patrick Massot]

@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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

exact h_right hu

[Dev-Indra]

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

[Mario Carneiro]

if hnp : not p and hp : p then hnp hp : false

[Mario Carneiro]

because not p is defined to be p -> false

[Patrick Massot]

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

[Patrick Massot]

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