Applying Theorems to Arguments

A characteristic of Kind that distinguishes it from many other proof assistants is that it treats proofs as first-class objects.

There is much to be said about this, but it is not necessary to understand in detail to use Kind. This section offers only a sample, while a deeper exploration can be found in the ProofObjects chapter.

We saw that we can use the check command to ask Kind to print the type of an expression. We can also use check to ask which theorem a particular identifier refers to.

PlusCommutative (m: Nat) (n: Nat) : Equal (Nat.add n m) (Nat.add m n)
PlusCommutative m n = ?

Kind prints the statement of the plusCommutative theorem in the same way it prints the type of any term we ask it to check. Why?

The reason is that the identifier plusCommutative actually refers to a proof object - a data structure that represents a logical derivation establishing the truth of the statement (n: Nat) (m: Nat) : n + m = m + n. The type of this object is the statement of the theorem of which it is a proof. Intuitively, this makes sense because the statement of a theorem tells us what we can use it for, just as the type of a computational object tells us what we can do with that object - for example, if we have a term of type Nat -> Nat -> Nat, we can give it two Nats as arguments and get a Nat back. Similarly, if we have an object of type n = m -> n + n = m + m and provide it with an "argument" of type n = m, we can derive n + n = m + m. Operationally, this analogy goes even further: by applying a theorem, as if it were a function, to hypotheses with corresponding types, we can specialize its result without having to resort to intermediate assertions. For example, suppose we wanted to prove the following result:

Plus_comm3a: (n: Nat) (m: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)

At first glance, it seems like we should be able to prove this by case analysis, for the zero and succ _ cases, but that would give us unnecessary work. Let's see an example:

Plus_comm3a Nat.zero n p = ?

In this case, our goal is to prove:

(Equal _ (Nat.add n p) (Nat.add (Nat.add p 0n) n)) 

But notice, for this we need another proof, that of

Equal Nat (Nat.add p 0n) p

To prove this, we would take the following steps:

Add_n_z (n: Nat)       : (Equal (Nat.add n Nat.zero) n)
Add_n_z Nat.zero       = Equal.refl
Add_n_z (Nat.succ n)   =
     let ind = Add_n_z n
     let app = (Equal.apply (x => (Nat.succ x)) ind)
     app

Now let's prove:

Plus_comm3a (n: Nat) (m: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)
Plus_comm3a Nat.zero n p = 
  let pzr = Add_z_r p
  let com = Plus_comm n p
  let rwt = Equal.rewrite (Equal.mirror pzr) (x =>(Equal _ (Nat.add n p) (Nat.add (x) n))) com
  rwt

Now we only need to prove it for the case of Nat.succ n

Plus_comm3a (Nat.succ m) n p = ?

and our goal is (Equal _ (Nat.succ (Nat.add m (Nat.add n p))) (Nat.add (Nat.add p n) (Nat.succ m))) and for that we would need other proofs, such as the one that

Plus_n_sm (n: Nat) (m: Nat) : (Equal Nat (Nat.succ (Nat.add n m))(Nat.add n (Nat.succ m)))
Plus_n_sm Nat.zero m        = Equal.refl
Plus_n_sm (Nat.succ n) m    = (Equal.apply (x => (Nat.succ x)) (Plus_n_sm n m))

And rewrite in the proof of the commutativity of addition between n and p and then use the proof of commutativity for all of this, a tiring and, I can say, unnecessary job.

Instead of doing case analysis, let's work with them as pure variables, almost without value

Plus_comm3 (m: Nat) (n: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)
Plus_comm3 m n p = ?

Our goal remains (Equal _ (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)) and to understand this, let's analyze our problem and the next steps will be too trivial:

• n + (m + p) = (p + m) + n

This is exactly the commutativity of addition, so we just need to rewrite our Plus_comm proof twice, one inside the other

let a = Equal.rewrite (Plus_comm p m) (x => (Equal (Nat.add n (Nat.add m p)) (Nat.add (x) n))) (Plus_comm3 m n p)

and see what our variable a returns

(Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (Nat.add m p) n))

We're almost there, we just need to rewrite the second Plus_comm in the innermost addition on the right-hand side

let b = Equal.rewrite (Plus_comm m p) (x => (Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (x) n))) a

and our b is exactly equal to our goal

(Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)) 

The complete proof is:

Plus_comm3 (m: Nat) (n: Nat) (p: Nat) : Equal (Nat.add n (Nat.add m p)) (Nat.add (Nat.add p m) n)
Plus_comm3 m n p = 
  let a = Equal.rewrite (Plus_comm p m) (x => (Equal (Nat.add n (Nat.add m p)) (Nat.add (x) n))) (Plus_comm3 m n p)
  let b = Equal.rewrite (Plus_comm m p) (x => (Equal Nat (Nat.add n (Nat.add m p)) (Nat.add (x) n))) a
  b

Much simpler and more elegant, it didn't require so much work, a brief reading of the problem practically gave us the solution. Notice that this was no different from everything we have done so far, it is even a repetition of the previous steps, it is similar to the application of a polymorphic function to an argument of type.

You can "use theorems as functions" in this way with almost all tactics that receive a theorem name as an argument. Note also that theorem application uses the same inference mechanisms as function application; therefore, it is possible, for example, to provide wildcards as arguments to be inferred, or declare some hypotheses of a theorem as implicit by default. These features are illustrated in the proof below.