Zulip Chat Archive

Stream: new members

Topic: equivalent definitions of prime


view this post on Zulip Lucas Allen (Oct 28 2019 at 02:52):

I have another definition for prime and I want to prove that it's equivalent to the definition in mathlib. My definition is

def divisors_aux (n : ) :   list 
| 0     := []
| 1     := [1]
| (h+1) := if n % h = 0
           then [h] ++ divisors_aux h
           else divisors_aux h

def divisors (n :) := divisors_aux n (n+1)

def myprime (p : ) : Prop := (p  2)  divisors p = [1,p]

The divisors function gives a list of divisors, and myprime p says a number is primes if the divisor are 1 and p.

Here's my attempt at the first direction

lemma my_prime_good (p n : ) : prime p  myprime p :=
have s₁ : prime p  (p  2), from prime.two_le,
have s₄ : prime p  (n  p  n = 1  n = p), from λ (pp : prime p), (dvd_prime pp).mp,
have s₂ : (n  p  n = 1  n = p)  divisors p = [1,p], from
begin
  intro,
  sorry
end,
have s₃ : (p  2)  (divisors p = [1,p])  myprime p, from
  begin intros, unfold myprime, assumption, end,
show prime p  myprime p, from
begin intro, apply s₃, split,
  exact s₁ a,
  exact s₂ (s₄ a)
end

I'm totally stuck at the sorry. I think I need to break divisors into cases somehow. How can I prove this?

view this post on Zulip Reid Barton (Oct 28 2019 at 03:12):

Since you defined divisors_aux by recursion you will need to prove things about it by induction. By the way, you should test your functions using #eval (divisors 5) to see if it really behaves how you expect.

view this post on Zulip Reid Barton (Oct 28 2019 at 03:13):

You can prove something like if p is prime and 1 <= a <= p then divisors_aux p a = [1] by induction on a, and then compute divisors p.

view this post on Zulip Lucas Allen (Oct 30 2019 at 00:08):

I had a go at proving that if p is prime and 1 <= a <= p then divisors_aux p a = [1], but I don't know how to break apart divisors_aux. When I run unfold divisors_aux I get the error "simplify tactic failed to simplify." Is there some other way to unfold these definitions, or is there a way around this problem?

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:16):

divisors_aux n 0 and divisors_aux n (h+1) can be simplified, but not divisors_aux

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:16):

so you need to do (strong) induction on the input

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:17):

also you might want to try #eval divisors_aux [some number] [some number] to see if you got the function right

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:18):

#eval divisors_aux 12 13 -- [12, 6, 4, 3, 2, 1, 1]

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:19):

#print prefix divisors_aux
/-
divisors_aux : ℕ → ℕ → list ℕ
divisors_aux._main : ℕ → ℕ → list ℕ
divisors_aux._main._meta_aux : ℕ → ℕ → list ℕ
divisors_aux._main.equations._eqn_1 : ∀ (n : ℕ), divisors_aux._main n 0 = list.nil
divisors_aux._main.equations._eqn_2 : ∀ (n : ℕ), divisors_aux._main n 1 = [1]
divisors_aux._main.equations._eqn_3 : ∀ (n n_1 : ℕ),
  divisors_aux._main n (nat.succ n_1 + 1) =
    ite (n % nat.succ n_1 = 0) ([nat.succ n_1] ++ divisors_aux._main n (nat.succ n_1))
      (divisors_aux._main n (nat.succ n_1))
divisors_aux._sunfold : ℕ → ℕ → list ℕ
divisors_aux.equations._eqn_1 : ∀ (n : ℕ), divisors_aux n 0 = list.nil
divisors_aux.equations._eqn_2 : ∀ (n : ℕ), divisors_aux n 1 = [1]
divisors_aux.equations._eqn_3 : ∀ (n n_1 : ℕ),
  divisors_aux n (nat.succ n_1 + 1) =
    ite (n % nat.succ n_1 = 0) ([nat.succ n_1] ++ divisors_aux n (nat.succ n_1)) (divisors_aux n (nat.succ n_1))
-/

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:20):

h+1 and 1 are overlapping cases

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:21):

def divisors_aux (n : ) :   list 
| 0     := []
| (h+1) := if n % h = 0
           then [h] ++ divisors_aux h
           else divisors_aux h

#eval divisors_aux 12 100 -- [12, 6, 4, 3, 2, 1]

