(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch L07 (Operations on sets) The material in this file contains coq proofs which can be read and animated with coqide or xemacs+proofgeneral. **) Section sets. (*** Finite sets ***) Inductive square : Set := | nought : square | cross : square | empty : square. (* In Maths : square = { nought, cross, empty } *) Definition swap (f : square) : square := match f with | nought => cross | cross => nought | empty => empty end. Eval compute in (swap cross). Definition is_empty (f : square) : bool := match f with | nought => false | cross => false | empty => true end. Eval compute in (is_empty cross). Goal forall s:square, is_empty s = is_empty (swap s). intro s. destruct s; reflexivity. Qed. (* Bool is just another inductive defn & if..then..else is a shorthand for match *) Definition negb' (b:bool) : bool := match b with | true => false | false => true end. (* finite sets may also be empty *) Inductive Empty_set : Set :=. Definition fromEmpty (A : Set) (x : Empty_set) : A := match x with end. (* this is already defined in the library. *) (*** Cartesian Product (A * B) ***) Definition ex1 : square * bool := ( nought, true ). (* Definition fst (p : square * bool) : square := match p with | (n,b) => n end. Eval compute in (fst ex1). Definition snd (p : nat * bool) : bool := match p with | (n,b) => b end. *) (* Q : How many elements are in square * bool ? *) (* Polymorphically: *) Set Implicit Arguments. Definition fst (A B : Set)(p : A * B) : A := match p with | (a,b) => a end. Eval compute in (fst ex1). (* Eval compute in (fst square bool ex1). without Implicit Arguments. *) Definition snd (A B : Set)(p : A * B) : B := match p with | (a,b) => b end. Eval compute in (snd ex1). Definition my_swap (A B : Set) (p : A * B) : B * A := match p with | (a,b) => (b,a) end. Eval compute in (my_swap ex1). Goal forall A B : Set,forall p:A*B, my_swap (my_swap p) = p. intros A B p. destruct p. unfold my_swap. reflexivity. Qed. (* surjective pairing *) Goal forall A B : Set,forall p:A*B, (fst p,snd p) = p. intros A B p. destruct p. reflexivity. Qed. (*** Disjoint union (A + B) ***) Definition ex2 : square + bool := inl bool nought. Definition ex3 : square + bool := inr square false. (* Q: How many elements are in square + bool? *) Definition is_empty_or_true (s : square + bool) : bool := match s with | inl f => is_empty f | inr b => b end. Eval compute in (is_empty_or_true ex2). Eval compute in (is_empty_or_true ex3). Definition phi (A B C : Set)(abc : A * (B + C)) : A * B + A * C := match abc with | (a,bc) => match bc with | inl b => inl (A * C) (a,b) | inr c => inr (A * B) (a,c) end end. Definition psi (A B C : Set)(abc : A * B + A * C) : A * (B + C) := match abc with | inl ab => match ab with | (a , b) => (a , inl C b) end | inr ac => match ac with | (a , c) => (a , inr B c) end end. (** Example of an isomorphism **) Goal forall (A B C : Set)(abc : A * (B + C)), psi (phi abc) = abc. intros A B C abc. destruct abc. destruct s. reflexivity. reflexivity. Qed. Goal forall (A B C : Set)(abc : A * B + A * C), phi (psi abc) = abc. intros A B C abc. destruct abc. destruct p. reflexivity. destruct p. reflexivity. Qed. (*** Function space ***) Definition is_empty' : square -> bool := fun (s : square) => match s with | nought => false | cross => false | empty => true end. (* fun (x : A) => M is an anonoymous function, in Math we write \lambda x:A.M hence this is called lambda-abstraction. Also in Haskell we write \ x -> M where \ stands for lambda *) (* higher order functions *) Open Scope bool_scope. Definition is_is_empty : (square -> bool) -> bool := fun (f : square -> bool) => negb (f nought) && negb (f cross) && f empty. (* this is a second order function. *) (* Definition order of a function: ** order (A -> B) = max(order A) +1,order B) *) (* the category of sets *) (* the identity function *) Definition id {A:Set} : A -> A := fun (a : A) => a. (* the composition function (2nd order) *) Definition comp (A B C : Set) : (B -> C) -> (A -> B) -> (A -> C) := fun (g : B -> C) => fun (f : A -> B) => fun (a : A) => g (f a). (* why the strange order ? *) (** The axiom of extensionality **) Axiom ext : forall (A B : Set)(f g : A -> B), (forall x:A,f x = g x) -> f = g. (* laws of a category : *) Lemma rneutr : forall (A B:Set)(f : A -> B), comp f id = f. intros A B f. apply ext. intro x. reflexivity. Qed. Lemma lneutr : forall (A B:Set)(f : A -> B), comp id f = f. intros A B f. apply ext. intro x. reflexivity. Qed. Lemma assoc : forall (A B C D : Set)(h : C -> D)(g : B -> C)(f : A -> B), comp (comp h g) f = comp h (comp g f). intros A B C D h g f. apply ext. intros x. reflexivity. Qed. (** What about other operations, like union, intersection, complement ? In Coq these are *not* operations on sets, but operations of subsets. *) Definition subset (A : Set) := A -> Prop. Definition union (A : Set) (p q : subset A) : subset A := fun (a : A) => p a /\ q a. Definition intersection (A : Set) (p q : subset A) : subset A := fun (a : A) => p a \/ q a. Definition complement (A : Set)(p : subset A) : subset A := fun (a : A) => ~ (p a). (* Compare Curry-Howard equivalence (of sets and prop) with the classical equivalence (of bool and prop) *)