Using Evidence in Proofs

In addition to constructing evidence that numbers are even, we can also reason about such evidence. Introducing Ev with a data statement tells Kind not only that the constructors ev_z and ev_ss are valid ways to construct evidence that a number is even, but also that these two constructors are the only ways to construct evidence that numbers are even (in the sense of Ev).

In other words, if someone gives us evidence and claims it to be of the form Ev n, then we know that e must have one of two forms:

e is ev_z (and n is Nat.zero), or
e is ev_ss applied to induction with n and it is equal to the successor of the successor of n*.

We've already used this strategy before, remember the Problems.t3 exercise from the induction chapter, here the difference is that there's only one more "Nat.succ" in our induction

This suggests that it should be possible to analyze a hypothesis of the form Ev n in the same way we do with data structures defined inductively; in particular, it should be possible to argue by induction and case analysis on this evidence. Let's see some examples to understand what this means in practice.

Pattern Matching on Evidence

Suppose we are proving some fact involving a number n and we are given the hypothesis Ev n. We already know how to perform case analysis on n using the inversion tactic, generating separate subgoals for the case where n = Nat.zero and the case where n = Nat.succ n for some n. But for some proofs, we may want to directly analyze the evidence that Ev n is true.

By the definition of Ev, there are two cases to consider:

If the evidence is of the form ev_z, we know that n = Nat.zero.
Otherwise, the evidence must have the form ev_ss n e, where n = Nat.succ (Nat.succ n) and e is the evidence for Ev n.

We can reason about this kind of pattern matching in Kind, again using pattern matching. In addition to allowing us to reason about equalities involving constructors, inversion provides a principle of case analysis for propositions defined inductively.