#print prefix divisors_aux
/-
divisors_aux : ℕ → ℕ → list ℕ
divisors_aux._main : ℕ → ℕ → list ℕ
divisors_aux._main._meta_aux : ℕ → ℕ → list ℕ
divisors_aux._main.equations._eqn_1 : ∀ (n : ℕ), divisors_aux._main n 0 = list.nil
divisors_aux._main.equations._eqn_2 : ∀ (n h : ℕ), divisors_aux._main n (h + 1) = ite (n % h = 0) ([h] ++ divisors_aux._main n h) (divisors_aux._main n h)
divisors_aux._sunfold : ℕ → ℕ → list ℕ
divisors_aux.equations._eqn_1 : ∀ (n : ℕ), divisors_aux n 0 = list.nil
divisors_aux.equations._eqn_2 : ∀ (n h : ℕ), divisors_aux n (h + 1) = ite (n % h = 0) ([h] ++ divisors_aux n h) (divisors_aux n h)
-/

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:21):

maybe this is what you want

view this post on Zulip Kenny Lau (Oct 30 2019 at 00:21):

also beware of the edge case:

#eval divisors_aux 0 10 -- [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]

view this post on Zulip Lucas Allen (Oct 30 2019 at 01:09):

Ok, I fixed the function so that it doesn't give two ones in the divisors list. But I'm still stuck with simplifying divisors_aux. When I try unfold [divisors_aux p (p+1)] I get the error "unknown identifier 'p'", unfold (divisors_aux p (p+1)), gives the same error. I'm not sure what I'm doing wrong.

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 01:14):

What are you trying to do? Mathematically?

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 01:15):

Can you formalise an intermediate step which you'd like to prove?

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 01:15):

There are two questions -- first what exactly you're trying to do in maths, and then how best to do it in Lean

view this post on Zulip Lucas Allen (Oct 30 2019 at 01:50):

Ultimately, what I want to do is show that the definition

def myprime (p : ) : Prop := (p  2)  divisors p = [1,p]

is equivalent to the definition for prime in mathlib.

To prove the first direction prime p → myprime p, I want to prove

s₂ : (n  p  n = 1  n = p)  divisors p = [1,p]

But I'm stuck. I want to break divisors down into divisors_aux and then break divisors_aux into something I can work with. I'm not sure how to unfold divisors_aux p (p+1), both unfold and dsimp don't seem to work. I don't know if it's a syntax issue or what.

view this post on Zulip Bryan Gin-ge Chen (Oct 30 2019 at 01:52):

Maybe this addresses your question about unfolding. Note that Lean already automatically "sees through" divisors_aux to its definition, no unfolding is required:

example (n : ) : divisors_aux n 0 = [] := rfl

example (m n : ) : divisors_aux m (n+1) = if m % n = 0 then [n] ++ divisors_aux m n else divisors_aux m n := rfl

If you have a goal involving divisors_aux, you can use show to change the goal to a definitionally equivalent expression:

example (m n : ) (l : list ) : divisors_aux m n = l :=
begin
  cases n,
  { -- ⊢ divisors_aux m 0 = l
    show [] = l,
    -- ⊢ list.nil = l
    sorry, },
  { -- ⊢ divisors_aux m (nat.succ n) = l
    show (if _ then _ else _) = l,
    -- ⊢ ite (m % nat.add n 0 = 0) ([nat.add n 0] ++ divisors_aux m (nat.add n 0)) (divisors_aux m (nat.add n 0)) = l
    sorry, },
end

This is sometimes useful for making proofs easier to follow, though in most cases you can delete show without changing the result.

view this post on Zulip Bryan Gin-ge Chen (Oct 30 2019 at 01:56):

So to address your most recent message, you can either just work with divisors_aux p (p+1) as if it were already in the form if _ then _ else _ or you can use the show tactic to make that explicit in the tactic state first.

view this post on Zulip Lucas Allen (Oct 30 2019 at 02:05):

The example

example (m n : ) : divisors_aux m (n+1) = if m % n = 0 then [n] ++ divisors_aux m n else divisors_aux m n := rfl

doesn't work for me. I get a red squiggle under the rfl with the error

type mismatch, term  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  divisors_aux n (h + 1) = ite (n % h = 0) ([h] ++ divisors_aux n h) (divisors_aux n h)"

Is my lean out of date or something?

view this post on Zulip Bryan Gin-ge Chen (Oct 30 2019 at 02:08):

Oh hmm, maybe I'm using a different definition for divisors_aux. Here's the full file:

def divisors_aux (n : ) :   list 
| 0     := []
| (h+1) := if n % h = 0
           then [h] ++ divisors_aux h
           else divisors_aux h

example (n : ) : divisors_aux n 0 = [] := rfl
example (m n : ) : divisors_aux m (n+1) = if m % n = 0 then [n] ++ divisors_aux m n else divisors_aux m n := rfl

