The goal of this study is to investigate lists and primitive iteration in tCPA.
Lists are implemented in the List library, which we should start by importing:
Require Import List.
From then on, we can have access to the empty list nil and the list constructor List.cons, abbreviated into the infix notation ::.
Lists are polymorphic, in that we can construct, e.g., lists of natural numbers, lists of Booleans, lists of lists of natural numbers, etc.:
Here is a polymorphic function to construct a singleton list:
Definition make_singleton_list (V : Type) (v : V) : list V :=
v :: nil.
For example,
to construct the singleton list of natural numbers containing 42, one applies make_singleton_list to the type nat and the natural number 42:
Compute (make_singleton_list nat 42).
and to construct the singleton list of Booleans containing true, one applies make_singleton_list to the type bool and the Boolean true:
Compute (make_singleton_list bool true).
Note how the type is an explicit argument in make_singleton_list and how it is implicit when using nil and ::.
To compare two polymorphic lists of values, we need a predicate for comparing these values. Hence the following implementation that is parameterized both by a type and by a predicate for comparing values at that type:
Fixpoint eqb_list (V : Type) (eqb_V : V -> V -> bool) (v1s v2s : list V) : bool :=
match v1s with
nil =>
match v2s with
nil =>
true
| v2 :: v2s' =>
false
end
| v1 :: v1s' =>
match v2s with
nil =>
false
| v2 :: v2s' =>
eqb_V v1 v2 && eqb_list V eqb_V v1s' v2s'
end
end.
This function is defined by structural induction over lists, with a base case (nil) and an induction step (::).
Prove the soundness and the completeness of eqb_list.
The length function is specified by induction on the structure of lists:
Definition specification_of_list_length (length : forall V : Type, list V -> nat) :=
(forall V : Type,
length V nil = 0)
/\
(forall (V : Type)
(v : V)
(vs' : list V),
length V (v :: vs') = S (length V vs')).
Here is a quick and dirty unit-test function, which unlike in OCaml is polymorphic since we can parameterize the candidate function with a type:
Definition test_list_length (candidate : forall V : Type, list V -> nat) :=
(candidate nat nil =? 0) &&
(candidate bool nil =? 0) &&
(candidate nat (1 :: nil) =? 1) &&
(candidate bool (true :: nil) =? 1) &&
(candidate nat (2 :: 1 :: nil) =? 2) &&
(candidate bool (false :: true :: nil) =? 2) &&
(candidate nat (3 :: 2 :: 1 :: nil) =? 3) &&
(candidate bool (false :: false :: true :: nil) =? 3).
The accompanying .v file contains
Implement the length function using an accumulator.
Copying a list is straightforwardly specified by induction over this list:
Definition specification_of_list_copy (copy : forall V : Type, list V -> list V) :=
(forall V : Type,
copy V nil = nil)
/\
(forall (V : Type)
(v : V)
(vs' : list V),
copy V (v :: vs') = v :: (copy V vs')).
The accompanying .v file contains a unit-test function for list_copy. Expand this unit-test function with a few more tests.
Implement the copy function recursively:
Fixpoint list_copy (V : Type) (vs : list V) : list V :=
...
State the associated fold-unfold lemmas.
Prove whether your implementation satisfies the specification.
Prove whether your implementation of copy is idempotent:
Proposition list_copy_is_idempotent :
forall (V : Type)
(vs : list V),
list_copy V (list_copy V vs) = list_copy V vs.
Prove whether copying a list preserves its length:
Proposition list_copy_preserves_length :
forall (V : Type)
(vs : list V),
list_length V (list_copy V vs) = list_length V vs.
Subsidiary question: can you think of a strikingly simple implementation of the copy function? If so, pray show that it satisfies the specification of copy:
Definition list_copy_alt (V : Type) (vs : list V) : list V :=
...
Concatenating two lists is straightforwardly specified by induction over the first list:
Definition specification_of_list_append (append : forall V : Type, list V -> list V -> list V) :=
(forall (V : Type)
(v2s : list V),
append V nil v2s = v2s)
/\
(forall (V : Type)
(v1 : V)
(v1s' v2s : list V),
append V (v1 :: v1s') v2s = v1 :: append V v1s' v2s).
Define a unit-test function for list concatenation.
Implement the append function recursively:
Fixpoint list_append (V : Type) (v1s v2s : list V) : list V :=
...
State the associated fold-unfold lemmas.
Prove that your implementation satisfies the specification.
Prove whether nil is neutral on the left of list_append.
Prove whether nil is neutral on the right of list_append.
Prove whether list_append is commutative.
Prove whether list_append is associative.
Prove whether concatenating two lists preserves their length:
Proposition list_append_and_list_length_commute_with_each_other :
forall (V : Type)
(v1s v2s : list V),
list_length V (list_append V v1s v2s) = list_length V v1s + list_length V v2s.
Prove whether list_append and list_copy commute with each other:
Proposition list_append_and_list_copy_commute_with_each_other :
forall (V : Type)
(v1s v2s : list V),
list_copy V (list_append V v1s v2s) = list_append V (list_copy V v1s) (list_copy V v2s).
Reversing a list is straightforwardly specified by induction over this list:
Definition specification_of_list_reverse (reverse : forall V : Type, list V -> list V) :=
forall append : forall W : Type, list W -> list W -> list W,
specification_of_list_append append ->
(forall V : Type,
reverse V nil = nil)
/\
(forall (V : Type)
(v : V)
(vs' : list V),
reverse V (v :: vs') = append V (reverse V vs') (v :: nil)).
Define a unit-test function for an implementation of list reversal.
Implement the reverse function recursively, using list_append:
Fixpoint list_reverse (V : Type) (vs : list V) : list V :=
...
State the associated fold-unfold lemmas.
Prove whether your implementation satisfies the specification.
Prove whether list_reverse is involutory:
Proposition list_reverse_is_involutory :
forall (V : Type)
(vs : list V),
list_reverse V (list_reverse V vs) = vs.
Pablito: Hmmm. Is the copy function also involutory?Halcyon (pensif): Oui... Cette fonction est-elle aussi involutive?
(N.B.: The adjective associated with “involution” is “involutory” in English and “involutive” in French. The French adjective is used in the Coq libraries, e.g., negb_involutive.)
Prove whether reversing a list preserves its length.
Do list_append and list_reverse commute with each other (hint: yes they do) and if so how?
Implement the reverse function using an accumulator instead of using list_append:
Definition list_reverse_alt (V : Type) (vs : list V) : list V :=
...
Revisit the propositions above (involution, preservation of length, commutation with append) and prove whether list_reverse_alt satisfies them. Two proof strategies are possible: (1) direct, stand-alone proofs with Eureka lemmas, and (2) proofs that hinge on the equivalence of list_reverse_alt and list_reverse. The latter proof is optional.
Mapping a given function over a given list is straightforwardly specified by induction over this list:
Definition specification_of_list_map (map : forall V W : Type, (V -> W) -> list V -> list W) :=
(forall (V W : Type)
(f : V -> W),
map V W f nil = nil)
/\
(forall (V W : Type)
(f : V -> W)
(v : V)
(vs' : list V),
map V W f (v :: vs') = f v :: map V W f vs').
Prove whether the specification specifies at most one map function.
(N.B.: The accompanying file contains this proof.)
Implement the map function recursively:
Fixpoint list_map (V W : Type) (f : V -> W) (vs : list V) : list W :=
...
(N.B.: The accompanying file contains this implementation.)
State the associated fold-unfold lemmas.
(N.B.: The accompanying file contains these fold-unfold lemmas.)
Prove whether your implementation satisfies the specification.
(N.B.: The accompanying file contains this proof.)
Implement the copy function using list_map:
Definition list_copy_using_list_map (V : Type) (vs : list V) : list V :=
...
Hint: Does list_copy_using_list_map satisfy the specification of copy?
Prove whether mapping a function over a list preserves the length of this list.
Do list_map and list_append commute with each other and if so how?
Do list_map and list_reverse commute with each other and if so how?
Do list_map and list_reverse_alt commute with each other and if so how? As in Task 5.i, two proof strategies are possible here.
Define a unit-test function for the map function and verify that your implementation satisfies it.
Alfrothul: My, my.Anton: Defining a unit-test function after implementing the function to test?Alfrothul (philosophical): Where is the world going?Loki: When in late Rome...
Folding right and folding left over lists abstract what to do in the base case and what to do in the induction step, and are straightforwardly specified by induction over the given list:
Definition specification_of_list_fold_right (fold_right : forall V W : Type, W -> (V -> W -> W) -> list V -> W) :=
(forall (V W : Type)
(nil_case : W)
(cons_case : V -> W -> W),
fold_right V W nil_case cons_case nil =
nil_case)
/\
(forall (V W : Type)
(nil_case : W)
(cons_case : V -> W -> W)
(v : V)
(vs' : list V),
fold_right V W nil_case cons_case (v :: vs') =
cons_case v (fold_right V W nil_case cons_case vs')).
Definition specification_of_list_fold_left (fold_left : forall V W : Type, W -> (V -> W -> W) -> list V -> W) :=
(forall (V W : Type)
(nil_case : W)
(cons_case : V -> W -> W),
fold_left V W nil_case cons_case nil =
nil_case)
/\
(forall (V W : Type)
(nil_case : W)
(cons_case : V -> W -> W)
(v : V)
(vs' : list V),
fold_left V W nil_case cons_case (v :: vs') =
fold_left V W (cons_case v nil_case) cons_case vs').
I fold-list to the left, I fold-list to the rightGonna rock’n’roll to the early, early night—Ready Teddy (nearly enough)
Implement the list-fold-right function:
Fixpoint list_fold_right (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
...
(N.B.: The accompanying file contains this implementation.)
Implement the list-fold-left function:
Fixpoint list_fold_left (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
...
(N.B.: The accompanying file contains this implementation.)
State the fold-unfold lemmas associated with list_fold_right and to list_fold_left.
(N.B.: The accompanying file contains these fold-unfold lemmas.)
Prove that each of your implementations satisfies the corresponding specification.
Which function do foo and bar compute:
Definition foo (V : Type) (vs : list V) :=
list_fold_right V (list V) nil (fun v vs => v :: vs) vs.
Definition bar (V : Type) (vs : list V) :=
list_fold_left V (list V) nil (fun v vs => v :: vs) vs.
On theories such as these we cannot rely.Proof we need. Proof!—Yoda
Show that if the cons case is a function that is left permutative, applying list_fold_left and applying list_fold_right to a nil case, this cons case, and a list give the same result:
Definition is_left_permutative (V W : Type) (op2 : V -> W -> W) :=
forall (v1 v2 : V)
(v3 : W),
op2 v1 (op2 v2 v3) = op2 v2 (op2 v1 v3).
Theorem folding_left_and_right :
forall (V W : Type)
(cons_case : V -> W -> W),
is_left_permutative V W cons_case ->
forall (nil_case : W)
(vs : list V),
list_fold_left V W nil_case cons_case vs =
list_fold_right V W nil_case cons_case vs.
Can you think of corollaries of this property?
Here is a simple example:
Lemma plus_is_left_permutative :
is_left_permutative nat nat plus.
Proof.
Abort.
Corollary example_for_plus :
forall ns : list nat,
list_fold_left nat nat 0 plus ns = list_fold_right nat nat 0 plus ns.
Proof.
Check (folding_left_and_right nat nat plus plus_is_left_permutative 0).
exact (folding_left_and_right nat nat plus plus_is_left_permutative 0).
Qed.
What do you make of this corollary? Can you think of more such corollaries? (Be imaginative.)
Subsidiary question: does the converse of Theorem folding_left_and_right hold? Namely:
Theorem folding_left_and_right_converse :
forall (V W : Type)
(cons_case : V -> W -> W),
(forall (nil_case : W)
(vs : list V),
list_fold_left V W nil_case cons_case vs =
list_fold_right V W nil_case cons_case vs) ->
is_left_permutative V W cons_case.
The functions list_fold_left and list_fold-right implement primitive iteration over lists. Let us turn to primitive iteration over natural numbers.
Here are the implementations of nat_fold_right and of its compeer nat_fold_left, that also abstract what to do in the base case and what to do in the induction step:
Fixpoint nat_fold_right (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
match n with
O =>
zero_case
| S n' =>
succ_case (nat_fold_right V zero_case succ_case n')
end.
Fixpoint nat_fold_left (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
match n with
O =>
zero_case
| S n' =>
nat_fold_left V (succ_case zero_case) succ_case n'
end.
Programmatically,
Implement the addition function as an instance of nat_fold_right or nat_fold_left, your choice.
(N.B.: The accompanying file contains such an implementation.)
Implement the power function as an instance of nat_fold_right or nat_fold_left, your choice.
Implement the factorial function as an instance of nat_fold_right or nat_fold_left, your choice.
Implement the Fibonacci function as an instance of nat_fold_right or nat_fold_left, your choice.
Under which conditions – if any – are nat_fold_left and nat_fold_right equivalent?
Created [22 Feb 2024]