Case Study: Improving Reflection

In the Logic chapter, we saw that we often need to relate Boolean computations to Type statements. However, performing this conversion as we did there can result in tedious proof scripts. Consider the proof of the following theorem:

filter_not_empty_In : {n : Nat} -> Not (filter ((==) n) l = []) -> In n l //terminar

In the second case, we explicitly apply the beq_nat_true lemma to the equation generated when doing a dependent match on n == x, to convert the assumption n == x = Bool.true into n = m.`

We can simplify this by defining an inductive proposition that provides a better case analysis principle for n == m. Instead of generating an equation like n == m = Bool.true, which is often not directly useful, this principle immediately gives us the assumption we actually need: n = m.

In fact, we will define something slightly more general, which can be used with arbitrary properties (not just equalities):

type Reflect  (p: Type) (b: Bool) { //TODO: corrigir
  ReflectT    (p: Type) (b = True) : Reflect p b
  ReflectF    (p: Type) (n: Not p) (b = False) : Reflect p b
}

The "reflect" property takes two arguments: a proposition p and a Boolean b. Intuitively, it states that the property p is reflected in (i.e., equivalent to) the Boolean b: p is true if and only if b = Bool.true. To understand this, note that by definition, the only way to obtain evidence that "Reflect p True" is true is by showing that p is true and using the "ReflectT" constructor. If we reverse this statement, it means that it should be possible to extract evidence for p from a proof of "Reflect p True". Similarly, the only way to show "Reflect p False" is by combining evidence of "Not p" with the "ReflectF" constructor.

It is easy to formalize this intuition and show that the two statements are indeed equivalent:

Equiv_reflect <b: Bool> (e: Equiv p  (b = True)) : Reflect p b
Equiv_reflect Bool.false (pb, _) = ReflectF (uninhabited . pb) Equal.refl
Equiv_reflect Bool.true (_, bp)  = ReflectT (bp Refl) Equal.refl

Reflect_equiv

Reflect_equiv (r: Reflect p b) : Equivalence p  (Bool.equal b Bool.true)
Reflect_equiv x = ?

The advantage of "Reflect" over the usual "if and only if" connective is that when we destruct a hypothesis or lemma of the form "Reflect p b", we can perform a case analysis on b while simultaneously generating appropriate hypotheses in both branches (p in the first subgoal and Not p in the second).

Beq_natP <n: Nat> <m : Nat> :  Reflect (Equal n m) (Nat.equal n m)
Beq_natP {n} {m} = iff_reflect (iff_sym (beq_nat_true_iff n m))

The new proof of filter_not_empty_In now proceeds as follows. Notice how the calls to destruct and apply are combined into a single destruct call.

(To see this clearly, compare the two proofs of filter_not_empty_In with Kind and observe the differences in the proof state at the beginning of the first case of destruct.)

Filter_not_empty_In_ <n : Nat> <n: Not (filter ((x => y => Nat.equal x y) n) l = []) : In n l

Beq_natP_practice

Use beq_natP, as mentioned above, to prove the following:

Count (n : Nat) : (l : List Nat) : Nat
Count n List.nil = 0n
Count n (List.cons xs.h xs.t) = Nat.add (Bool.if (Nat.equal n xs.h) 1n 0n)  (Count n xs.t)

Beq_natP_practice (e: Equal (count n l) Nat.zero) : Not (In n l)
Beq_natP_practice e = ? 

Indeed, this technique provides us with only a small convenience advantage for the proofs we have seen here, but using "Reflect" consistently often results in noticeably shorter and clearer proof scripts as the proofs grow larger. We will see many more examples in the upcoming chapters.

The use of the "reflect" property was popularized by SSReflect, a Coq library that has been used to formalize important results in mathematics, including the Four Color Theorem and the Feit-Thompson Theorem. The name SSReflect stands for "small-scale reflection," which refers to the widespread use of reflection to simplify small proof steps involving Boolean computations.