Reasoning about Lists

Just like numbers, simple facts about list processing functions can sometimes be entirely proven by simplification. For example, the simplification performed by Equal.refl is sufficient for this theorem...

`List.nil`_app (xs: List Nat) : Equal (Concat (List.nil Nat) xs) xs
`List.nil`_app xs = Equal.refl

...this is because the Type "sees" the List.nil and automatically reduces equality just as it does with natural numbers and Nat.zero.

Furthermore, as with numbers, it is sometimes useful to perform a case analysis on the possible forms (empty or non-empty) of an unknown list.

Tl_length_pred (xs: List Nat)         : Equal Nat (Pred (Length xs)) (Length (Tail xs))
Tl_length_pred List.nil               = Equal.refl
Tl_length_pred (List.cons head tail)  = Equal.refl

If the user does not open the cases and uses Equal.refl directly, the Type returns a type error:

- ERROR  Type mismatch

   • Got      : Equal Nat (Nat.pred (Length xs)) (Nat.pred (Length xs)) 
   • Expected : Equal Nat (Nat.pred (Length xs)) (Length (Tail xs)) 

   • Context: 
   •   xs : (List Nat) 

   Tl_length_pred xs = Equal.refl
                       ┬─────────
                       └Here!

Similarly, some theorems require induction for their proofs.

• Micro-Sermon. Simply reading example proof scripts won't get you very far! It's important to work through the details of each one, using the Type and thinking about what each step achieves. Otherwise, it's more or less guaranteed that the exercises won't make sense when you get to them. ( ಠ ʖ̯ ಠ)

Induction on Lists

Proofs by induction on data types like List are a bit less familiar than standard natural number induction, but the idea is equally simple. Each data declaration defines a set of data values that can be constructed using the declared constructors: a boolean can be True or False; a number can be Zero or Succ applied to another number; a list of naturals can be List.nil or List.cons applied to a number and a list.

Moreover, the applications of the declared constructors to each other are the only possible forms that elements of an inductively defined set can have, and this fact directly gives rise to a way of reasoning about inductively defined sets: a number is Zero or else it is Succ applied to a smaller number; a list is List.nil or else it is a List.cons applied to some number and a smaller list, etc. So, if we have in mind some proposition p that mentions a listl and we want to argue that p holds for all lists, we can reason as follows:

• First, show that p is true for l when l is List.nil.
• Then show that p is true for l when l is List.cons n l for some number n and some smaller list l, assuming that p is true for l.

Since larger lists can only be constructed from smaller lists, eventually reaching List.nil, these two arguments together establish the truth of p for all lists l. Here's a concrete example:

Concat_assoc (xs: List Nat) (ys: List Nat) (zs: List Nat) : Equal (Concat (Concat xs ys) zs) (Concat xs (Concat ys zs))
Concat_assoc List.nil                               ys zs = Equal.refl
Concat_assoc (List.cons Nat xs.head xs.tail)        ys zs = 
  let ind = Concat_assoc xs.tail ys zs
  let app = Equal.apply (x => (List.cons xs.head x)) ind
  app

We are given three lists xs, ys, and zs and we check if concatenating xs and ys with zs is equal to concatenating xs with the concatenation of ys and zs.

For this, we check for the case where xs is an empty list, then we receive a reflection that the concatenation is between ys and zs, and it suffices to give an Equal.refl.

Next, we "open up" xs to obtain xs.tail for our induction, and we receive as the objective:

 • Expected: Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs))) 

and our ind variable is:

 • ind: Equal (List Nat) (Concat (Concat xs.tail ys) zs) (Concat xs.tail (Concat ys zs))

it is sufficient to apply a List.cons xs.head on both sides of the equality to obtain the final objective, which is what we do in app:

 • app : Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs)))

NOTE

e Type Check returns types t2, t3, and others generated in the same style, which we can ignore and even delete when comparing the return of variables, as we see in the following case

 • Expected: Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs))) 
 •   app   : Equal (List Nat) (List.cons Nat xs.head (Concat (Concat xs.tail ys) zs)) (List.cons Nat xs.head (Concat xs.tail (Concat ys zs)))

This way it's easier to see that app and Expected are identical, so there's no need to be alarmed when seeing these generated types.

Reversing a list

For a slightly more complicated example of inductive proof about lists, suppose we use Concat to define a list reversal function Rev:

Rev (xs: List Nat)        : List Nat
Rev List.nil              = List.nil Nat
Rev (List.cons head tail) = Concat (Rev tail) [head]

