Computing Science -> Bengt Nordström -> Type theory exercises |
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.
(A,B:Set;And(A,B))A (A,B:Set;And(A,B))B
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)Aby giving computation rules for them (pattern-matching).
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.
lambda:(A,B:Set;(A)B)Imply(A,B)and justify
app:(A,B:Set;Imply(A,B);A)Bby 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).
(A:Set)(Not(Equiv(A,Not(A))))where Equiv is {A,B]And(Imply(A,B),Imply(B,A))
List : (A:Set)Set nil : (A:Set)List(A) cons : (A:Set)(a:A)(l:List(A))List(A)
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)
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).
ln n m = le (succ n) mWe 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).
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)).
gt m n = lt m nWe 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)).
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)
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.
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.