(*
Proving with computer assistance, February 2006.
Exercises with the proof assistant Coq

Coq a free program available via the site http://coq.inria.fr/. There
are compiled binary versions for Linux and Windows. This script
uses the syntax of Coq v8.0 and is not compatible with the earlier
versions of Coq.

For this practicum it is recommended that you install Coq IDE

Minimum recommended set of exercises: 1,4,8

For more information, look at:

 http://www.win.tue.nl/~fdechesn/2IF48/.

*)

Section Introduction.

(* Using the command Goal we enter the proof mode and set the proposition
that we will try to prove. *)

Goal forall A B C:Prop, (A->B->C)->(A->B)->(A->C).

intros.
apply H.
assumption.
apply H0.
assumption.

(*The proof is now complete. It can be saved for future use with the command
Save, followed by a name for the new theorem. This also ends the proof mode.*)

Save Tautology1.

(* To prove and save the result above, we could also have stated it as a Theorem
or Lemma, as follows: 

Theorem (or Lemma) Tautology1: 
forall A B C:Prop, (A->B->C)->(A->B)->(A->C).
Proof.
[...]
Qed.

With Qed. the proof is validated and added to the environment. *)

(*
The natural numbers are pre-defined in Coq as
 nat: Set
Check that with the command
 Check nat.
The terms 'O' and 'S' represent the natural number zero and the
successor function (adding of 1). Check their types with the Check
command.*)
Check nat.
Check O.
Check S.

(* the function that adds two to its argument can be defined as *)

Definition Add_two := fun x:nat=>(S(S x)).

(* But also, the number two can be defined as *)

Definition two := (S(S O)).

(* and used in the definition of the function: *)

Definition AddsTwo := fun x:nat=>x+two.


(*
One example on how the notion of equality can be introduced in Coq.

(Note: Coq has already a built-in equality denoted by the symbol =,
 but in this example we define our own).
*)

Variable IS : forall A:Set, A->A->Prop.

(*The line above only defines IS as a binary relation on an arbitrary
set A - this is a polymorphic equality. Reflexivity can be introduced by an extra axiom:
*)

Axiom refl: forall (A:Set) (z:A), (IS A z z).

(*Now we should be able to prove 'IS nat (Add_two O) two' and really this is the case
as shown below  *)

Goal (IS nat (Add_two O) two).
apply refl.
Qed.

Goal (IS nat (AddsTwo O) two).
apply refl.
Qed.

(* What happened here?  Coq sees that (IS nat (Add_two O) twee) is an instance of
the reflexivity axiom (IS A z z). It takes nat for the set A. For z Coq takes two,
but two is (by definition) equal to (Add_2 O). This check is performed automatically
as follows:

 (Add_two O) =                              (By unfolding Add_two)
  = ((fun x:nat =>(S(S x))) O) =      (By beta-reduction)
  = S(S O) =                                   (By the definition of two)
  = two

Hence, when comparing two terms, Coq folds or unfolds definitions as necessary *)


(* ==========================================================================*)


(* This example shows how we can do classical logic in Coq

Suppose we want to prove that for all propositions A and B the following holds:
((not A) -> B) -> ((not B) -> A).
Let us give this proposition the name contra (from contraposition): *)

Definition contra := forall A B:Prop,((not A)->B)->((not B)->A).

(* Note that 'not' is defined as fun A:Prop=>A->False. Also, Coq abbreviates (not A) by ~A *)
Print not.
Print contra.

(*
You can try to prove contra using the tauto or the intuition tactic:
 Goal contra.
 tauto.
Unfortunately, Coq cannot prove contra with the tactic tauto or intuition, because it is
not provable in the constructive logic of Coq. To prove this proposition, we
need the axiom for double negation: *)

Hypothesis classical : forall A:Prop,(not(not A))->A.

(* With this extra axiom we can prove contra *)

