(** Introduction to Formal Reasoning (G52IFR)
    Nicolai Kraus

    Tutorial 4: Sets
**)


Section Tutorial4.

(** two colours **)
Inductive Colour : Set := 
   | blue : Colour
   | red  : Colour.


(** more complicated colours**)
Inductive ComplColour : Set :=
   | orange : ComplColour
   | aBitDarker : Colour -> ComplColour
   | mix : ComplColour -> ComplColour -> ComplColour.

(** "mix (aBitDarker blue) (aBitDarker red)" could 
be something like violet **)

(** the identity function **)
Definition id : Colour -> Colour :=
   fun (c : Colour) =>
      match c with 
        | red  => red
        | blue => blue
      end.

(** again **)
Definition id' : Colour -> Colour := 
   fun c => c.

(** can we prove id = id'? **)

Axiom extensionality : 
   forall A B : Set, 
      forall f g : A -> B,
         (forall a : A, f a = g a) -> f = g.


Lemma same : id = id'.
apply extensionality.
intro c.
destruct c.
reflexivity.
reflexivity.
Qed.


Inductive Rows : Set :=
  | r1 : Rows
  | r2 : Rows.

Inductive Cols : Set := | c1 | c2.

Definition Board : Set := Rows * Cols -> Colour.

(** a special board: every field is red **)
Definition allRed : Board := 
   fun (rc : Rows * Cols) => red.



(** More general sets could be more interesting! **)


Variables A B : Set.

(** this it the eta law: if you abstract a varia**)
Lemma eta : forall f : A -> B, 
   f = (fun a => f a).
intro f.
apply extensionality.
intro a.
reflexivity.
Qed.


(** let's do an exercise about isomorphism of sets **)

(** do not worry about these commands for now: **)
Open Scope type_scope.
Set Implicit Arguments.
Implicit Arguments inl [A B].
Implicit Arguments inr [A B].


(** Let's construct an isomorphism between two sets **)

Definition S1 : Set := (A + B) * Colour.

Definition S2 : Set := Colour * B + Colour * A.


Definition f : S1 -> S2 := 
  fun (s : S1) => match s with
    | (ab , c) => match ab with
       | (inl a) => inr (c , a)
       | (inr b) => inl (c , b)
       end
    end.

Definition g : S2 -> S1 :=
  fun s => match s with 
     | inl (c , b) => (inr b , c)
     | inr (c , a) => (inl a , c)
     end.


Lemma firstFthenGisID : 
  forall s : S1, g(f(s)) = s.
intro s.
destruct s as (ab , c).
destruct ab.
simpl.
reflexivity.
unfold g.
unfold f.
reflexivity.
Qed.


Lemma firstGthenFisID : forall s : S2, f(g(s)) = s.
intro s.
destruct s;
destruct p;
reflexivity.
Qed.

End Tutorial4.