Falsehood and Negation

Up until now, we have mainly been concerned with proving that certain things are true - addition is commutative, list concatenation is associative, etc. Of course, we may also be interested in negative results, showing that certain propositions are not true. In Kind, such negative statements are expressed with the negation type-level function Not.

To see how negation works, recall the discussion of the principle of explosion from the previous chapter; it states that if we assume a contradiction, then any other proposition can be derived. Following this intuition, we could define Not p as q -> (p -> q). Kind actually makes a slightly different choice, defining Not as p -> Empty, where Empty is a specific contradictory proposition defined in the standard library as a data type with no constructors.

Empty: Type

Not <p: Type>: Type
Not p = p -> Empty

Since Empty is a contradictory proposition, the principle of explosion also applies to it. If we obtain Empty in the proof context, we can call it Empty or absurd to complete any goal:

Ex_falso_quodlibet <p> : Empty -> p
Ex_falso_quodlibet p   = e => Empty.absurd e

The Latin phrase ex falso quodlibet literally means "from falsehood, anything follows"; this is another common name for the principle of explosion.

Not_implies_our_not

Show that the definition of negation in Kind implies the intuitive one mentioned above:

Not_implies_our_not <p> <q> (e: Not p) : q -> (p -> q)
Not_implies_our_not p q e = ?

This is how we use Not to assert that 0 and 1 are different elements of Nat:

Zero_not_one : Not (Equal Nat.zero (Nat.succ Nat.zero))
Zero_not_one = 
  (emp => 
    let app = Equal.apply (x => Nat.is_zero x) emp
    Equal.rewrite app (e => if e {Nat} else {Empty}) Nat.zero)

It takes a bit of practice to get used to working with negation in Kind. Even if you can see perfectly well why a statement involving negation is true, it can be a bit tricky at first to get things set up in the right way so that Kind can understand! Here are proofs of some familiar facts to warm you up:

Not_false : Not Empty
Not_false = e => Empty.absurd e

Contradiction_implies_anythig <p> <q> (a: Pair p (Not p)) : q
Contradiction_implies_anythig p q (Pair.new fst snd) =
  let app = snd fst
  Empty.absurd app

Double_neg_inf

Write an informal proof of Double_neg:

Theorem: If p, then (not (not p)), for any proposition p.

Contrapositive

Contrapositive <p> <q> (f: p -> q) : (Not q -> Not p)
Contrapositive p q f = ?

Not_both_true_and_false

Not_both_true_and_false <p> : Not (Pair p (Not p))
Not_both_true_and_false p = ?

Similarly, since inequality involves negation, it takes a bit of practice to work with it fluently. Here's a useful trick. If you're trying to prove a goal that is absurd (e.g., the final state is Bool.false = Bool.true), apply Empty.absurd to change the goal to Empty. This makes it easier to use assumptions of the form (Not p) that may be available in the context - in particular, assumptions of the form Not (x = y).

Not_true_is_false (b: Bool) (e: Not (Equal Bool b Bool.true)) : Equal Bool b Bool.false
Not_true_is_false Bool.false e = Equal.refl
Not_true_is_false Bool.true e = Empty.absurd (e Equal.refl)