(** 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.