(** Formal Type Theory, Autumn 2009, Exercise set 2

NAME(S) OF SUBMITTER(S):
                        
COMMENTS ON THE EXERCISE:


Send this file (with the problems solved) to ftt09@cs.helsinki.fi by 
2009-11-20 03:00+02
*)


(** This weeks exercises are all relatively straightforward induction
problems. That is, expect to see [induction] in every proof script.

Some general guidelines:

- use [intros] to introduce assumptions in order to prove an implication
  or universally quantified sentence

- use [destruct] to decompose simple inductive types, in particular to
  split a conjunction to its constituent propositions

- use [simpl] to perform "the right amount" of computation in a function
  application

- use [red] to "open up" a defined variable into the body of its definition

- use [apply] to use a lemma or other implication whose conclusion
  matches the goal (you can also use it if you have an assumption that
  matches the goal exactly). For proving a conjunction, [split] is a
  shorter alternative to [apply conj].

- special case with transitivity: often you want to apply a transitivity
  lemma of some sort without wanting to specify the middle element of
  the transitivity chain exactly. In these situations, [apply] won't
  work, but [eapply] can be used. It leaves an "existential variable"
  into the goal, which can then match anything you want as you prove the
  new goal.

- use [rewrite] to substitute between terms for which you have an
  equality proof

- use [reflexivity] to prove a definitional equality

- finally, use [induction] for induction *)

(** We move to Pierce's Software Foundations framework, so the file
Logic.v from there should be in Coq's include path while developing the
proofs.
 *)

Require Import Logic.


(** Problem 1.a (2 p)

Prove an auxiliary lemma showing that adding one to a summand adds one
to the sum. *)

Lemma plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).
Proof.
  intros n m.
  induction n as [| n'].
    Case "n = 0".
      admit. (* <- replace this with a proof script *)
    Case "n = S n'".
      admit. (* <- replace this with a proof script *)
Qed.

(** Problem 1.b (2 p)

Prove the commutativity of addition. You are going to need the above
lemma, as well as the previously proven [plus_0_r], the proof that zero
is the right identity of addition. *)

Lemma plus_comm : forall n m, n + m = m + n.
Proof.
Admitted. (* <- replace this with a proof script, and end it with [Qed.] *)


(** Problem 2.a (1 p)

Prove that the empty list is the right identity of list concatenation.

HINT: the structure of this proof is exactly similar to the structure of
the proof of [plus_0_r] *)

Lemma app_nil_end : forall A (l : list A), l ++ [] = l.
Proof.
Admitted.


(** Problem 2.b (2 p)

Study the files Lists.v and Poly.v to find the definition of [rev]
(reverse a list) and [snoc] (append a single element to the end of a
list). Then prove the following fact about the relationship between
them. *)

Lemma rev_snoc : forall A (l : list A) (a : A), rev (snoc l a) = a :: rev l.
Proof.
Admitted.


(** Problem 2.c (2 p)

With the use of the above lemma, prove that reversing a reversed list
yields the original list. *)

Lemma rev_involutive : forall A (l : list A), rev (rev l) = l.
Proof.
Admitted.



(** Problem 3.

Let us define the following inductive relationship: [precedes n m] holds
exactly when [n] immediately precedes [m], or in other words, [m] is the
successor of [n]. *)

Inductive precedes : nat -> nat -> Prop :=
  precedes_S : forall n, precedes n (S n).

(** The _transitive closure_ [TC R] of a relation [R] can be defined
inductively as follows (see TAPL 2.2.7): *)

Inductive TC {A : Type} (R : relation A) : relation A :=
  | tc_R : forall a b : A, R a b -> TC R a b
  | tc_trans : forall a b c : A, TC R a b -> TC R b c -> TC R a c
  .

(** A relation [R1] is a _subrelation_ of [R2], if whenever [R1 a b]
holds, [R2 a b] also holds. *)

Definition subrelation {A : Type} (R R' : relation A) := 
  forall a b : A, R a b -> R' a b.

(** Now study the definition of [lt] (and [le]) in Logic.v, and show
that the transitive closure of [precedes] is the same relation as [lt].
That is, [TC precedes] and [lt] are both subrelations of each other. *)

(* Problem 3.a (1 p) *)

Lemma TC_precedes_implies_lt : subrelation (TC precedes) lt.
Proof.
Admitted.


(* Problem 3.b (1 p) *)

Lemma lt_implies_TC_precedes : subrelation lt (TC precedes).
Proof.
Admitted.



(** Problem 4 (1 p)

The following exercise is conceptually slightly more complicated than
the previous ones, and requires a slightly longer proof. It doesn't
require any new techniques, but you may want to leave it last.

We say that [R] is the _smallest_ relation with the property [RP], if it:
 - has the property [RP], and
 - is a subrelation of every other relation that has the property [RP] *)

Definition smallest {A : Type} (RP : relation A -> Prop) (R : relation A) :=
  RP R /\ forall R' : relation A, RP R' -> subrelation R R'.

(** (TAPL 2.2.5) A relation [R1] is the [RP]-closure of a relation [R2], if it is the 
_smallest_ relation that:
 - has the property [RP], and
 - contains [R2] (i.e. [R2] is its subrelation) *)

Definition closure {A : Type} (RP : relation A -> Prop) (R1 R2 : relation A) :=
  smallest (fun R : relation A => RP R /\ subrelation R2 R) R1.


(** (TAPL 2.2.7) Show that for any relation [R], our inductive relation
[TC R] is exactly the transitive closure of [R] in the sense defined above. *)

Lemma TC_trans_clos : 
  forall (A : Type) (R : relation A), closure (@transitive A) (TC R) R.
Proof.
Admitted.