Goal contra.
unfold contra.
intros.
apply classical.
(* the goal at this moment is

  A : Prop
  B : Prop
  H : ~A->B
  H0 : ~B
  ===================
  ~~A

Note again the use of ~ for denoting negation.Since ~~A can also be written as ~A->False,
*)

intro.

(*
This results in the following goal:
  A : Prop
  B : Prop
  H : ~A->B
  H0 : ~B
  H1 : ~A
  ===================
  False

In this context, from H and H1 we can obtain a proof of B
and since H0 is a proof of ~B (i.e. B->False), we will get False. However, Coq always
works in a backwards manner, we need to use first H0 (and then the goal will be to prove B).
Next, to prove B, we will need to use H (and the goal will become ~A). The final step will
be trivial, because H1 is a proof of ~A.
*)

apply H0.

(*
  A : Prop
  B : Prop
  H : ~A->B
  H0 : ~B
  H1 : ~A
  ===================
  B
*)
apply H.

(*
  A : Prop
  B : Prop
  H : ~A->B
  H0 : ~B
  H1 : ~A
  ===================
  ~A
*)


assumption.


(* To see the proof-term that we created, use Show Proof:*)
Show Proof.

(*
Proof: fun (A B : Prop)(H : ~A->B)(H0 : ~B) =>
    classical A (fun H1 : ~A => H0 (H H1))

Although we prove a formula in classical logic, you can still use the
automated tactics of Coq. They will work for subgoals that do not require
the axiom 'classical'*)
Qed.

(* The part with the worked-out examples ends here. Now you can try to
prove the exercises below yourself.*)

End Introduction.

(* ===========================================================*)

(*
Exercise 1. (implications)
Prove the following propositions: *)
Lemma L1_1: forall p q r:Prop, (p->q)->(q->r)->(p->r).

Lemma L1_2: forall p q:Prop,(p->p->q)->(p->q).

Lemma L1_3: forall p q:Prop, (p->q)->(p->p->q).

Lemma L1_4: forall p q r:Prop, (p->q->r)->(q->p->r).


(*
Exercise 2. (falsum) Define False as follows: *)

Definition False := forall p:Prop, p : Prop.

Check False.

(* Prove that from False follows any other proposition, i.e. prove the following *)

Lemma ex_falso: forall p:Prop,(False -> p).

(* Save the proof for later use with Save.*)

Print not.

(*
prove the following propositions: *)

Lemma L2_1: forall p q:Prop, (p->q)->~q->~p.


Lemma L2_2: forall p:Prop, p->~~p.

Lemma L2_3: forall p:Prop,~~~p->~p.

(*
Exercise 3. Introduce the following axiom *)

Axiom classical: forall p:Prop, ~~p->p.

(* Using it prove: *)

Lemma L3_1: forall p q:Prop, (~q->~p)->(p->q).

Lemma L3_2: forall p q:Prop, ((p->q)->p)->p.

(*
Exercise 4. (conjunction) Define conjunction by *)

Definition AND := (fun (p q:Prop) => (forall (a:Prop), (p->q->a)->a)): Prop->Prop->Prop.

Lemma projl: forall p q:Prop, (AND p q)->p.

Lemma projr: forall p q:Prop, (AND p q)->q.

Lemma pair:  forall p q:Prop, (p->q->(AND p q)).

(* Note: Coq defines conjunction and disjunction in a different way that we are not
using here. More information on this can be found in the Coq tutorial (see the Coq homepage) *)


(* Exercise 5. (disjunction) Define disjunction as follows *)

Definition OR := (fun p q:Prop => forall (a:Prop), (p->a)->(q->a)->a): Prop->Prop->Prop.

(* Prove the following tautologies: *)

Lemma inl: forall p q:Prop, p->(OR p q).

Lemma inr: forall p q:Prop, q->(OR p q).

(* Exercise 7. (more junctions) Prove the following using the lemmas proved in Exercise 5 and 6: *)

Lemma L7_1: forall (p q:Prop),(AND p q)->(OR q p).

