Zulip Chat Archive

Stream: new members

Topic: Either Prime or Composite


view this post on Zulip Dev-Indra (Apr 26 2020 at 15:55):

Here is the theorem (either prime or composite) that I am trying to prove (I also gave some helper lemmas that are already proven). I created a lemma called dvd_n_less_than_n but I cannot seem to apply it. I commented this near the end of my theorem. Please help.

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,-- I have the lemma proved above but can't use it

            },


            split,
            exact hk,

            split,

            have h3: u  1, from and.left h2,
            refl,

            --apply dvd_n_less_than_n, I have the lemma proved above but can't use it

        }

    },
    {

    }
end

view this post on Zulip Reid Barton (Apr 26 2020 at 16:03):

Please supply the correct imports, especially if you are pasting 200 lines of code already :upside_down:

view this post on Zulip Reid Barton (Apr 26 2020 at 16:04):

You're missing a comma before the first commented-out apply

view this post on Zulip Reid Barton (Apr 26 2020 at 16:04):

however, in my opinion the main problem is that your proof is too big and inefficient

view this post on Zulip Reid Barton (Apr 26 2020 at 16:05):

I can't get Lean to show the tactic state after apply dvd_n_less_than_n, and I suspect the reason is that the proof uses linarith about 20 times.

view this post on Zulip Dev-Indra (Apr 26 2020 at 16:09):

Thanks, it was the comma that was messing things up.


Last updated: May 08 2021 at 09:11 UTC