Zulip Chat Archive

Stream: new members

Topic: Proving Something is False


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 22 2020 at 18:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Daniel Keys (Mar 22 2020 at 18:54):

exact h_right hu

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 18:55):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 18:55):

because not p is defined to be p -> false

view this post on Zulip Patrick Massot (Mar 22 2020 at 18:56):

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

view this post on Zulip 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