Zulip Chat Archive

Stream: new members

Topic: Help with Proving a Simple Theorem


view this post on Zulip Dev-Indra (Apr 25 2020 at 01:00):

Here is the lemma I am trying to prove (along with my definitions)

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 dvd_n_less_than_n (u n : ) (ha: dvd u n)(hb: u1 )(hc: u n) : u < n :=
begin
    rw dvd at ha,
    cases ha with k hk,
    rw hk,

end

Here is my tactic state after rw hk

1 goal
u n : ,
hb : u  1,
hc : u  n,
k : ,
hk : n = u * k
 u < u * k

I have tried proving this with linarith but that hasn't worked. Can anyone help me prove this lemma?

view this post on Zulip Shing Tak Lam (Apr 25 2020 at 01:33):

You haven't got strong enough assumptions in your lemma statement. You also need that n ≠ 0.

view this post on Zulip Bryan Gin-ge Chen (Apr 25 2020 at 01:33):

Here's the first thing I could get to work with that hypothesis:

import data.nat.basic

def dvd (m n: ): Prop :=  k, n = m * k

lemma dvd_n_less_than_n (u n : ) (ha: dvd u n) (hb: u  1) (hc: u  n) (hn : n  0) : u < n :=
begin
  cases ha with k hk,
  subst hk,
  rw lt_mul_iff_one_lt_right,
  { cases k,
    { contradiction, },
    { cases k,
      { simp at hc, contradiction, },
      { simp [nat.succ_lt_succ], } } },
  { cases u,
    { simp at hc, contradiction, },
    { simp, } }
end

This can probably be simplified greatly.

view this post on Zulip Shing Tak Lam (Apr 25 2020 at 01:37):

(Wrong thread sorry)

view this post on Zulip Mario Carneiro (Apr 25 2020 at 01:40):

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

view this post on Zulip Reid Barton (Apr 25 2020 at 01:42):

Ah, this is a custom dvd. Otherwise the last four lines are in the library already.

view this post on Zulip Bryan Gin-ge Chen (Apr 25 2020 at 01:57):

For completeness:

lemma dvd_n_less_than_n' (u n : ) (ha: u  n) (hb: u  1) (hc: u  n) (hn : n  0) : u < n :=
begin
  refine lt_of_le_of_ne _ hc,
  exact nat.le_of_dvd (nat.pos_of_ne_zero hn) ha,
end

Last updated: May 10 2021 at 18:22 UTC