Ev_minus2 (n: Nat) (e: Ev n) : Ev (Nat.pred (Nat.pred n))
Ev_minus2 Nat.zero e = e
Ev_minus2 (Nat.succ Nat.zero) e = Ev.ev_z
Ev_minus2 (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = e

In words, here is how the pattern matching reasoning works in this proof:

If the evidence is of the form ev_z, we know that n = Nat.zero. Therefore, it is sufficient to show that Ev (Nat.pred (Nat.pred Nat.zero)) is valid. By the definition of Nat.pred, this is equivalent to showing that Ev Z is valid, which follows directly from ev_0.
Otherwise, the evidence must have the form ev_ss n e, where n = Nat.succ (Nat.succ n) and e is the evidence for Ev n. We must then show that Ev (Nat.pred (Nat.pred (Nat.succ (Nat.succ n)))) is valid, which, after simplification, follows directly from e.

Evss_ev (n: Nat) (e: Ev (Nat.succ (Nat.succ n))) : Ev n

Intuitively, we know that the evidence for the hypothesis cannot consist solely of the constructor ev_z, since Nat.zero and Nat.succ are different constructors of the type Nat; therefore, ev_ss is the only applicable case. Unfortunately, pattern matching is not smart enough to realize this and still generates two subgoals. Even worse, by doing so, it leaves the final goal unchanged, failing to provide any useful information to complete the proof.

The inversion tactic, on the other hand, can detect (1) that the first case does not apply and (2) that the n appearing in the Ev_SS case must be the same as n. This allows us to conclude the proof.

Evss_ev n (Ev.ev_ss e) = e

Using dependent pattern matching, we can also apply the principle of explosion to "obviously contradictory" hypotheses involving inductive properties. For example:

One_not_even : Not (Ev 1n)

Inversion_practice

Prove the following results using pattern matching.

Ssssev__even (n: Data.Nat) (e: Ev (Data.Nat.succ (Data.Nat.succ (Data.Nat.succ (Data.Nat.succ n))))) : Ev n
Ssssev__even n e = ?

Even5_nonsense (e: Ev 5n) : Prop.Equal (Data.Nat.add 2n 2n) 9n
Even5_nonsense e = ?

The way we use inversion here may seem a bit mysterious at first. So far, we have only used inversion on equality propositions to make use of the injectivity of constructors or to discriminate between different constructors. But we see here that inversion can also be applied to analyze evidence of inductively defined propositions.

Here is how inversion works in general. Suppose the name I refers to an assumption P in the current context, where P was defined by an Inductive statement. Then, for each of the constructors of P, inversion of I generates a subgoal in which I has been replaced by the exact and specific conditions under which this constructor could have been used to prove P. Some of these subgoals will be self-contradictory; inversion discards those. The ones that are left represent the cases that must be proven to establish the original goal. For these, inversion adds all the equations to the proof context that must hold true for the arguments supplied to P (e.g., Nat.succ (Nat.succ k) = n in the proof of evSS_ev).

The exercise ev_double above shows that our new notion of evenness is implied by the two previous ones (since, by even_bool_prop in the Logic chapter, we already know they are equivalent to each other). To show that the three coincide, we just need the following lemma:

Ev_even
  (n: Nat)
  (e: Ev n) :
  (Sigma Nat (k => Prop.Equal n (Nat.double k)))
Ev_even n e = ?

We proceed by case analysis on Ev n. The first case can be resolved trivially.

Ev_even Nat.zero e = Sigma.new 0n Equal.refl

Unfortunately, the second case is more challenging. We need to show [k: Nat] -> (Equal (Nat.succ (Nat.succ n')) (Nat.double k)), but the only assumption available is e', which states that Ev n' is true. Since this is not directly useful, it seems like we are stuck and that the case analysis on Ev n was a waste of time.

Ev_even (Nat.succ Nat.zero) e = Empty.absurd _ //todo

If we take a closer look at our second goal, however, we can see that something interesting happened: by performing case analysis on Ev n, we were able to reduce the original result to a similar one that involves a different evidence for Ev n: e'. More formally, we can conclude our proof by showing that

Ev_even (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = Ev_even_ss n (Ev_even n e)

which is the same as the original statement, but with n' instead of n. In fact, it is not difficult to convince Kind that this intermediate result is sufficient.

Ev_even (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = Ev_even_ss n (Ev_even n e)

Induction on Evidence

If this seems familiar, it's no coincidence: we encountered similar problems in the Induction chapter when trying to use case analysis to prove results that required induction. And once again, the solution is... induction!

Let's try our current lemma again:

Ev_even
  (n: Nat)
  (e: Ev n) :
  (Sigma Nat(k => Equal n ( Nat.double k)))
Ev_even Nat.zero e = Sigma.new 0n Equal.refl
Ev_even (Nat.succ Nat.zero) e = Empty.absurd _
Ev_even (Nat.succ (Nat.succ n)) (Ev.ev_ss e) = Ev_even_ss n (Ev_even n e)
// Ev_even (Nat.succ (Nat.succ n)) Ev.ev_z = Caso impossível

The equivalence between the second and third definitions of evenness now follows.


Ev_even_equiv (n: Nat)  : Equivalence (Ev n) (Sigma Nat (k => Equal n (Nat.double k)))
Ev_even_equiv n         = Equivalence.new (x => Ev_even n x) (y => From_eee n y)

From_eee (n: Nat) (s: Sigma Nat (k => Equal n (Nat.double k))) : Ev n
From_eee n (Sigma.new a b fst snd) =
  Equal.rewrite (Equal.mirror (specialize b into #0 in snd)) (x =>(Ev x)) (Ev_double fst)

Ev_double (n: Nat)      : Ev (Nat.double n)
Ev_double Nat.zero      = Ev.ev_z
Ev_double (Nat.succ n)  = Ev.ev_ss (Ev_double n)

As we will see in the upcoming chapters, induction on evidence is a recurring technique in various areas, especially in the formalization of programming language semantics, where many properties of interest are defined inductively.

The following exercises provide simple examples of this technique to help you become familiar with it.

Ev_sum

Ev_sum (n: Nat) (m: Nat) (e1: Ev n) (e2: Ev m) : Ev (Nat.add n m)
Ev_sum n m e1 e2 = ?

Ev_alternate

In general, there can be multiple ways to define a property inductively. For example, here is an alternative (somewhat forced) definition for Ev:

type Evn ~ (n: Nat){
  z : Evn Nat.zero
  d : Evn (Nat.succ (Nat.succ Nat.zero))
  sum <n : Nat> <m: Nat> (evn: Evn n) (evm: Evn m) : Evn (Nat.add n m)
}

Prove that this definition is logically equivalent to the old one. (You may want to refer to the previous theorem when you reach the induction step.)

Ev_evn (n: Nat): Equivalence (Ev n) (Evn n)
Ev_evn n = ?

Ev_ev__ev

Finding the appropriate thing to induct on is a bit tricky here:


Ev_ev_ev (n: Nat) (m: Nat) (e: Ev (Nat.add n m)) (en: Ev n) : Ev m
Ev_ev_ev Nat.zero m e en = ?

Ev_plus_plus

This exercise only requires the application of existing lemmas. No induction or even case analysis is needed, although some of the rewrites may be tedious.

Ev_pp 
  <n: Nat> 
  <m: Nat> 
  <p: Nat> 
  (e1: Ev (Nat.add n m))
  (e2: Ev (Nat.add n p))
  : Ev (Nat.add m p)
Ev_pp Nat.zero m p e1 e2 =
``