(** Introduction to Formal Reasoning (G52IFR) Nuo Li Tutorial 4 **) Section Sets. Open Scope type_scope. Set Implicit Arguments. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. (** Reversi/Othello **) (** To build the coordinates using finite sets **) (** Do we need to enumerate all of them ? **) Inductive Row : Set := | r1 | r2 | r3 | r4 | r5 | r6 | r7 | r8 . Inductive Column : Set := | ca | cb | cc | cd | ce | cf | cg | ch. (** Products of types **) Definition Coord : Set := Row * Column. (** How to use products ? **) 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 (r5 , ca)). (** the pieces in reversi **) Inductive Piece : Set := | white : Piece | black : Piece. (** Be careful they are not the pieces in tic-tac-toe **) (** flip function **) Definition flip (a : Piece) : Piece := match a with | white => black | black => white end. (** How many possible states can a field have? **) Inductive Empty : Set := | empty : Empty. (** Disjoint Union **) Definition Field : Set := Piece + Empty. Eval compute in (inl white) : Piece + Empty. (** enumerate the elements of Field **) Definition FW : Field := inl white. Definition FB : Field := inl black. Definition FE : Field := inr empty. (** A Board is a function like a sequence **) Definition Board : Set := Coord -> Field. (** What are the difference between Coord * Field, Coord + Field and this one ? **) (** Write an example **) Definition EmptyBoard : Board := fun c : Coord => FE. (** The start of an Reversi board **) Definition start : Board := fun c : Coord => match c with | (r4 , cd) => FB | (r4 , ce) => FW | (r5 , cd) => FW | (r5 , ce) => FB | _ => FE end. (** Part 2 **) (** Isomorphism between F and G **) Definition F : bool * bool -> bool + bool := fun (bb : bool * bool) => match bb with | (a , b) => match a with | true => inl b | false => inr b end end. Definition G : bool + bool -> bool * bool := fun (bb : bool + bool) => match bb with | inl b => (true , b) | inr b => (false , b) end. Lemma FG : forall (bb : bool + bool), F (G bb) = bb. intro. destruct bb; simpl; reflexivity. Qed. Lemma GF : forall (bb : bool * bool), G (F bb) = bb. intro. destruct bb. destruct b; simpl; reflexivity. Qed. (** Using axiom ext **) Axiom ext : forall (A B : Set)(f g : A -> B), (forall x:A,f x = g x) -> f = g. Inductive Colour : Set := | red : Colour | blue : Colour. Definition id : Colour -> Colour := fun (c : Colour) => match c with | red => red | blue => blue end. Definition id' : Colour -> Colour := fun c => c. Lemma same : id = id'. apply ext. intro. destruct x; simpl; reflexivity. Qed. (** What is a higher order function ? **) (** is "and" function You can't pattern match on functions **) Definition isAnd (f : bool * bool -> bool) : bool := match f (true , true) with | true => match f (true , false) with | false => match f (false , true) with | false => match f (false , false) with | false => true | true => false end | true => false end | true => false end | false => false end. (* think all assumptions you have including implicit ones *) Lemma full : forall (a : bool)(f g : bool -> bool), f a = g a \/ f a = negb (g a). intros. destruct (g a); destruct (f a); [left | right | right | left]; split. Qed. (* can we enumerate function sets? *) (* How many elements in bool -> bool? *) Lemma onlyfour : forall (f : bool -> bool), f = (fun x : bool => x) \/ f = (fun x : bool => true) \/ f = (fun y : bool => false) \/ f = negb. Definition Constant (f : bool -> bool) : Prop := exists b : bool, forall n : bool, f n = b. Definition Involutary (f : bool -> bool) : Prop := forall n : bool, f (f n) = n. Lemma twoKinds : forall (f : bool -> bool), Constant f \/ Involutary f. intro. case_eq (f true); case_eq (f false); intros. left. exists true. intro. destruct n; assumption. right. intro. destruct n. repeat rewrite H0. split. repeat rewrite H. split. right. intro. destruct n. rewrite H0. rewrite H. split. rewrite H. rewrite H0. split. left. exists false. intro. destruct n;assumption. Qed. End T4.