view this post on Zulip Bryan Gin-ge Chen (Oct 30 2019 at 02:20):

If you post your new definition of divisors_aux I can update my examples above, but basically if you replace the stuff on the right hand side of the equation with a suitable version of whatever's in the (h+1) case of your new definition, rfl should work. (I say "a suitable version" because you may have to do things like replace divisors_aux h with divisors_aux m n as I did in my example.)

view this post on Zulip Lucas Allen (Oct 30 2019 at 02:24):

The problem was that my definition for divisors_aux had an unnecessary case | 1 := [] in it. It now works. I'm gonna mess around with this for a while. Thanks for the help :).

view this post on Zulip Lucas Allen (Nov 02 2019 at 02:28):

Is it possible to start induction a at 2 instead of 0 if we have the hypothesis a >= 2?

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:29):

If I want a quick and dirty solution to this I just do cases a couple of times before I start. Hang on I'll knock something up.

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:40):

import tactic.linarith

open nat

def induction_from_2 (P :   Prop) (h2 : P 2)
(IH :  d : , 2  d  P d  P (succ d)) (a : ) (ha : 2  a) : P a :=
begin
  cases a with b,
    linarith,
  cases b with c,
    linarith,
  clear ha, -- no longer of any use to us
  -- induction starts here on c=0 with a=c+2
  induction c with d hd,
    assumption,
  apply IH,
    simp [succ_eq_add_one],
  assumption,
end

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:41):

You can just apply that function now

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:41):

if you can't be bothered to fill in an input, just use _ and Lean will try and figure it out.

view this post on Zulip Lucas Allen (Nov 02 2019 at 02:42):

Ok, thanks.

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:44):

If you want more hints about how to steer that function, just post some code and I'll show you how to drop it in.

view this post on Zulip Kenny Lau (Nov 02 2019 at 02:44):

import tactic.solve_by_elim

@[elab_as_eliminator]
lemma nat.induction_from {proposition :   Prop} (start : )
  (proposition_start : proposition start)
  (induction_hypothesis :  d : , start  d  proposition d  proposition (nat.succ d))
  (current : ) (start_le_current : start  current) :
  proposition current :=
by induction start_le_current; solve_by_elim

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:44):

Go Kenny

view this post on Zulip Kenny Lau (Nov 02 2019 at 02:44):

the trick is to actually do induction on the inequality

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:44):

Kenny has proved the general case by induction on the starting point.

view this post on Zulip Kenny Lau (Nov 02 2019 at 02:45):

import tactic.solve_by_elim

@[elab_as_eliminator]
lemma nat.induction_from {P :   Prop} (s : ) (hs : P s)
  (ih :  d : , s  d  P d  P (nat.succ d))
  (n : ) (hsn : s  n) : P n :=
by induction hsn; solve_by_elim

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:46):

@Lucas Allen they are making better and better tools to do this job. They can even turn them into tactics for you.

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:46):

(I don't know how to do that)

view this post on Zulip Kenny Lau (Nov 02 2019 at 02:47):

why are condensed variable names preferred?

view this post on Zulip Lucas Allen (Nov 02 2019 at 02:56):

Oh... so the induction tactic can already handle this problem?

view this post on Zulip Kenny Lau (Nov 02 2019 at 02:58):

yes because \le for nat is defined inductively

view this post on Zulip Lucas Allen (Nov 02 2019 at 02:58):

Cool, thanks.

view this post on Zulip Lucas Allen (Nov 05 2019 at 03:54):

I have the goal

 k  ite (p % h₁_b = 0) ([h₁_b] ++ divisors_aux p h₁_b) (divisors_aux p h₁_b)

and the hypothesis h₁_ih : k ∈ divisors_aux p h₁_b. Is there some way to split the goal into two goals, one where p % h₁_b = 0 is true and one where it's false?

Another problem I have is the goal

  (m : ), m  p  m = 1  m = p

with the hypthoses s₄ : k ∣ p → k = 1 ∨ k = p, and k : ℕ, I tried using revert but it reverts all the hypotheses between k and s₄ . Now I'm wondering if this theorem is even true.

view this post on Zulip Alex J. Best (Nov 05 2019 at 03:57):

You could try the split_ifs tactic, or by_cases h : p % h₁_b = 0

view this post on Zulip Lucas Allen (Nov 05 2019 at 03:58):

That works, thanks.

view this post on Zulip Lucas Allen (Nov 05 2019 at 04:03):

I just figured out the second problem as well. I'm finished with this problem now. :)

view this post on Zulip Kevin Buzzard (Nov 05 2019 at 07:18):

The "goals accomplished" buzz :D Very addictive!


Last updated: May 10 2021 at 00:31 UTC