Quantifying over an uninhabited type (false/ empty)

Stream: general

[Adam Kurkiewicz]

I'm wondering whether this is something I should be able to prove (I think I should). It came up when I was trying to show that two definitions of primality are equivalent.

Let's say that we have a property, which quantifies over an empty, uninhabited type:

def  impossible_property : Prop  :=
∀ (Pfalse : false), 1  =  1

Is it true that ¬ impossible_property, i.e. how, if at all, can I finish this proof:

def  cant_happen : ¬ impossible_property :=
λ Pimp : impossible_property,
sorry

[Johannes Hölzl]

Its the opposite: impossible_property is always inhabited, it can be easily proved using false.elim.

[Adam Kurkiewicz]

Cheers, indeed:

def  impossible_property : Prop  :=
∀ (Pfalse : false), 1  =  1
def  can_happen_ : impossible_property :=
λ (Pfalse: false),
false.elim Pfalse

[Moses Schönfinkel]

This is better shown with a "ridiculous" example.

lemma exfalso_quod_libet (h : false) : 4 = 2 := false.elim h

[Adam Kurkiewicz]

Thanks Moses,

this is indeed a better example. I'm afraid though that my confusion goes deeper than the initial question.

I've been trying to show that two definitions of primality are equivalent:

def  is_divisible: nat → nat →  Prop  :=
λ n m : nat, ∃ k : nat, m * k = n

def  is_prime1: nat →  Prop  :=
λ p, ∀ (m : nat) (Pmdp : is_divisible p m), ((m =  1) ∨ (m = p)) ∧ (p ≠  1)

def  is_prime2: nat →  Prop  :=
λ p, ∀ (k : nat) (b1 : k < p) (b2 : 1  < k), (¬ is_divisible p k)

Using your example I was able to show that 1 is prime according to the second definition is_prime2:

def  one_is_prime2 : is_prime2 1  :=
λ (k : nat) (x : k <  1) (y : 1  < k),
have a : 1  <  1, from lt.trans y x,
have one_ne_one : 1  ≠  1, from (ne_of_lt a),
false.elim (one_ne_one (eq.refl 1))

This clearly makes is_prime_2 a bad definition of primality, but I really can't see what went wrong.

[Mario Carneiro]

You should look at the definition of prime and equivalent variations in mathlib data.nat.prime

[Mario Carneiro]

Most definitions of prime have to explicitly exclude 1

[Mario Carneiro]

It is true that there are no 1<k<1 such that 1 | k, meaning that 1 is spuriously identified as prime using is_prime2.

[Mario Carneiro]

By the way you probably want p \ne 1 inis_prime1 to come before the forall, otherwise it only applies when there exists an m such that p|m (which is true, but still it's a bit subtle)

[Mario Carneiro]

forall has low binding power, meaning that it extends until it hits a close parenthesis

[Adam Kurkiewicz]

Thanks, this makes sense.

The problem extends to is_prime2 0, since k < 0 → false and we end up with the same problems. Definition of primality in mathlib excludes these cases, just as you pointed out, before the quantifier: def prime (p : ℕ) := p ≥ 2 ∧ ∀ m ∣ p, m = 1 ∨ m = p