Lemma L7_2: forall (p q:Prop),(AND p q)->(AND q p).

Lemma L7_3: forall (p q r :Prop), (OR (OR p q) r)->(OR p (OR q r)).


(* Exercise 8 (Inductive types)

Define the type of the finite lists of natural numbers: *)

Inductive List: Set:=
  nil :List |
  cons : nat -> List -> List.

(* Coq defines automatically the corresponding induction principle: *)
Check List_ind.

(* Hence we can prove properties of lists of natural numbers by induction.
Furthermore, we can define functions with recursion: *)

(* Length of a list *)
Fixpoint Len(L:List):nat :=
 match L with
   nil => O |
  (cons n R) => (S (Len R))
end.

(* Appending two lists *)
Fixpoint Append(L:List):List->List :=
fun R:List =>
 match L with
  nil => R |
 (cons n T) => (cons n (Append T R))
end.

Print Append.

(* Prove the following: *)

Lemma L8_1:(Len nil)=O.


Lemma L8_2: forall (L R:List), (plus (Len L) (Len R))=(Len (Append L R)).

(* We define a function Reverse that given a list returns another list with
the elements of the first in reverse order *)

Fixpoint Reverse (L:List):List :=
 match L with
  nil => nil |
 (cons n R) => (Append (Reverse R) (cons n nil))
end.

Lemma L8_3: (Reverse nil) = nil.

Lemma L8_4: forall a b:nat,(Reverse (cons a (cons b nil)))=(cons b (cons a nil)).

(* Use these lemma's without proofs in L8_5 *)
Axiom help_8_5_1: forall (L R:List), (Len (Append L R))=(plus (Len L) (Len R)).

Axiom help_8_5_2: forall (x y:nat), (plus x y)=(plus y x).

(* Prove that Reverse returns a list of the same size as its argument *)
Lemma L8_5: forall (L:List), (Len (Reverse L))=(Len L).

(* Prove that if we apply Reverse two times we get back the original list *)

Lemma L8_6:forall (L R T:List), (Append (Append L R) T)=(Append L (Append R T)).

Lemma L8_7: forall (L R:List), (Reverse (Append L R))= (Append (Reverse R) (Reverse L)).
Lemma RevInv: forall (L:List), L = (Reverse (Reverse L)).

(*
Exercise 9. (naive set representation) Introduce a variable U of type Set.: *)

Variable U:Set.

(* We can think of the predicates on U as sets, i.e. U is the 'universe' of all objects
and a set is a predicate that describes which of the elements of the universe belong to it.
If A is of type U -> Prop then A can be seen as the set {x:U | A(x)}, the elements of U for which
the predicate holds. Hence we define*)

Definition SET := U -> Prop.

(* If A : SET and x : U then (A x) means `x is an element of A'. *)

(* 1. Define the subset relation on SET. *)
Definition subset:= fun (P Q:SET) => forall (x:U), (P x)->(Q x).
Check subset.

(* 2. Prove that subset is reflexive and transitive *)
Lemma L9_1: forall (A:SET), (subset A A).

Lemma L9_2: forall (A B C:SET), (subset A B) ->(subset B C)->(subset A C).

(* 3. Using subset, define equality, union and intersection of SETs. *)
Definition eq_set:= fun (A B:SET)=>(subset A B)/\(subset B A).
Definition Union:= fun (A B:SET)(x:U)=>(A x)\/(B x).
Definition Intersection:= fun (A B:SET) (x:U)=> (A x)/\(B x).

(* 4. Prove *)
Lemma L9_3: forall (A B:SET),(subset (Intersection A B) A).

Lemma L9_4: forall (A B:SET),(subset A (Union A B)).

Lemma L9_5: forall (A:SET), (eq_set (Union A A) A).

(* 5. Define the empty set and prove that it is a subset of every other SET. *)

Definition empty:= fun(x:U)=>False.

Lemma L9_6: forall (A:SET), (subset empty A).