Library Sets
Section Sets.
Some magic incantations...
Open Scope type_scope.
Set Implicit Arguments.
Implicit Arguments inl [A B].
Implicit Arguments inr [A B].
As we have defined bool we can define other finite sets
just by enumerating the elements.
Im Mathematics (and conventional Set Theory), we just write C = { c1, c2 , .. , cn } for a finite set.
In Coq we write
Inductive C : Set := | c1 : C | c2 : C ... | cn : C.
As a special example we define the empty set:
Im Mathematics (and conventional Set Theory), we just write C = { c1, c2 , .. , cn } for a finite set.
In Coq we write
Inductive C : Set := | c1 : C | c2 : C ... | cn : C.
As a special example we define the empty set:
Inductive empty_set : Set := .
As an example for finite sets, we consider the game of chess.
We need to define the colours, the different type of pieces,
and the coordinates.
Inductive Colour : Set :=
| white: Colour
| black : Colour.
Inductive Rank : Set :=
| pawn : Rank
| rook : Rank
| knight : Rank
| bishop : Rank
| queen : Rank
| king : Rank.
Inductive XCoord : Set :=
| xa : XCoord
| xb : XCoord
| xc : XCoord
| xd : XCoord
| xe : XCoord
| xf : XCoord
| xg : XCoord
| xh : XCoord.
Inductive YCoord : Set :=
| y1 : YCoord
| y2 : YCoord
| y3 : YCoord
| y4 : YCoord
| y5 : YCoord
| y6 : YCoord
| y7 : YCoord
| y8 : YCoord.
In practice it is not such a good idea to use different
sets for the x and y coordinates. We use this here for
illustration and it does reflect the chess notation
like e2 - e4 for moving the pawn in front of the king.
We can define operations on finite sets using the match
construct we have already seen for book. As an example
we define the operation
oneUp : YCoord -> YCoord
which increases the y coordinates by 1. We have to decide
what to do when we reach the 8th row. Here we just get
stuck.
Definition oneUp (y : YCoord) : YCoord :=
match y with
| y1 => y2
| y2 => y3
| y3 => y4
| y4 => y5
| y5 => y6
| y6 => y7
| y7 => y8
| y8 => y8
end.
Given two sets A B : Set we define a new set
A * B : Set which is called the product of
A and B. It is the set of pairs (a,b) where
a : A and b : B.
As an example we define the set of chess pieces
and coordinates:
Definition Piece : Set := Colour * Rank.
Definition Coord : Set := XCoord * YCoord.
And for illustration construct some elements:
Definition blackKnight : Piece := (black , knight).
Definition e2 : Coord := (xe , y2).
On Products we have some generic operations called
projections which extract the components of a product.
Definition fst(A B : Set)(p : A * B) : A :=
match p with
| (a , b) => a
end.
Definition snd(A B : Set)(p : A * B) : B :=
match p with
| (a , b) => b
end.
Eval compute in fst blackKnight.
Eval compute in snd blackKnight.
Eval compute in (fst blackKnight,snd blackKnight).
A general theorem about products is that if we take
apart an element using projections and then put it
back together again we get the same element. In predicate
logic this is:
forall p : A * B, (fst p , snd p) = p
This is called surjective pairing. In the actual statement in Coq we also have to quantify over the sets involved (which technically gets us into the realm of higher order logic - but we shall ignore this).
forall p : A * B, (fst p , snd p) = p
This is called surjective pairing. In the actual statement in Coq we also have to quantify over the sets involved (which technically gets us into the realm of higher order logic - but we shall ignore this).
Lemma surjective_pairing : forall A B : Set,
forall p : prod A B, (fst p , snd p) = p.
intros A B p.
The actual proof is rather easy.
All that we need to know is that we can take apart
a product the same way as we have taken apart conjunctions.
destruct p as [a b].
simpl.
simpl.
Can you simplify this goal in your head?
Yes simpl will do the job but why?
reflexivity.
Qed.
Qed.
Question: If |A| and |B| are finite sets with |m| and
|n| elements respectively, how many elements are in
|A * B|?
Given two sets A B : Set we define a new set
A + B : Set which is called the disjoint union of
A and B. Elements of A + B are either inl a
where a : A or inr b where b : B. Here inl
stands for "inject left" and inr stands for
"inject right".
It is important not to confuse + with the union of sets. The disjoint union of bool with bool has 4 elements because inl true is different from inr true while in the union of bool with bool there are only 2 elements since there is only one copy of true. Actually, the union of sets does not exist in Coq.
It is important not to confuse + with the union of sets. The disjoint union of bool with bool has 4 elements because inl true is different from inr true while in the union of bool with bool there are only 2 elements since there is only one copy of true. Actually, the union of sets does not exist in Coq.
As an example we use disjoint union to define the set
field which can either be a piece or empty. The second
case is represented by a set with just one element called
Empty which has just one element empty.
Inductive Empty : Set :=
| empty : Empty.
Definition Field : Set := Piece + Empty.
some examples
Definition blackKnightHere : Field := inl blackKnight.
Definition emptyField : Field := inr empty.
As an example of a defined operation we define swap
which maps elements of A + B to B + A by mapping
inl to inr and vice versa.
Definition swap(A B : Set)(x : A + B) : B + A :=
match x with
| inl a => inr a
| inr b => inl b
end.
The same question as for products: If A has
m elements and B has n elements, how many
elements are in A + B?
Disjoint unions are sometimes called coproducts
because there are in a sense the mirror image
of products. To make this precise we need the language
of category theory, which is beyond this course.
However, if you are curious look up Category Theory
on wikipedia.
Given two sets A B : Set we define a new set
A -> B : Set, the set of functions form A
to B. We have already seen one way to define
functions, whenever we have defined an operation
we have actually defined a function. However, as
you have already seen in Haskell, we can define
functions directly using lambda abstraction. The
syntax is fun x => b where b is an expression
in B which may refer to x : A.
In the case of our chess example we can use functions to define
a chess board as a function form Coord to Field,
this function would give us the content of a field for
any coordinate.
Definition Board : Set := Coord -> Field.
A particular simple example is the empty board:
Definition EmptyBoard : Board := fun x => emptyField.
I leave it as an exercise to construct the initial board for a
chess game.
As another example instead of defining negb as an
operation we could also have used fun:
Definition negb' : bool -> bool
:= fun (b : bool) => match b with
| true => false
| false => true
end.
Using fun is especially useful when we are dealing with higher
order functions, i.e. function which take functions as
arguments. As an example let us define the function isConst which
determines wether a given function f : bool -> bool is
constant.
Open Scope bool_scope.
Definition isConst (f : bool -> bool) : bool :=
(f true) && (f false) || negb (f true) && negb (f false).
What will Coq answer when asked to evaluate the terms below.
In three cases we are using fun to construct the argument.
Could we have done this in the 1st case as well?
Eval compute in isConst negb.
Eval compute in isConst (fun x => false).
Eval compute in isConst (fun x => true).
Eval compute in isConst (fun x => x).
Are there any other cases to consider ?
In general, if A,B are finite sets with m and n elements,
how many elements are in A -> B? Actually we need to assume the
axiom of extensionality to get the right answer. This axiom states that any
two functions which are equal for all arguments are equal.
Axiom ext : forall (A B : Set)(f g : A -> B), (forall x:A,f x = g x) -> f = g.
There is a close correspondence between sets and propositions. We
may translate a proposition by the set of its proofs. The question
wether a proposition holds corresponds then to finding an element
which lives in the corresponding set. Indeed, this is what Coq's proof objects
are based upon. For propositional logic the translation works as follows:
- conjunction (/\) is translated as product (*),
- disjunction (\/) is translated as disjoint union (+),
- implication (->) is translated as function set (->).
Definition curry (A B C : Set) : ((A * B -> C) -> (A -> B -> C)) :=
fun f => fun a => fun b => f (a , b).
Definition curry' (A B C : Set) : (A -> B -> C) -> (A * B -> C) :=
fun g => fun p => g (fst p) (snd p).
Indeed, curry and curry' do not just witness a logical equivalence
but they constitute an isomorphism. That is if we go back and forth we end up
with the lement we started. We will need the axiom of extensionality.
To make this precise we get:
Lemma curryIso1 : forall A B C : Set, forall f : A * B -> C,
f = (curry' (curry f)).
intros A B C f.
apply ext.
intro p.
destruct p.
reflexivity.
Qed.
Lemma curryIso2 : forall A B C : Set, forall g : A -> B -> C,
g = (curry (curry' g)).
intros A B C g.
apply ext.
intro a.
apply ext.
intro b.
reflexivity.
Qed.
End Sets.