Kind vs Set Theory

The logical core of Coq, the Calculus of Inductive Constructions, differs in some important ways from other formal systems used by mathematicians to write precise and rigorous proofs. For example, in the most popular foundation for mathematics in conventional pen-and-paper, Zermelo-Fraenkel set theory (ZFC), a mathematical object can potentially be a member of many different sets; a term in Kind's logic, on the other hand, is a member of at most one type. This difference often leads to slightly different ways of capturing informal mathematical concepts, but these are largely quite natural and easy to work with. For example, instead of saying that a natural number n belongs to the set of even numbers, we would say in Kind that ev n is true, where ev: Nat -> Type is a property that describes even numbers.

However, there are some cases where translating standard mathematical reasoning to Kind can be both laborious and sometimes even impossible, unless we enrich the core logic with additional axioms. We conclude this chapter with a brief discussion of some of the most significant differences between the two worlds.

Functional Extensionality

The equality statements we have seen so far mainly concern elements of inductive types (Nat, Bool, etc.). But since Kind's equality operator is polymorphic, these are not the only possibilities -- in particular, we can write propositions that assert that two functions are equal to each other:

#![allow(unused)]
fn main() {
Function_equality_ex1 : Equal (Nat.succ 3n) (Nat.succ (Nat.pred 4n))
Function_equality_ex1 = Equal.refl
}

In common mathematical practice, two functions f and g are considered equal if they produce the same outputs:

(∀𝑥, 𝑓(𝑥) = 𝑔(𝑥)) → 𝑓 = 𝑔

This is known as the principle of functional extensionality.

Informally, an "extensional property" is one that concerns the observable behavior of an object. Thus, functional extensionality simply means that the identity of a function is completely determined by what we can observe from it -- that is, in terms of Kind, the results we obtain after applying it.

Functional extensionality is not part of Kind's basic axioms. This means that some "reasonable" propositions are not provable.

#![allow(unused)]
fn main() {
Function_equality_ex2 : Equal ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x)
Function_equality_ex2 = ?
}

However, we can state a theorem and skip its proof or use a hole.

#![allow(unused)]
fn main() {
Functional_extensionality <a><b> (f: a -> b) (g: a -> b) (e: (x: a) -> Equal (f x) (g x)) : Equal f g
}

Now we can invoke functional extensionality in proofs:

#![allow(unused)]
fn main() {
Function_equality_ex2 : Equal ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x)
Function_equality_ex2 =
  Functional_extensionality ((x: Nat) => Nat.add x 1n) ((x: Nat) => Nat.add 1n x) (x => Plus_comm x 1n)
}

Of course, we should be careful when adding new axioms to Kind's logic, as they may make it inconsistent -- that is, they may make it possible to prove all propositions, including Empty!

Unfortunately, there is no simple way to tell whether an axiom is safe to add: it usually takes hard work to establish the consistency of any particular combination of axioms.

However, it is known that adding functional extensionality, in particular, is consistent.

Tr_rev

A problem with the definition of the list reversal function "rev" we have is that it performs a call to "++" at each step. Executing "++" takes asymptotically linear time in the size of the list, which means that "rev" has quadratic running time. We can improve this with the following definition:

#![allow(unused)]
fn main() {
Rev_append <x> (l1: List x) (l2: List x)  : List x
Rev_append x List.nil l2                  = l2
Rev_append x (List.cons xs.h xs.t) l2     = Rev_append xs.t (List.cons xs.h l2)

Tr_rev <x> (l: List x) : List x
Tr_rev x l = Rev_append x l List.nil1
}

