(** Mathematics for Computer Scientists 2 (G52MC2)
    Thorsten Altenkirch

    L04 (Bool and predicate logic)

    This lecture introduces propositional logic using the proof
    assistant Coq.  The material in this file contains coq proofs
    which can be read and animated with coqide or xemacs+proofgeneral.

**)

Section l04.

Require Import Coq.Bool.Bool. (* not sure why I need this. *)

(* bool is defined in the standard prelude: *)
Print bool.
Check bool.
Check true.

(* We redefine some library functions, e.g. *)

Definition negb(b:bool) : bool :=
  if b then false else true.

Eval compute in (negb true).

Definition andb(b c:bool) : bool :=
  if b then c else false.
 
Eval compute in (andb true false).

Eval compute in (true && false).

Definition orb (b c : bool) : bool :=
  if c then true else b.

Eval compute in (true || false).

(* reasoning about functions on bool *)

Lemma negb_involutive : 
     forall b:bool, negb (negb b) = b.
intros.
case b.
unfold negb.
reflexivity.
unfold negb.
reflexivity.
Qed.

Lemma andb_comm : 
  forall a b : bool, a && b = b && a.
intros.
case a.
simpl.
case b.
simpl.
reflexivity.
reflexivity.
case b.
reflexivity.
reflexivity.
Qed.

(* properties of bool *)

Lemma true_or_false : 
 forall b : bool, b = true \/ b = false.
intro b.
case b.
left.
reflexivity.
right.
reflexivity.
Qed.


(* reasoning with equality *)

Lemma use_rewrite : 
forall b:bool, b = true 
               -> negb b = false.
intros b hb.
rewrite hb.
unfold negb.
reflexivity.
Qed.


(* true != false *)

Definition Is_true (b:bool) : Prop :=
   if b then True else False.

Lemma diff_true_false : 
      (true = false) -> False.
intro tf.
fold (Is_true false).
rewrite<- tf.
simpl.
split.
Qed.

(* In practice we use a tactic: *)
Goal true <> false.
intro tf.
discriminate tf.
Qed.

(* verifying andb *)

Lemma andb_compl: 
forall a b : bool, a=true /\ b=true 
     -> a && b = true.
intros.
destruct H as [Ha Hb].
rewrite Ha.
simpl.
exact Hb.
Qed.

Lemma andb_sound : 
forall a b : bool, a && b = true 
     -> a=true /\ b=true.
intros a b.
case a.
intro hb.
split.
reflexivity.
exact hb.
intro hb.
discriminate hb.
Qed.

Theorem andb_ok : 
forall a b : bool, a=true /\ b=true 
               <-> a && b = true.
split.
apply andb_compl.
apply andb_sound.
Qed.

(* existential quantification *)

Lemma ex1 : exists b : bool, b && negb b = b.
exists false.
reflexivity.
Qed.

Lemma ex2 : forall a:bool, (exists b:bool,b && a = true) -> a=true.
intros a h.
elim h.
intros b.
case b.
intro ha.
exact ha.
intro ha.
discriminate ha.
Qed.

(* universal quantification over bool *)

Definition allb (p : bool -> bool) : bool :=
  p true && p false.

Lemma allb_compl : forall (p : bool -> bool),
  (forall b:bool, p b = true) -> (allb p = true).
intros p hp.
unfold allb.
apply andb_compl.
split.
apply hp.
apply hp.
Qed.

Theorem allb_sound: forall (p : bool -> bool),
  (allb p = true) -> (forall b:bool, p b = true).
intros p hp b.
cut (p true = true /\ p false = true).
intros hp'.
destruct hp' as [hpt hpf].
case b.
exact hpt.
exact hpf.
apply andb_sound.
exact hp.
Qed.

Theorem allb_ok: forall (p : bool -> bool),
  (forall b:bool, p b = true) <-> (allb p = true).
split.
apply allb_compl.
apply allb_sound.
Qed.