Zulip Chat Archive

Stream: new members

Topic: Help with proving with contradiction


view this post on Zulip Dev-Indra (Apr 28 2020 at 18:40):

Here is my code, along with some definitions and helper theorems (I know its long, but my main issue is at the very end where I have the comment -- Help here ---)

def dvd (m n: ): Prop :=  k, n = m * k
def prime (p : ) : Prop := p  2   n, dvd n p  n = 1  n = p
def composite (d : ): Prop:=  (a b: ), d = a*b  a  b  b < d

lemma greater_than_not_zero (n : )(n  2): n  0:=
begin
    exact lattice.ne_bot_of_gt H,
end

lemma dvd_n_less_than_n (u n : ) (ha: dvd u n) (hb: u  1) (hc: u  n) (hn : n  0) : u < n :=
begin
  refine lt_of_le_of_ne _ hc,
  rcases ha with k, rfl,
  simpa using nat.mul_le_mul_left _ (_:1≤_),
  refine nat.pos_iff_ne_zero.2 (mt _ hn),
  rintro rfl, refl,
end

lemma either_prime_or_composite (n: ) (ge: n 2): (¬ (prime n)  composite n) :=
begin
    split,
    {
        intros h,
        rw prime at h,
        rw composite,

        push_neg at h,

        cases h,
        {
            linarith,
        } ,
        {
            cases h with u hu,
           let hu_left:= hu.1,
           rw dvd at hu_left,
           cases hu_left with k hk,

           have u_g_k : (u k) (u>k),
           {
--               by library_search,
                exact le_or_lt u k,
           },
           cases u_g_k,
            {
                use u,
                use k,
                split,
                exact hk,
                split,
                exact u_g_k,

                let hu_mid:= hu.2.1,

                have u_ge_1 : (u 1),
                {
                    by_contradiction,
                    have u_zero: u=0,
                    {
                        linarith,
                    },
                    have n_zero: n=0,
                    {
                        subst u_zero,
                        simp at hk,
                        exact hk,
                    },
                    linarith,
                },
                have u_ge_2 : (u 2),
                {
                    by_contradiction,
                    have u_less_2 : u<2,
                    {
                        linarith,
                    },
                    have u_eq_1: u=1,
                    {
                        linarith,
                    },
--                    by library_search,
                    exact hu_mid u_eq_1,
                },
                by_contradiction,

                have k_ge_n: k n,
                {
                    linarith,
                },
                have uk_ge_2n: u*k 2* n,
                {
--                    by library_search,
                    exact canonically_ordered_semiring.mul_le_mul u_ge_2 k_ge_n,
                },
                have n_ge_2n: n 2*n,
                {
                    linarith,
                },
                have twon_gt_n: 2*n > n,
                {
                    linarith,
                },
                linarith,

            },
            {
                use k,
                use u,
                split,
                rw mul_comm at hk,
                exact hk,
                split,
                --exact u_g_k,

                let hu_mid:= hu.2.1,

                have u_ge_1 : (u 1),
                {
                    by_contradiction,
                    have u_zero: u=0,
                    {
                        linarith,
                    },
                    have n_zero: n=0,
                    {
                        subst u_zero,
                        simp at hk,
                        exact hk,
                    },
                    linarith,
                },
                have u_ge_2 : (u 2),
                {
                    by_contradiction,
                    have u_less_2 : u<2,
                    {
                        linarith,
                    },
                    have u_eq_1: u=1,
                    {
                        linarith,
                    },
--                    by library_search,
                    exact hu_mid u_eq_1,
                },
                by_contradiction,

                have k_ge_n: k n,
                {
                    linarith,
                },
                have uk_ge_2n: u*k 2* n,
                {
--                    by library_search,
                    exact canonically_ordered_semiring.mul_le_mul u_ge_2 k_ge_n,
                },
                have n_ge_2n: n 2*n,
                {
                    linarith,
                },
                have twon_gt_n: 2*n > n,
                {
                    linarith,
                },
                linarith,

                have ha: dvd u n, from and.left hu,
                have h2: u  1  u  n, from and.right hu,
                have hc: u  n, from and.right h2,
                have hb: u  1, from and.left h2,
                have hn: n  0,
                {
                    exact lattice.ne_bot_of_gt ge,
                },

                apply dvd_n_less_than_n,
                have h4: dvd u n, from and.left hu,
                apply h4,
                apply hb,
                apply hc,
                apply hn,
            },

        }

    },
    {
      intros h,
      rw composite at h,
      by_contradiction,
      rw prime at a,

      cases h with a1 ha1,
      cases ha1 with b hb,

      have h1: n = a1*b, from and.left hb,
      have temp: a1  b  b < n, from and.right hb,
      have h2: a1  b, from and.left temp,
      have h3: b < n, from and.right temp,

      have hc := a.right b,

      have b_isnt_one: b  1,
      {
        by_contradiction,
        push_neg at a_1,
        subst a_1,
        rw mul_one at h1,
        linarith,
      },

      have b_divides_n: dvd b n,
      {
          rw dvd,
          rw mul_comm at h1,
          use a1,
          rw h1,
      },

      have b_is_trivial: b = 1  b = n,
      {
        exact hc b_divides_n,
      },

      --Help here--
    },
