Computing Science -> Bengt Nordström -> Type theory exercises

Some exercises in formal proofs

Content

  1. Propositional logic
  2. Properties of lists
  3. A library for natural numbers and their properties
  4. Dutch national flag
  5. Bounded linear search
  6. Permutations
  7. Type checking

Propositional logic.

  1. Define Or,And,False:(Set;Set)Set by giving the introduction rules
    2.   inl:(A,B:Set;A)Or(A,B)
  inr:(A,B:Set;B)Or(A,B)
  pair:(A,B:Set;A;B)And(A,B)
    no introduction rule for False.
  2.  Construct an element in the following types:
    3.   (A,B:Set;And(A,B))A
  (A,B:Set;And(A,B))B
  3. Justify the elimination rule
    4.  or_elim:(A,B,C:Set;(A)C;(B)C;Or(A,B))C
 and_elim:(A,B,C:Set;(A;B)C;And(A,B))C
 false_elim:(A:Set;False)A
    by giving computation rules for them (pattern-matching).
  4.  Give a similar justification of the rule
    5.  distr:(A,B,C:Set;And(A,Or(B,C)))Or(And(A,B),And(A,C))
    by giving computation rules. Alternatively, derive it by using and_elim and or_elim.
  5.  Define Imply by the introduction rule
    6.  lambda:(A,B:Set;(A)B)Imply(A,B)
    and justify 
     app:(A,B:Set;Imply(A,B);A)B
    by giving computation rules. Prove, using and_elim, or_elim, false_elim and app (and the introduction rules, of course) the equivalence between the statements 
     (A:Set)Imply(Not(Not(A)),A)
    and 
     (A:Set)Or(A,Not(A))
    where Not is [A]Imply(A,False).
  6.  Prove
    7. (A:Set)(Not(Equiv(A,Not(A))))
    where Equiv is {A,B]And(Imply(A,B),Imply(B,A))

Lists

The set of lists of elements of an arbitrary set A is defined by 
   List : (A:Set)Set
     nil  : (A:Set)List(A)
     cons : (A:Set)(a:A)(l:List(A))List(A)
  1. Define the following functions as implicit constants:
    2.    map : (A,B : Set)(f : (A)B)(l : List(A))List(B)
   foldl : (A,B : Set)(f : (A)(B)A)(b : A)(l : List(B))A
   foldr : (A,B : Set)(f :(A)(B)B)(b : B)(l : List(A))B
   filter : (A : Set)(p : (A)Bool)(l : List(A))List(A)
    Use these to define the following as explicit constants: 
       append : (A : Set)(l1,l2 : List(A))List(A)
   length : (A : Set)(l : List(A))N
   sum : (l : List(N))N
   prod : (l : List(N))N
   reverse : (A : Set)(l : List(A))List(A)
  2. Prove the following properties about the functions defined above:
    1. map distributes over composition of functions.
    2.  map distributes over append.
    3.  append has unit to the left.
    4.  append has unit to the right.
    5.  append is associative.
    6.  The length of the result of appending two lists is the sum of the lengths of these two lists.
    7.  filter distributes over append.
    8.  filter is idempotent.

A library for natural numbers and their properties

The task is to build up an arithmetical library. The structure of the library is taken from the corresponding library of Coq. Here I have only given the types and the names of the theorems, the proofs are left as exercises. When doing the proofs one can assume that the earlier theorems in the list have been proven (but not the later). The expression n=m stands for a propositional equality between n and m. The disjunction between a and b is written a \/ b. You only need to prove 10 - 15 of the following (I will distribute them among the students).

Module le, Properties of le:

Suppose that we have a definition of le (less than or equal). Then we must prove the following theorems. 
Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).

Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p).

Theorem le_n_Sn : (n:nat)(le n (S n)).

Theorem le_O_n : (n:nat)(le O n).

Theorem le_pred_n : (n:nat)(le (pred n) n).

Theorem le_trans_S : (n,m:nat)(le (S n) m)->(le n m).

Theorem le_S_n : (n,m:nat)(le (S n) (S m))->(le n m).

Theorem le_Sn_O : (n:nat)~(le (S n) O).

Theorem le_Sn_n : (n:nat)~(le (S n) n).

Theorem le_antisym : (n,m:nat)(le n m)->(le m n)->(n=m).

Theorem le_n_O_eq : (n:nat)(le n O)->(O=n).

Module lt, Properties of lt:

