equivalent definitions of prime

Stream: new members

[Lucas Allen]

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?

[Reid Barton]

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.

[Reid Barton]

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.

[Lucas Allen]

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?

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

#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))
-/

[Kenny Lau]

h+1 and 1 are overlapping cases

[Kenny Lau]

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)
-/

[Kenny Lau]

maybe this is what you want

[Kenny Lau]

also beware of the edge case:

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

[Lucas Allen]

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.

[Kevin Buzzard]

What are you trying to do? Mathematically?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Lucas Allen]

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.

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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.

[Lucas Allen]

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?

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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.)

[Lucas Allen]

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 :).

[Lucas Allen]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

You can just apply that function now

[Kevin Buzzard]

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

[Lucas Allen]

Ok, thanks.

[Kevin Buzzard]

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.

[Kenny Lau]

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

[Kevin Buzzard]

Go Kenny

[Kenny Lau]

the trick is to actually do induction on the inequality

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(I don't know how to do that)

[Kenny Lau]

why are condensed variable names preferred?

[Lucas Allen]

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

[Kenny Lau]

yes because \le for nat is defined inductively

[Lucas Allen]

Cool, thanks.

[Lucas Allen]

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.

[Alex J. Best]

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

[Lucas Allen]

That works, thanks.

[Lucas Allen]

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

[Kevin Buzzard]

The "goals accomplished" buzz :D Very addictive!