Either Prime or Composite

Stream: new members

[Dev-Indra]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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.

[Dev-Indra]

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