Given a definition of le we can define lt by 
ln n m = le (succ n) m
We then must prove the following properties: 
Theorem lt_n_Sn : (n:nat)(lt n (S n)).

Theorem lt_S : (n,m:nat)(lt n m)->(lt n (S m)).

Theorem lt_n_S : (n,m:nat)(lt n m)->(lt (S n) (S m)).

Theorem lt_S_n : (n,m:nat)(lt (S n) (S m))->(lt n m).

Theorem lt_O_Sn : (n:nat)(lt O (S n)).

Theorem lt_n_O : (n:nat)~(lt n O).

Theorem lt_n_n : (n:nat)~(lt n n).

Theorem S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))).

Theorem lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)).

Theorem lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n).
(* Relationship between le and lt *) 
Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p).

Theorem lt_n_Sm_le : (n,m:nat)(lt n (S m))->(le n m).

Theorem le_lt_n_Sm : (n,m:nat)(le n m)->(lt n (S m)).

Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m).

Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).

Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
(* Transitivity properties *) 
Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p).

Theorem lt_le_trans : (n,m,p:nat)(lt n m)->(le m p)->(lt n p).

Theorem le_lt_trans : (n,m,p:nat)(le n m)->(lt m p)->(lt n p).

Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).

Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).

Theorem le_not_lt : (n,m:nat)(le n m)->~(lt m n).

Theorem lt_not_le : (n,m:nat)(lt n m)->~(le m n).

Theorem lt_not_sym : (n,m:nat)(lt n m)->~(lt m n).

Theorem nat_total_order: (m,n: nat) ~ m = n -> (lt m n) \/ (lt n m).

Module plus, Properties of plus:

Theorem plus_sym : (n,m:nat)((plus n m)=(plus m n)).

Theorem plus_Snm_nSm : 
  (n,m:nat)(plus (S n) m)=(plus n (S m)).

Theorem simpl_plus_l : (n,m,p:nat)((plus n m)=(plus n p))->(m=p).

Theorem plus_assoc_l : (n,m,p:nat)((plus n (plus m p))=(plus (plus n m) p)).

Theorem plus_permute : (n,m,p:nat) ((plus n (plus m p))=(plus m (plus n p))).

Theorem plus_assoc_r : (n,m,p:nat)((plus (plus n m) p)=(plus n (plus m p))).

Theorem simpl_le_plus_l : (p,n,m:nat)(le (plus p n) (plus p m))->(le n m).

Theorem le_reg_l : (n,m,p:nat)(le n m)->(le (plus p n) (plus p m)).

Theorem le_reg_r : (a,b,c:nat) (le a b)->(le (plus a c) (plus b c)).

Theorem le_plus_plus : 
        (n,m,p,q:nat) (le n m)->(le p q)->(le (plus n p) (plus m q)).

Theorem le_plus_l : (n,m:nat)(le n (plus n m)).

Theorem le_plus_r : (n,m:nat)(le m (plus n m)).

Theorem le_plus_trans : (n,m,p:nat)(le n m)->(le n (plus m p)).

Theorem simpl_lt_plus_l : (n,m,p:nat)(lt (plus p n) (plus p m))->(lt n m).

Theorem lt_reg_l : (n,m,p:nat)(lt n m)->(lt (plus p n) (plus p m)).

Theorem lt_reg_r : (n,m,p:nat)(lt n m) -> (lt (plus n p) (plus m p)).

Theorem lt_plus_trans : (n,m,p:nat)(lt n m)->(lt n (plus m p)).

Module gt, Properties of gt:

We define gt by 
gt m n = lt m n
We then have the following properties of gt: 
Theorem gt_Sn_O : (n:nat)(gt (S n) O).

Theorem gt_Sn_n : (n:nat)(gt (S n) n).

Theorem le_S_gt : (n,m:nat)(le (S n) m)->(gt m n).

Theorem gt_n_S : (n,m:nat)(gt n m)->(gt (S n) (S m)).

Theorem gt_trans_S : (n,m,p:nat)(gt (S n) m)->(gt m p)->(gt n p).

Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p).

Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p).

Theorem le_not_gt : (n,m:nat)(le n m)->~(gt n m).

Theorem gt_antirefl : (n:nat)~(gt n n).

Theorem gt_not_sym : (n,m:nat)(gt n m)->~(gt m n).

Theorem gt_not_le : (n,m:nat)(gt n m)->~(le n m).

Theorem gt_trans : (n,m,p:nat)(gt n m)->(gt m p)->(gt n p).

Theorem gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n).

Theorem gt_S_le : (n,p:nat)(gt (S p) n)->(le n p).

