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