This version is said to be tail-recursive, because the recursive call to the function is the last operation that needs to be performed (i.e., we don't need to execute ++ after the recursive call); a decent compiler will generate very efficient code in this case. Prove that the two definitions are actually equivalent.

#![allow(unused)]
fn main() {
Tr_rev_correct <a> (xs: List a) : Equal (Tr_rev xs) (Rev xs)
Tr_rev_correct a xs = ?
}

Propositions and Booleans

We have seen two different ways of encoding logical facts in Kind: with booleans (of type Bool) and with propositions (of type Type).

For example, to assert that a number n is even, we can say that • (1) evenb n returns True, or • (2) there exists a k such that n = double k. In fact, these two notions of parity are equivalent, as can be easily shown with a pair of auxiliary lemmas.

We often say that the boolean evenb n reflects the proposition (n => Equal n (double k)).

#![allow(unused)]
fn main() {
Evenb_double (k: Nat)     : Equal (Nat.is_even (Nat.double k)) Bool.true
Evenb_double Nat.zero     = Equal.refl
Evenb_double (Nat.succ k) = Evenb_double k
}

Evenb_double_conv

#![allow(unused)]
fn main() {
Evenb_double_conv (n: Nat):
  Sigma Nat (k => (Equal n (Bool.if (Evenb n) (Nat.double k) (Nat.succ (Nat.double k)))))
Evenb_double_conv n = ?
}

#![allow(unused)]
fn main() {
Even_bool_prop (n: Nat): 
  Equivalence (Equal (Evenb n) Bool.true) (Sigma Nat (k => Equal n (Nat.double k)))
}

Similarly, to assert that two numbers n and m are equal, we can say (1) that n == m returns Bool.true or (2) that n = m. These two notions are equivalent.

#![allow(unused)]
fn main() {
Beq_nat_true_equiv (n1: Nat) (n2: Nat) : Equivalence (Equal (Nat.equal n1 n2) Bool.true) (Equal n1 n2)
Beq_nat_true_equiv n1 n2 = Equivalence.new (x => To_beq_nat_true n1 n2 x) (y => Fro_beq_nat_true n1 n2 y)

To_beq_nat_true (n1: Nat) (n2: Nat) (e: Equal (Nat.equal n1 n2) Bool.true) : Equal n1 n2  
To_beq_nat_true Nat.zero Nat.zero Equal.refl = Equal.refl
To_beq_nat_true Nat.zero (Nat.succ n2) e = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
To_beq_nat_true (Nat.succ n1) Nat.zero e = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
To_beq_nat_true (Nat.succ n1) (Nat.succ n2) e = Equal.apply (x => Nat.succ x) (Extract_equal n1 n2 e)

Fro_beq_nat_true (n1: Nat) (n2: Nat) (e: Equal  n1 n2) : Equal (Nat.equal n1 n2) Bool.true
Fro_beq_nat_true Nat.zero Nat.zero Equal.refl = Equal.refl
Fro_beq_nat_true Nat.zero (Nat.succ n2) e = 
  let emp = (Equal.rewrite e 
    (x => match Nat x {
      zero => Unit
      succ => Empty
    })
    (Unit.new))
  Empty.absurd emp
Fro_beq_nat_true (Nat.succ n1) Nat.zero e = 
  let emp = (Equal.rewrite e 
    (x => match Nat x {
      zero => Empty
      succ => Unit
    })
    (Unit.new))
  Empty.absurd emp
Fro_beq_nat_true (Nat.succ n1) (Nat.succ n2) e =
  let e2  = Succ_n1_n2 n1 n2 e
  let ind = Fro_beq_nat_true n1 n2 e2
  ind

  Succ_n1_n2 (n1: Nat) (n2: Nat) (e : (Equal Nat (Nat.succ n1) (Nat.succ n2))) : Equal Nat n1 n2
Succ_n1_n2 Nat.zero Nat.zero e            = Equal.refl
Succ_n1_n2 (Nat.succ n1) Nat.zero e       = Equal.apply (x => Nat.pred x) e
Succ_n1_n2 Nat.zero (Nat.succ n2) e       = Equal.apply (x => Nat.pred x) e
Succ_n1_n2 (Nat.succ n1) (Nat.succ n2) e  = Equal.apply (x => Nat.pred x) e

Extract_equal (n1: Nat) (n2: Nat) (e: Equal (Nat.equal n1 n2) Bool.true) : Equal n1 n2
Extract_equal Nat.zero Nat.zero (Equal.refl) = Equal.refl
Extract_equal Nat.zero (Nat.succ n2) (e) = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
Extract_equal (Nat.succ n1) Nat.zero (e) = 
  let emp = (Equal.rewrite e 
    (x => match Bool x {
      true  => Empty
      false => Unit
    })
    (Unit.new))
  Empty.absurd emp
Extract_equal (Nat.succ n1) (Nat.succ n2) e = Equal.apply (x => Nat.succ x) (Extract_equal n1 n2 e)
}

However, while the boolean and propositional formulations of a statement are equivalent from a purely logical point of view, they need not be operationally equivalent. Equality provides an extreme example: knowing that n = m = True is usually of little direct help in the middle of a proof involving n and m; however, if we convert the statement to the equivalent form n = m, we can rewrite it.

The case of even numbers is also interesting. Recall that, when proving the inverse direction of even_bool_prop (i.e., evenb_double, going from the propositional assertion to the boolean one), we used a simple induction on k. On the other hand, the converse (the evenb_double_conv exercise) required some clever generalization, since we cannot directly prove (k => Equal n (Nat.double k)) = Bool.true

For these examples, the propositional assertions are more useful than their boolean counterparts, but this is not always the case. For example, we cannot test whether a general proposition is true or not in a function definition; as a consequence, the following code snippet is rejected:

#![allow(unused)]
fn main() {
Is_even_prime : Nat -> Bool
Is_even_prime = (n: Nat) => Bool.if (Equal n 2n) Bool.true Bool.false
}

Kind complains that n = 2 has type Type, while it expects an element of Bool (or some other inductive type with two elements). The reason for this error message has to do with the computational nature of the core language of Kind, which is designed such that every function it can express is computable and total. One reason for this is to allow for the extraction of executable programs from Kind developments. As a consequence, in Kind, Type does not have a universal case analysis operation that says whether a given proposition is true or false, since such an operation would allow for the writing of non-computable functions.

Although non-computable general properties cannot be formulated as boolean computations, it is worth noting that many computable properties are easier to express using Type than Bool, since recursive function definitions are subject to significant restrictions in Kind. For example, the next chapter shows how to define the property that a regular expression matches a given string using Type. Doing the same with Bool would be equivalent to writing a regular expression checker, which would be more complicated, harder to understand, and harder to reason about.

On the other hand, an important additional benefit of stating facts using booleans is enabling some proof automation through computation with terms in Kind, a technique known as reflection proof. Consider the following statement:

#![allow(unused)]
fn main() {
Even_1000 : Sigma Nat (k => Equal 1000n (Nat.double k))
}

"The most straightforward proof of this fact is to provide the value of k explicitly."

#![allow(unused)]
fn main() {
Even_1000 = $ 500n Equal.refl
}

On the other hand, the proof of the corresponding boolean statement is even simpler:

#![allow(unused)]
fn main() {
Even_1000a : Equal (Evenb 1000n) Bool.true
Even_1000a = Equal.refl
}

"Interestingly, as the two notions are equivalent, we can use the boolean formulation to prove the other without explicitly mentioning the value 500."

#![allow(unused)]
fn main() {
Even_1000b : Sigma Nat (k => Equal 1000n (Nat.double k))
Even_1000b = Sigma.new 500n Equal.refl
}

Although we haven't gained much in terms of proof size in this case, larger proofs can be considerably simplified by using reflection. As an extreme example, the proof of the four-color theorem in Coq uses reflection to reduce the analysis of hundreds of different cases to a boolean computation. We won't delve into reflection in great detail, but it serves as a good example that shows the complementary strengths of booleans and general propositions.

Logical_connectives

The following lemmas relate the propositional connectives studied in this chapter to their corresponding boolean operations.

#![allow(unused)]
fn main() {
Andb_true_equiv 
  (b1: Bool) 
  (b2: Bool) : Equivalence (Equal (Bool.and b1 b2) Bool.true) (Pair (Equal b1 Bool.true) (Equal b2 Bool.true))
Andb_true_equiv b1 b2 = ?


Orb_true_equiv 
  (b1: Bool) 
  (b2: Bool): Equivalence (Equal (Bool.or b1 b2) Bool.true) (Either (Equal b1 Bool.true) (Equal b2 Bool.true))
Orb_true_equiv b1 b2 = ?
}

Beq_nat_false_equiv

The following theorem is an alternative "negative" formulation of beq_nat_true_equiv that is more convenient in certain situations (we will see examples in later chapters).

#![allow(unused)]
fn main() {
Beq_nat_false_equiv (n1: Nat) (n2: Nat) : Equivalence (Equal (Nat.equal n1 n2) Bool.false) (Not (Equal n1 n2))
Beq_nat_false_equiv n1 n2 = ?
}

Beq_list

Given a boolean operator beq to test the equality of elements of some type a, we can define a function beq_list beq to test the equality of lists with elements in a. Complete the definition of the function beq_list below. To ensure that your definition is correct, prove the theorem beq_list_true_equiv.

#![allow(unused)]
fn main() {
Beq_list <a> (beq: a -> a -> Bool) (xs: List a) (ys: List a) : Bool
Beq_list a beq  xs ys = ?

Beq_list_true_equiv <a> 
  (beq: a -> a -> Bool) 
  (a1: a) 
  (a2: a) 
  (e: Equivalence (Equal (beq a1 a2) Bool.true) (Equal a1 a2))
  (xs: List a)
  (ys: List a): Equivalence (Equal (Beq_list beq xs ys) Bool.true) (Equal xs ys)
Beq_list_true_equiv a beq a1 a2 e xs ys = ?
}

All_forallb

#![allow(unused)]
fn main() {
Forallb <x> (t: x -> Bool) (xs: List x) : Bool
Forallb x t List.nil = Bool.true
Forallb x t (List.cons xs.h xs.t) = Bool.and (t xs.h) (Forallb t xs.t)

}

Prove the theorem below, which relates forallb to the property All from the above exercise.

#![allow(unused)]
fn main() {
Forallb_true_equiv <x> 
  (t: x -> Bool) 
  (xs: List x) : 
  Equivalence (Equal (Forallb t xs) Bool.true) ((All ((k: x) => Equal (t k) Bool.true) xs))
Forallb_true_equiv x t xs = ?
}

Are there any important properties of the function forallb that are not captured by this specification?