Test_rev1 : Equal (List Nat) (Rev [1n,2n,3n]) [3n,2n,1n]
Test_rev1 = Equal.refl

Test_rev2 : Equal (Rev List.nil) List.nil
Test_rev2 = Equal.refl

Properties of Rev

Now let's prove some theorems about the Rev we just defined. For something a bit more challenging than what we've seen, let's prove that reversing a list doesn't change its length. Our first attempt gets stuck at the successor case...

Rev_length_firsttry (xs: List Nat)              : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length_firsttry List.nil                    = Equal.refl
Rev_length_firsttry (List.cons xs.head xs.tail) =
   let ind = Rev_length_firsttry xs.tail
   ?

The Type Check returns the following goal and context:

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail)
   •   ind  = (Rev_length_firsttry tail) 

   let ind = Rev_length_firsttry tail
      ?
      ┬
      └Here!

Now we have to prove that the length of the concatenation of the reverse of the tail of the list and its head is equal to the successor of the length of the tail, so we'll need to use some other proofs, one of which is that the length of the concatenation of two lists is the same as the sum of the lengths of each of them:

Concat_length (xs: List Nat) (ys: List Nat)  : Equal Nat (Length (Concat xs ys)) (Plus (Length xs) (Length ys))
Concat_length List.nil ys                    = Equal.refl
Concat_length (List.cons xs.head xs.tail) ys =
   let ind = Concat_length xs.tail ys
   let app = Equal.apply (x => (Nat.succ x)) ind
   app

In addition to this proof, we'll use others already proven in previous chapters:

Plus_n_z (n: Nat)     : Equal Nat n (Plus n Nat.zero)
Plus_n_sn (n: Nat) (m: Nat) : Equal Nat (Nat.succ (Plus n m)) (Plus n (Nat.succ m))
Plus_comm (n: Nat) (m: Nat) : Equal Nat (Plus n m) (Plus m n)

And now we can prove our theorem:

Rev_length (xs: List Nat)               : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                     = Equal.refl
Rev_length (List.cons Nat head tail)  =
   let ind   = Rev_length tail
   ?

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail) 
   •   ind  = (Rev_length tail) 

   let ind   = Rev_length tail
      ?
      ┬
      └Here!

We create a variable with our auxiliary Concat_length:

Rev_length (xs: List Nat)             : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                   = Equal.refl
Rev_length (List.cons Nat head tail)  =
   let ind  = Rev_length tail
   let aux1 = Concat_length (Rev xs.tail) [xs.head]
   ?

We receive a new context for our auxiliaries...

 • aux1: Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n)

... the aux1 is equal to the left side of our Expected, so half the work is already done, we just need the other side of the equality and for that we create a new variable, aux2:

let aux2 = Plus_comm (Length (Rev xs.tail)) (1n)

Now our context is even better:

 • aux2: Equal Nat (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) 

As we make progress in our formal proofs, we can see that the left side of aux2 is equal to the right side of aux1, and we can chain them together using Equal.chain:

let chn = Equal.chain aux1 aux2

When we Type Check, we see our new context:

 • chn : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length (Rev tail)))

Nossa variável chn é praticamente idêntica ao nosso Expected só diferindo na parte final, pois Expected espera um Nat.succ (Length xs.tail) e o chn nos dá Nat.succ (Length (Rev xs.tail)), mas nós temos a variável ind que nos retorna essa igualdade. Vamos relembrar:

Our chn variable is practically identical to our Expected, differing only in the final part, since Expected expects a Nat.succ (Length xs.tail) and chn gives us Nat.succ (Length (Rev xs.tail)), but we have the ind variable that returns us this equality. Let's remember:

 • ind: Equal Nat (Length (Rev tail)) (Length tail) 

Incredible, isn't it? It returns exactly what we need, that the size of the reverse of the tail is equal to the size of the tail, so we just need to rewrite the ind variable in our chn:

let rrt = Equal.rewrite ind (x => Equal Nat (Length (Concat (Rev tail) (List.cons head (List.nil)))) (Nat.succ x )) chn

Let's see our new context, only hiding the types for easier reading:

