Inferring decidability

Stream: general

[Bolton Bailey]

The following mwe comes from some experiments we were running on the speed of the Miller-Rabin test. Lean has no trouble figuring out that equality on zmod is decidable when evaluating fast_strong_probable_prime, but it somehow won't infer this when evaluating fermat_strong_probable_prime. Why is this? In fact, why is it even necessary to write or.decidable to prove fast_strong_probable_prime is decidable? Shouldn't the typeclass inference system know this already without having to be told?

import data.zmod.basic

def binpow {M} [has_one M] [has_mul M] (m : M) : ℕ → M :=
nat.binary_rec 1 (λ b _ ih, let ih2 := ih * ih in cond b (m * ih2) ih2)

def fast_two_multiplicity : ℕ → ℕ :=
nat.binary_rec 0 (λ b _ ih, cond b 0 (ih+1))

def fast_odd_part (n : ℕ) := n / (2 ^ fast_two_multiplicity n)

def fast_strong_probable_prime (n : nat) (a : zmod n) : Prop :=
binpow a (fast_odd_part (n-1)) = 1
∨ (∃ r : ℕ, r < fast_two_multiplicity (n-1) ∧ binpow a (2^r * fast_odd_part(n-1)) = -1)

def fermat_strong_probable_prime (n : nat) (a : zmod n) : Prop :=
binpow a (n-1) = 1

instance {n : ℕ} {a : zmod n} : decidable (fast_strong_probable_prime n a) := or.decidable

#eval to_bool (fast_strong_probable_prime 1241213 3)

-- instance {n : ℕ} {a : zmod n} : decidable (fermat_strong_probable_prime n a) := sorry

#eval to_bool (fermat_strong_probable_prime 1241213 3)

[Kyle Miller]

Definitions are by default semireducible, and semireducible definitions aren't unfolded during typeclass inference. If you unfold it yourself, then it's able to infer it automatically:

instance {n : ℕ} {a : zmod n} : decidable (fast_strong_probable_prime n a) :=
by { unfold fast_strong_probable_prime, apply_instance }

When you do or.decidable, what's happening is that the elaborator unfolds the definition for you since during unification semireducible definitions are unfolded as needed.

[Kyle Miller]

If you make the definition reducible, then typeclass inference will unfold the definition if needed:

@[reducible]
def fast_strong_probable_prime (n : nat) (a : zmod n) : Prop :=
binpow a (fast_odd_part (n-1)) = 1
∨ (∃ r : ℕ, r < fast_two_multiplicity (n-1) ∧ binpow a (2^r * fast_odd_part(n-1)) = -1)

#eval to_bool (fast_strong_probable_prime 1241213 3)

[Kyle Miller]

Both of these methods adapt for the last #eval. Here's creating a decidable instance by unfolding:

instance {n : ℕ} {a : zmod n} : decidable (fermat_strong_probable_prime n a) :=
by { unfold fermat_strong_probable_prime, apply_instance }

#eval to_bool (fermat_strong_probable_prime 1241213 3)

[Kyle Miller]

You can also avoid this by making your functions be bool-valued:

def fast_strong_probable_prime (n : nat) (a : zmod n) : bool :=
binpow a (fast_odd_part (n-1)) = 1
∨ (∃ r : ℕ, r < fast_two_multiplicity (n-1) ∧ binpow a (2^r * fast_odd_part(n-1)) = -1)

def fermat_strong_probable_prime (n : nat) (a : zmod n) : bool :=
binpow a (n-1) = 1

#eval fast_strong_probable_prime 1241213 3

#eval fermat_strong_probable_prime 1241213 3

There's a coercion from bool to Prop so you can still use these inside propositions.

#eval to_bool (fast_strong_probable_prime 1241213 3 ∨ fermat_strong_probable_prime 1241213 3)