boolean indicator function

Stream: new members

[Alex Kontorovich]

Really stupid question: why doesn't this work?

def divides (d n :ℕ)  := ∃ ℓ , n=d*ℓ

def is_prime : ℕ → bool
    := λ p:ℕ ,
        (
            (2 ≤ p)
            ∧
            (∀ m:ℕ , 2≤ m → divides m p →   m = p)
        )

(Something about decidability?...) Thanks!

[Kevin Buzzard]

import tactic

open_locale classical


def divides (d n :ℕ)  := ∃ ℓ , n=d*ℓ

noncomputable def is_prime : ℕ → bool
    := λ p:ℕ ,
        (
            (2 ≤ p)
            ∧
            (∀ m:ℕ , 2≤ m → divides m p →   m = p)
        )

[Kevin Buzzard]

It is computable, and things are decidable, but you would have to prove this before you can get rid of the CS boilerplate

[Kevin Buzzard]

Probably for Lean's actual definition of divides, this is done

[Kevin Buzzard]

But this is better:

def divides (d n :ℕ)  := ∃ ℓ , n=d*ℓ

def is_prime : ℕ → Prop
    := λ p:ℕ ,
        (
            (2 ≤ p)
            ∧
            (∀ m:ℕ , 2≤ m → divides m p →   m = p)
        )

[Jalex Stark]

if you're just doing math, you probably want a Prop instead of bool

[Jalex Stark]

def is_prime (p : ℕ) : Prop :=
2 ≤ p ∧ (∀ m : ℕ, 2 ≤ m → divides m p → m = p)

[Kevin Buzzard]

Actually defining a function to bool forces Lean to try and figure out an algorithm

[Alex Kontorovich]

Ok but then how do I make an indicator function?

def is_prime_f : ℕ → ℝ
    := λ (n:ℕ ), if (is_prime n) then 1 else 0

[Kevin Buzzard]

Back to open_locale classical

[Jalex Stark]

import data.real.basic

open_locale classical
noncomputable theory

def divides (d n :ℕ)  := ∃ ℓ , n=d*ℓ
def is_prime (p : ℕ) : Prop := (2 ≤ p) ∧ (∀ m:ℕ , 2≤ m → divides m p → m = p)
def is_prime_f : ℕ → ℝ
    := λ (n:ℕ ), if (is_prime n) then 1 else 0

[Jalex Stark]

i needed to also add noncomputable theory

[Jalex Stark]

but this is where it tops out, once you have both of these, lean shouldn't ask you about decidability or excluded-middle stuff unless you mention them

[Jalex Stark]

(i really do recommend putting the argument to the left of the colon, it helps readability a lot

[Scott Olson]

I think you could have a generalized def indicator (p : Prop) [decidable p] : ℝ := if p then 1 else 0. If you use classical this will accept any proposition.

[Scott Morrison]

We have talked previously about adding def boole with exactly this definition. But I think the if statement is short and clear so it hasn't happened.