# Zulip Chat Archive

## 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 := [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 = [1]`

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 = [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 (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 = [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 (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, simp [succ_eq_add_one], 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.

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

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

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

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

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

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