end

So basically, I have the statements: b_is_trivial : b = 1 \or b = n, b_isnt_one: b \neq 1 andh3: b < n. I want to get a contradiction, but I cant. I tried using linarith and by library search, but nothing worked. Any suggestions?

view this post on Zulip Reid Barton (Apr 28 2020 at 18:43):

A huge block of code is not useful without the correct imports.

view this post on Zulip Reid Barton (Apr 28 2020 at 18:43):

That said, use cases on b_is_trivial.

view this post on Zulip Patrick Massot (Apr 28 2020 at 18:54):

@Dev-Indra Why do you post this huge pile of code (without import) if your question if how to prove example (n b) (b_is_trivial : b = 1 ∨ b = n) (b_isnt_one: b ≠ 1) (h3: b < n) : false?

view this post on Zulip Patrick Massot (Apr 28 2020 at 18:56):

Alternative to Reid's method: by linarith [or_iff_not_imp_left.mp b_is_trivial b_isnt_one]. Of course you can also write the proof term by hand.

view this post on Zulip Dev-Indra (Apr 28 2020 at 18:59):

@Patrick Massot Sometimes when I asked questions in the past, people wanted me to put in the code so that they can run it on their laptops. As for imports I only had import tactic at the top, and I assumed everyone has this import statement. But thanks for the help. My code works now.

view this post on Zulip Reid Barton (Apr 28 2020 at 19:01):

With just import tactic already lattice.ne_bot_of_gt is not in scope.

view this post on Zulip Reid Barton (Apr 28 2020 at 19:01):

But why omit one or two lines out of a hundred?

view this post on Zulip Patrick Massot (Apr 28 2020 at 19:02):

What I posted is a MWE. You can copy the file I posted in an empty Lean file and it works.

view this post on Zulip Patrick Massot (Apr 28 2020 at 19:03):

I mean before I posted the proof, which does use import tactic

view this post on Zulip Jalex Stark (Apr 29 2020 at 13:58):

Dev-Indra said:

Patrick Massot Sometimes when I asked questions in the past, people wanted me to put in the code so that they can run it on their laptops. As for imports I only had import tactic at the top, and I assumed everyone has this import statement. But thanks for the help. My code works now.

"minimum working example" means that I can copy your code block, paste into a new file in my lean project, and see what the problem is. The "working" part means I shouldn't have to add any code myself, and you can test this by... copying your code block into a new lean file! The "minimum" part means that there aren't unnecessary bits that will distract me before I see what's wrong.

I know it sounds annoying, but if you don't post a mwe then you are implicitly valuing your time over the time of people that might help you.

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:00):

do we have a standard linkpost for the definition of MWE yet?

view this post on Zulip Reid Barton (Apr 29 2020 at 14:01):

I also endorse the edit. In particular, there is only one of you but there may be multiple people who could help you, so even if you valued all people's time equally it would still make sense to put in the effort yourself.

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:02):

