## Stream: new members

### Topic: equivalent definitions of prime

#### 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     := 
| (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 (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.

#### 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 =  by induction on a, and then compute divisors p.

#### 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 = , 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 (Oct 30 2019 at 00:16):

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

#### Kenny Lau (Oct 30 2019 at 00:16):

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

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

#### Kenny Lau (Oct 30 2019 at 00:18):

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


#### 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 = 
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 = 
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 (Oct 30 2019 at 00:20):

h+1 and 1 are overlapping cases

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


#### Kenny Lau (Oct 30 2019 at 00:21):

maybe this is what you want

#### 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]


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

#### Kevin Buzzard (Oct 30 2019 at 01:14):

What are you trying to do? Mathematically?

#### Kevin Buzzard (Oct 30 2019 at 01:15):

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

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

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

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

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

#### 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?

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


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

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

#### 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?

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

#### 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,
assumption,
end


#### Kevin Buzzard (Nov 02 2019 at 02:41):

You can just apply that function now

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

Ok, thanks.

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

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


Go Kenny

#### Kenny Lau (Nov 02 2019 at 02:44):

the trick is to actually do induction on the inequality

#### Kevin Buzzard (Nov 02 2019 at 02:44):

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

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


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

#### Kevin Buzzard (Nov 02 2019 at 02:46):

(I don't know how to do that)

#### Kenny Lau (Nov 02 2019 at 02:47):

why are condensed variable names preferred?

#### Lucas Allen (Nov 02 2019 at 02:56):

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

#### Kenny Lau (Nov 02 2019 at 02:58):

yes because \le for nat is defined inductively

Cool, thanks.

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

#### Alex J. Best (Nov 05 2019 at 03:57):

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

#### Lucas Allen (Nov 05 2019 at 03:58):

That works, thanks.

#### Lucas Allen (Nov 05 2019 at 04:03):

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

#### Kevin Buzzard (Nov 05 2019 at 07:18):

The "goals accomplished" buzz :D Very addictive!

Last updated: May 10 2021 at 00:31 UTC