(** Introduction to Formal Reasoning (G52IFR) Nuo Li T06 **) Section Tictactoe. Open Scope type_scope. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. (** Represent the game of Tic-tac-toe (see wikipedia) using finite sets, products and coproducts. In particular define the following sets - Piece : the set pof pieces - Coord : the set of coordinates - Field : the set of contents of a field - Board : the set of boards Construct the following board as myboard : Board XXO .O. ... Define a function mirrorBoard : Board -> Board which mirrors a board along the diagonal, i.e. in the example we would get ..O .OX ..X *) Inductive Piece : Set := | O : Piece | X : Piece. Inductive Three : Set := | t1 : Three | t2 : Three | t3 : Three. Definition Coord : Set := Three * Three. Inductive Empty : Set := | empty : Empty. Definition Field : Set := Piece + Empty. Definition FX : Field := inl X. Definition FO : Field := inl O. Definition FE : Field := inr empty. Definition Board : Set := Coord -> Field. Definition myBoard : Board := fun xy : Coord => match xy with | (t1 , t3) => FX | (t2 , t2) => FO | (t2 , t3) => FX | (t3 , t3) => FO | _ => FE end. Definition mirrorBoard : Board -> Board := fun b : Board => fun c : Coord => match c with | (x , y) => b (y , x) end. Eval compute in ((mirrorBoard myBoard) (t3 , t1)). End Tictactoe. Section CW3. Require Import Coq.Bool.Bool. Lemma ex36 : ~(exists y : bool, forall x : bool, x || y = x && y). intro. destruct H. destruct x. discriminate (H false). discriminate (H true). Qed. Theorem tricky: forall (f:bool -> bool) (b:bool), f( f( f( b))) = f b. intros. assert ((exists x : bool, forall a, f a = x) \/ forall a, f (f a) = a). case_eq (f true); case_eq (f false);intros. left. exists true. intro. destruct a;assumption. right. intro. destruct a. rewrite H0. assumption. rewrite H. assumption. right. destruct a. rewrite H0. assumption. rewrite H. assumption. left. exists false. intro. destruct a;assumption. destruct H. destruct H. rewrite (H b). apply H. rewrite H. reflexivity. Qed. End CW3. Section T6. Load Lists. Set Implicit Arguments. Implicit Arguments nil [A]. Infix "::" := cons (at level 60, right associativity). Infix "++" := app (right associativity, at level 60). (* An alternative way to define snoc*) Definition snoc' (l : list nat)(n : nat) := l ++ (n :: nil). Fixpoint frev_aux (A : Set)(l acc : list A) : list A := match l with | nil => acc | a :: l' => frev_aux l' (a::acc) end. Definition frev (A:Set)(l:list A) : list A := frev_aux l nil. (* Because frev is just a special case of frev_aux, it is also hard to only reason about frev *) Lemma frev_aux_lem : forall(A : Set)(l l' : list A), frev_aux l l' = rev l ++ l'. induction l. simpl. reflexivity. simpl. intro. rewrite IHl. clear IHl. induction (rev l). simpl. reflexivity. simpl. rewrite IHl0. reflexivity. Qed. Lemma frevfrev : forall(A : Set)(l : list A), frev (frev l) = l. unfold frev. intros. rewrite frev_aux_lem. rewrite frev_aux_lem. rewrite app_l_nil. rewrite app_l_nil. apply revrev. Qed. (* We say that a list is a permutation of another list if one list can be obtained from the other by rearranging the elements. One way to specify this is to say is using a function which counts occurences and then a list is a permutation if the number of all elements is the same. *) Fixpoint count (n:nat)(ms:list nat) {struct ms} : nat := match ms with | nil => 0 | m::ms' => let cn := count n ms' in if eqnat n m then S cn else cn end. Definition Perm (ns ms:list nat) := forall n:nat,count n ns=count n ms. (* we can prove a smimilar lemma in cw *) (** A hint (I add this after both tutorials) : if we prove add an element at the beginning of a list is perm to insert it into the list, then it is easy to prove repeating inserting is the same as repeating cons (::) **) Lemma count_inv : forall n l,count n (insert n l) = S (count n l). intros. induction l. simpl. rewrite eqnat_refl. reflexivity. simpl. case_eq (leqb n a);intro. simpl. rewrite eqnat_refl. split. simpl. rewrite IHl. destruct (eqnat n a);split. Qed. End T6.