Maybe we can use the Zulip linkifier so that #mwe links to something useful

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:03):

macro time... maybe not

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:04):

does Zulip even have macros?

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:04):

https://en.wikipedia.org/wiki/Minimal_working_example

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:05):

@Kenny Lau lean#251

view this post on Zulip Rob Lewis (Apr 29 2020 at 14:05):

If there's a place to link to, that's very easy to do. Maybe even better: posting #mwe or #codebackticks or whatever could summon a bot to make a prerecorded post.

view this post on Zulip Rob Lewis (Apr 29 2020 at 14:05):

Zulip bot scripting is pretty easy.

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:05):

your wiki link doesn't emphasize on "working"

view this post on Zulip Reid Barton (Apr 29 2020 at 14:06):

It also doesn't explain the why

view this post on Zulip Rob Lewis (Apr 29 2020 at 14:06):

The bigger challenge is automatically identifying posts that are missing a mwe or backticks.

view this post on Zulip Reid Barton (Apr 29 2020 at 14:07):

I think we could train an AI for the backticks one.

view this post on Zulip Reid Barton (Apr 29 2020 at 14:07):

Once Sebastien formalizes the sigmoid function.

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:07):

Rob Lewis said:

The bigger challenge is automatically identifying posts that are missing a mwe or backticks.

That would be great, too, but having a macro for humans to type is already a big step forward

view this post on Zulip Reid Barton (Apr 29 2020 at 14:08):

I'm not sure but I think there's some way a human can trigger a bot manually, using a / command or something? Now that I think about it I'm not sure how it is supposed to work

view this post on Zulip Rob Lewis (Apr 29 2020 at 14:09):

I think bots can scan the contents of posts. It should be easy to write a bot that watches for #mwe.

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:09):

I think the documentation here is enough for anyone willing to give it a go:
https://zulipchat.com/api/running-bots

view this post on Zulip Reid Barton (Apr 29 2020 at 14:11):

Right, I was just wondering whether the extra noise of someone typing #mwe could be avoided

view this post on Zulip Reid Barton (Apr 29 2020 at 14:12):

maybe that's not even a good idea though

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:12):

I was thinking we would just write

please provide an #mwe

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:12):

And then Zulip would linkify #mwe

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:12):

Gotcha.
My model of how this works i based off of chatbots in twitch streams.

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:12):

what is linkify? is it something admins can edit?

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:12):

And then user clicks and gets enlightened

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:13):

Do we have a "server meta" stream?

view this post on Zulip Reid Barton (Apr 29 2020 at 14:13):

Johan Commelin said:

And then Zulip would linkify #mwe

This might be better, since we can put more text on the page linked to than we would want to see a bot write out over and over.

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:13):

I think the bot should say two-ish sentences to convince the user to click the link

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:13):

Kenny Lau said:

what is linkify? is it something admins can edit?

yes

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:14):

We only need to ping @Mario Carneiro and it will be done before you can say #mwe

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:14):

but what do we want to link it to?

view this post on Zulip Rob Lewis (Apr 29 2020 at 14:15):

Yeah, I was thinking the bot post would be more visible. We don't have to trust people to click #mwe instead of posting "what's a #mwe?"

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:15):

If we are lazy: wiki, and otherwise a custom page hosted on leanprover-community.github.io

view this post on Zulip Rob Lewis (Apr 29 2020 at 14:15):

But either way is an improvement!

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:17):

https://github.com/leanprover-community/mathlib/wiki/Minimum-Working-Example-(MWE)

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:18):

I think this discussion could profitably move here
https://leanprover.zulipchat.com/#narrow/stream/236604-server-meta/topic/.23mwe.20bot

view this post on Zulip Mario Carneiro (Apr 29 2020 at 14:27):

Just clarifying that the reason I was summoned is not the way people are planning to implement this, yes?

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:28):

Well...

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:29):

I don't see anything wrong with having #mwe link to the wiki page

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:29):

You are an admin, so you can help us avoid it that way


Last updated: May 08 2021 at 02:46 UTC