(** Introduction to Formal Reasoning (G52IFR)
    Nuo Li

    Tutorial 4

**)

Section Sets.

Open Scope type_scope.

Set Implicit Arguments.


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

(** the pieces in reversi **)

Inductive Piece : Set :=
  | white : Piece
  | black : Piece.

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

Definition Field : Set := Piece + Empty.

Implicit Arguments inl [A B].
Implicit Arguments inr [A B].

Eval compute in (inl white) : Field. 

(** enumerate the elements of Field **)

Definition FW : Field := inl white.
Definition FB : Field := inl black.
Definition FE : Field := inr empty.

(** A Board is a mapping from coordinates to fields **)

Definition Board : Set := Coord -> Field.

Definition EmptyBoard : Board :=
  fun x : Coord => FE.

Eval compute in (EmptyBoard (r4 , cd)).

(** The start of a Othello board **)

Definition start : Board := fun x : Coord =>
  match x with
    | (r4, cd) => FW
    | (r4, ce) => FB
    | (r5, cd) => FB
    | (r5, ce) => FW
    | _        => FE
  end.



(** Isomorphism between F and G **)

Definition F : bool * bool -> bool + bool :=
  fun x : bool * bool =>
    match x with
      | (true , b)  => inl b
      | (false , b) => inr b
    end.

Definition G : bool + bool -> bool * bool :=
  fun x : bool + bool =>
    match x 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.
simpl.
reflexivity.
Qed.

Lemma GF : forall (bb : bool * bool), G (F bb) = bb.
intro.
destruct bb.
destruct b; simpl.
reflexivity.
split.
Qed.

(* think all assumptions you have including primitive 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.
split.
right.
split.
right.
split.
left.
split.
Qed.

(* can we enumerate function sets? *)
(* How many elements in bool -> bool? *)


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.
rewrite H0.
rewrite H0.
split.

rewrite H.
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 Sets.

Section Nat.

Inductive Nat : Set :=
  | zero : Nat
  | S    : Nat -> Nat.

End Nat.