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

    Exercise 6
    published 3/11/08, deadline 10/11/08, 17:00 electronic submission

    Use
    $ cw submit ex06.v
    on one of the CS servers
    then look for the coursework 227 labelled 'g52mc2 coursework 6' 
    and enter the associated code.

    Multiple submissions are allowed, up to the deadline.

    Fill in the missing proofs. You are only supposed to use the
    tactics introduced in the lectures, e.g.
    cut, exact, assumption, intro(s), apply, split, elim, left, right, case,
    exists, reflexivity, rewrite(<-), pattern, discriminate, destruct, induction

    If you want to use another simple tactic not on the list, please
    check with your tutor.
**)

Section ex6.

(* repeating some definitions from the lecture. *)
Fixpoint is_even (n : nat) {struct n} : bool :=
  match n with
  | 0 => true
  | S m => negb (is_even m)
  end.

Fixpoint double  (n : nat) {struct n} : nat :=
  match n with
  | 0 => 0
  | S m => S (S (double m))
  end.

(* show that double always produce even numbers. Use induction! *)
Goal forall n : nat, is_even (double n) = true.
intro n.
induction n.
reflexivity.
simpl.
rewrite IHn.
simpl.
reflexivity.
Qed.

(* For the following we import a library module: *)
Require Import Coq.Arith.Plus.
(*
It provides the following lemmas:

Lemma plus_0_l : forall n, 0 + n = n.
Lemma plus_0_r : forall n, n + 0 = n.
Lemma plus_comm : forall n m, n + m = m + n.
Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.

and more, see http://coq.inria.fr/stdlib/Coq.Arith.Plus.html
*)

Lemma double_lem : forall n:nat, double n = n+n.
intro.
induction n.
  reflexivity.
  simpl.
  rewrite IHn.
  pattern (n + S n).
  rewrite plus_comm.
  reflexivity.
Qed.

(* We are defining multiplication: *)
Fixpoint mult (n m:nat) {struct n} : nat :=
  match n with
  | O => 0
  | S n' => m + mult n' m
  end.

Notation "n * m" := (mult n m).

(* Show that the law of distributivity holds: *)
Goal forall (i j k:nat), i*(j+k) = i*j + i*k.
intros i j k.
induction i.
reflexivity.
simpl.
rewrite IHi.
rewrite<- plus_assoc.
pattern (k + (i * j + i * k)).
rewrite plus_assoc.
pattern (k + i * j).
rewrite plus_comm.
pattern (i * j + k + i * k).
rewrite<- plus_assoc.
rewrite plus_assoc.
reflexivity.
Qed.

(* We define Le m n = less or equal *)

Definition Le (m n : nat) := exists k:nat, k+m = n.
Notation "n <= m" := (Le n m).

(* Show that <= is a "partial order", i.e. it is
   reflexive, transitive and antisymmetric. 
*)

Lemma le_refl: forall n:nat,n <= n.
intro n.
exists 0.
reflexivity.
Qed.

Lemma le_trans : forall (l m n : nat), l <= m -> m <= n -> l <= n.
intros l m n lm mn.
destruct lm as [k klm].
destruct mn as [j jmn].
exists (j+k).
rewrite<- jmn.
rewrite<- klm.
rewrite-> plus_assoc.
reflexivity.
Qed.


Lemma asym_lem1 : forall (k j : nat), j+k=0 -> k=0.
intros k j.
induction j.
intro k0.
exact k0.
intro s0.
discriminate s0.
Qed.

Lemma asym_lem2 : forall (k n : nat), n+k = n -> k=0. 
intros k n.
induction n.
intro k0.
exact k0.
intro snk.
apply IHn.
injection snk.
intro nkn.
exact nkn.
Qed.

Lemma le_asym : forall (m n : nat), m <= n -> n <= m -> m=n.
intros m n mn nm.
destruct mn as [k kmn].
destruct nm as [j jnm].
cut (k=0).
intro k0.
replace m with (k+m).
exact kmn.
rewrite k0.
reflexivity.
cut ((k+j)+n = n).
intro kjn.
cut (k+j = 0).
intro kj0.
eapply asym_lem1.
rewrite plus_comm.
apply kj0.
eapply asym_lem2.
rewrite plus_comm.
apply kjn.
pattern n at 2.
rewrite<- kmn.
rewrite<- jnm.
rewrite plus_assoc.
reflexivity.
Qed.