(** Introduction to Formal Reasoning (G52IFR)
    Nicolai Kraus, Nuo Li
    Tutorial 8

    November 27/28, 2012
**)

Section RevisionPart1.



(** 4 out of 6 parts to be completed in the exam *)



(**   1. Propositional Logic   *)

(** tactics for \/  ->  /\  ~  ...
    assert, classic, NNPP *)

Require Import Coq.Logic.Classical.

Variable P Q R : Prop.


Lemma implToOr : (P -> Q) <-> ~P \/ Q.
split.
intro pq.
destruct (classic P).
right; exact (pq H).
left; assumption.
intros npq p.
destruct npq.
destruct (H p).
assumption.
Qed.



(**   Predicate logic   *)

(** tactics for exists, forall, formalize statements *)

Variable PeopleInPub : Set.
Variable Drinks : PeopleInPub -> Prop.

(** Formalize the statement:

If there is someone in the pub, then we can find a person X such that: 
If X drinks, then everybody drinks! *)

Hypothesis drinker : (exists p : PeopleInPub, True) 
   -> exists X : PeopleInPub, (Drinks X -> forall y : PeopleInPub, Drinks y).

End RevisionPart1.


Section RevisionPart2.


(**   Bool   *)

(* inductive type -> you can use 'destruct' (or 'induction'), and case_eq *)

Require Import Coq.Bool.Bool.

Lemma forallExists : forall x : bool, exists y : bool, x || y = x && y.
intro x; destruct x.
exists true; reflexivity.
exists false; reflexivity.
Qed.





(**   Sets   *)

(** know inductive definitions of sets, pattern matching, induction, etc *)

Inductive Brightness :=
  | light : Brightness
  | dark  : Brightness.

Inductive Colour :=
  | red  : Brightness -> Colour
  | blue : Brightness -> Colour
  | green: Brightness -> Colour
  | white: Colour
  | black: Colour.



(**   Arithmetic   *)

(** lemmas for +, *
    know how to do induction on natural numbers  *)

Require Import Coq.Arith.Arith.

Lemma exchange : forall a b x y, (x + y) + (a + b) = (x + a) + (y + b).
intros.
repeat rewrite plus_assoc.
pattern (x + y + a).
rewrite <- plus_assoc.
pattern (y + a).
rewrite plus_comm.
rewrite plus_assoc.
reflexivity.
Qed.



(**   Lists   *)

(** know how they are constructed
    know rev, length, map ...
    know simple lemmas: app_nil_r, app_nil_l, ... *)

Require Import Coq.Lists.List.
Set Implicit Arguments.

Fixpoint map (A B : Set)(f : A -> B)(l : list A) : list B :=
  match l with 
  | nil => nil
  | a :: l => f a :: map f l
  end.

Variables A B C : Set.

Lemma map_comp : forall (l : list A)(f : A -> B)(g : B -> C),
  map g (map f l) = map (fun a => g (f a)) l.
intros.
induction l; simpl.
reflexivity.
rewrite IHl.
reflexivity.
Qed.



(**   Trees, Expressions, Compilers   *)

(** similar to lists *)

Inductive BinTree (X : Set) : Set :=
  leaf : X -> BinTree X
| node : BinTree X -> BinTree X -> BinTree X.


Fixpoint subst (A B : Set) (bina: BinTree A) (a2binb: A -> BinTree B) : BinTree B :=
    match bina with
      | leaf a     => a2binb a
      | node t1 t2 => node (subst t1 a2binb) (subst t2 a2binb)
    end.


Lemma rneutr : forall (t : BinTree A),
                   subst t (fun a => leaf a) = t.
intros.
induction t; simpl.
reflexivity.
rewrite IHt1.
rewrite IHt2.
reflexivity.
Qed.







End RevisionPart2.