+ INFO  Inspection.

   • Expected: Equal Nat (Length (Concat (Rev tail) (List.cons _ head (List.nil _)))) (Nat.succ (Length tail)) 

   • Context: 
   •   head : Nat 
   •   tail : (List Nat) 
   •   ind  : Equal Nat (Length (Rev tail)) (Length tail) 
   •   ind  = (Rev_length tail) 
   •   aux1 : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n) 
   •   aux1 = (Concat_length (Rev tail) (List.cons Nat head (List.nil Nat))) 
   •   aux2 : Equal Nat (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) 
   •   aux2 = (Plus_comm (Length (Rev tail)) 1n) 
   •   chn  : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length (Rev tail)))
   •   chn  = Equal.chain Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Plus (Length (Rev tail)) 1n) (Nat.succ (Length (Rev tail))) aux1 aux2 
   •   rrt  : Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ (Length tail)) 
   •   rrt  = Equal.rewrite Nat (Length (Rev tail)) (Length tail) ind (x => Equal Nat (Length (Concat (Rev tail) (List.cons Nat head (List.nil Nat)))) (Nat.succ x))) chn

Now it's much easier to see that our rrt is exactly our Expected, so our proof is as follows:

Rev_length (xs: List Nat)            : Equal Nat (Length (Rev xs)) (Length xs)
Rev_length List.nil                  = Equal.refl
Rev_length (List.cons Nat head tail) =
   let ind   = Rev_length tail
   let aux1  = Concat_length (Rev tail) [head]
   let aux2  = Plus_comm (Length (Rev tail)) (1n)
   let chn   = Equal.chain aux1 aux2
   let rrt = Equal.rewrite ind (x => Equal Nat (Length (Concat (Rev tail) [head])) (Nat.succ x)) chn
   rrt

List Exercises, Part 1

List_exercises

Let's practice a little more with lists:

Concat_nil_r (xs: List Nat) : Equal (Concat xs List.nil) xs
Concat_nil_r xs = ?

Concat_assoc (xs: List Nat) (ys: List Nat) (zs: List Nat) : Equal (Concat (Concat xs ys) zs) (Concat xs (Concat ys zs))
Concat_assoc xs ys zs = ?

Rev_app_distr (xs: List Nat) (ys: List Nat) : Equal (Rev (Concat xs ys)) (Concat (Rev ys) (Rev xs))
Rev_app_distr xs ys = ?

Rev_involutive (xs: List Nat) : Equal (Rev (Rev xs)) xs
Rev_involutive xs = ?

There is a short solution to the next one. If you find it too difficult or it starts to get too long, step back and try to find a simpler way.

Concat_assoc4 (l1: List Nat) (l2: List Nat) (l3: List Nat) (l4: List Nat) : Equal (List Nat) (Concat l1 (Concat l2 (Concat l3 l4))) (Concat (Concat (Concat l1 l2) l3) l4)
Concat_assoc4 l1 l2 l3 l4 = ? 

An exercise on your implementation of Nonzeros:

Nonzeros_app (xs: List Nat) (ys: List Nat) : Equal (List Nat) (Nonzeros (Concat xs ys)) (Concat (Nonzeros xs) (Nonzeros ys))
Nonzeros_app xs ys = ?

Beq_NatList

Fill in the definition of beq_NatList, which compares lists of numbers for equality. Prove that beq_NatList xs ys produces Bool.true for each list.

Beq_NatList (xs: List Nat) (ys: List Nat) : Bool
Beq_NatList xs ys = ? 

Test_beq_natlist1 : Equal Bool (Beq_list List.nil List.nil) Bool.true
Test_beq_natlist1 = ?

Test_beq_natlist2 : Equal Bool (Beq_list [1n,2n,3n] [1n,2n,3n]) Bool.true
Test_beq_natlist2 = ?

Test_beq_natlist3 : Equal Bool (Beq_list [1n,2n,3n] [1n,2n,4n]) Bool.false
Test_beq_natlist3 = ?

Beq_natlist_refl (xs: List Nat) : Equal Bool Bool.true (Beq_list xs xs)
Beq_natlist_refl xs = ?

List Exercises, Part 2

Proofs

Prove the following theorem, it will help you in the next proof:

Ble_n_succ_n (n: Nat) : Equal Bool (Lte n (Nat.succ n)) Bool.true
Ble_n_succ_n n = ? 

Prove the following theorem, it will help you in the next proof:

Count_member_nonzero (xs: List Nat) : Equal Bool (Lte 1n (Count 1n (List.cons 1n xs))) Bool.true
Count_member_nonzero xs = ?

Rev_injective

Prove that the Rev function is injective - that is,

Rev_injective (xs: List Nat) (ys: List Nat) (e: Equal (List Nat) (Rev xs) (Rev ys)) :tail Equal (List Nat) xs ys
Rev_injective xs ys e = ?  

Opcional: Count_sum

Write an interesting theorem about Lists involving the functions count and sum, and prove it. (You may find that the difficulty of the test depends on how you set the count!)

Count_sum : ?