Theorem gt_le_S : (n,p:nat)(gt p n)->(le (S n) p).

Theorem le_gt_S : (n,p:nat)(le n p)->(gt (S p) n).

Theorem gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n).

Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(m=n)).

Theorem gt_O_eq : (n:nat)((gt n O)\/(O=n)).

Theorem simpl_gt_plus_l : (n,m,p:nat)(gt (plus p n) (plus p m))->(gt n m).

Theorem gt_reg_l : (n,m,p:nat)(gt n m)->(gt (plus p n) (plus p m)).

Module minus, Properties of minus:

Theorem minus_plus_simpl : 
        (n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).

Theorem minus_n_O : (n:nat)(n=(minus n O)).

Theorem minus_n_n : (n:nat)(O=(minus n n)).

Theorem plus_minus : (n,m,p:nat)(n=(plus m p))->(p=(minus n m)).

Theorem minus_plus : (n,m:nat)(minus (plus n m) n)=m.

Theorem le_plus_minus : (n,m:nat)(le n m)->(m=(plus n (minus m n))).

Theorem le_plus_minus_r : (n,m:nat)(le n m)->(plus n (minus m n))=m.

Theorem minus_Sn_m : (n,m:nat)(le m n)->((S (minus n m))=(minus (S n) m)).

Theorem lt_minus : (n,m:nat)(le m n)->(lt O m)->(lt (minus n m) n).

Theorem lt_O_minus_lt : (n,m:nat)(lt O (minus n m))->(lt m n)

Module mult, Properties of mult:

Theorem mult_plus_distr : 
      (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))).

Theorem mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))).

Theorem mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)).

Theorem mult_assoc_r : (n,m,p:nat)((mult (mult n m) p) = (mult n (mult m p))).

Theorem mult_assoc_l : (n,m,p:nat)(mult n (mult m p)) = (mult (mult n m) p).

Theorem mult_1_n : (n:nat)(mult (S O) n)=n.

Theorem mult_sym : (n,m:nat)(mult n m)=(mult m n).

Theorem mult_n_1 : (n:nat)(mult n (S O))=n.

Some bigger exercises

Dutch national flag problem

This exercise consists of solving the Dutch national flag problem, which can be described as follows :

Given a list whose elements are coloured red, white and blue in any order, construct a new list in which the elements are reordered in such a way that it constitutes a representation of the Dutch flag.

There are many ways to formalize this problem. In this exercise you should compare the internal and external approaches:

In the internal approach you start with stating a theorem to be proven: For a given l : List(C) there exist l1, l2, l3:List(C) such that Red(l1), White(l2), Blue(l3) and Perm(l, l1 ++ l2 ++ l3), where C = {red, white, blue}, ++ is list concatenation, and Perm is a predicate expressing that the two arguments are permutations of each other.

In the external approach you start to write a function dutch : (List(C))List(C) X List(C) X List(C) and then prove that the function has the desired properties.

For this exercise it is not necsessary to prove all properties of Perm. See also the exercise below.

Bounded linear search

Consider a Boolean function f on the natural numbers. The problem we consider is that of finding the smallest n:N for which f(n) = true. The obvious algorithm is to evaluate first f(0), then f(1) etc until the proper n is found. There are two obstacles: first, no such n need exist and, second, even if it does we have no bound on how far we need to search. We therefore consider only bounded linear search, where we give the search function two arguments, f and a bound max:N and want as output either the smallest n<max for which f(n)=true or, if no such n exists, max itself.

Permutations.

Define the permutation relation between lists. You may want to do it for some particular type of elements (e.g. lists of natural numbers) or more generally. There are many possible definitions. Then develop some theory for permutations, such as
  1. the permutation relation is an equivalence relation,
  2.  if l2 is permutation of l1 then l1 and l2 are of the same length,
  3.  if rev(l) denotes l reversed, then rev(l) is a permutation of l,
  4.  if l1 is a permutation of l2 and l3 a permutation of l4, then append(l1,l3) is a permutation of append(l2,l4).

Type-checking.

We consider the simply typed lambda calculus with variables represented by de Bruijn indices. Define
  1. the set of terms,
  2.  the set of types (e.g. one ground type and function types),
  3.  the typing relation.
Then define a type-checker as a function taking a term as argument and returning either a type error or a correct type for the argument. Prove the soundness and completeness of the type-checker.
 

Bengt Nordstr|m

Fri Sep 5 13:39:35 MET DST 1997