Require Arith.
Require ZArith.
Require EqNat.

Require dec.


(**
 * Polymorphic lists.
 *)

Inductive list [A:Set]: Set :=
   Nil: (list A)
 | Cons: A -> (list A) -> (list A).

(* Length of a list *)

Fixpoint length [A:Set; l:(list A)]: nat :=
   Cases l of
      Nil        => O
    | (Cons a r) => (S (length A r))
   end.

Lemma length_0: (A:Set; l:(list A))(length A l)=O -> (l=(Nil A)).
Proof.
   Intros A l. Case l.
   Reflexivity.
   Simpl. Intros. Discriminate H.
Qed.

Lemma length_S:
   (A:Set; l:(list A); n:nat)(length A l)=(S n)->
      (EX h:A | (EX t:(list A) | l=(Cons A h t) /\ (length A t)=n)).
Proof.
   Intros A l. Case l.
   Simpl. Intros. Discriminate H.
   Simpl. Intros h0 t0 n H. Injection H. Intro. 
   Split with h0. Split with t0. Split.
   Reflexivity. Assumption.
Qed.

(* Map a function over a list *)

Fixpoint map [A,B:Set; f:A->B; l:(list A)]: (list B) :=
   Cases l of
      Nil        => (Nil B)
    | (Cons a r) => (Cons B (f a) (map A B f r))
   end.

Lemma length_map:
   (A,B:Set)(f:A->B)(l:(list A))(length A l)=(length B (map A B f l)).
Proof.
   Induction l.
   Simpl. Reflexivity.
   Simpl. Intros. Rewrite H. Reflexivity.
Qed.

(* Checks that all members of a list are P *)

Fixpoint alllist [A:Set; P:A->Prop; qlist:(list A)]: Prop :=
   Cases qlist of
        Nil        => True
      | (Cons m l) => ((P m) /\ (alllist A P l))
   end.

(* Checks that some member of a list is P *)

Fixpoint exlist [A:Set; P:A->Prop; qlist:(list A)]: Prop :=
   Cases qlist of
        Nil        => False
      | (Cons m l) => ((P m) \/ (exlist A P l))
   end.

(* Membership *)

Definition inlist := [A:Set; a:A](exlist A [b:A]a=b).

Lemma inlist_head_eq:
   (A:Set; x,y:A; l:(list A))x=y->(inlist A x (Cons A y l)).
Proof.
   Intros. Unfold inlist. Simpl.
   Left. Assumption.
Qed.

Lemma inlist_head_neq:
   (A:Set; x,y:A; l:(list A))~x=y->(inlist A x (Cons A y l))<->(inlist A x l).
Proof.
   Intros. Unfold inlist. Simpl.
   Split.
   Intros. Elim H0. Intro. Elim H. Assumption.
   Intros. Assumption.
   Intros. Right. Assumption.
Qed.

Lemma inlist_tail:
   (A:Set; x,y:A; l:(list A))(inlist A x l)->(inlist A x (Cons A y l)).
Proof.
   Intros. Unfold inlist. Simpl. Right. Assumption.
Qed.

(* alllist and exlist behave nicely *)

Theorem alllist_ok:
   (A:Set; P:A->Prop; qlist:(list A))
      (alllist A P qlist) <-> (q:A)(inlist A q qlist)->(P q).
Proof.
   Split.

   (* -> *)
   Elim qlist.
   Unfold inlist. Simpl. Intros. Elim H0.
   Unfold inlist. Simpl. Intros q l IH H. Elim H. Intros. Elim H2.
   Intro. Rewrite H3. Assumption.  
   Intro. Apply IH. Assumption. Assumption.

   (* <- *)
   Elim qlist.
   Unfold inlist. Simpl. Intros. Trivial.
   Unfold inlist. Simpl. Intros q l IH H. Split.
   Apply H. Left. Reflexivity.
   Apply IH. Intros. Apply H. Right. Assumption.
Qed.

Theorem exlist_ok:
   (A:Set; P:A->Prop; qlist:(list A))
      (exlist A P qlist) <-> (EX q:A | (inlist A q qlist)/\(P q)).
Proof.
   Split.

   (* -> *)
   Elim qlist.
   Unfold inlist. Simpl. Intros. Elim H.
   Unfold inlist. Simpl. Intros q l IH H. Elim H.
   Intro. Split with q. Split. Left. Reflexivity. Assumption.
   Intro. Elim IH. Intros q1 Hq1. Elim Hq1. Intros. Split with q1.
   Split. Right. Assumption. Assumption. Assumption.

   (* <- *)
   Elim qlist.
   Unfold inlist. Simpl. Intros. Elim H. Intros. Elim H0. Intros. Elim H1.
   Unfold inlist. Simpl. Intros q l IH H. Elim H.
   Intros q1 Hq1. Elim Hq1. Intros. Elim H0.
   Intro. Left. Rewrite <- H2. Assumption.
   Intro. Right. Apply IH. Split with q1. Split. Assumption. Assumption.
Qed.


(**
 * Lists of natural numbers.
 *)

Definition natlist := (list nat).

(* Multiply all elements of a natlist *)

Fixpoint product [qlist:natlist] : nat :=
   Cases qlist of
        Nil        => (1)
      | (Cons m l) => (mult m (product l))
   end.

(* Drop the first occurance of q from qlist *)

Fixpoint drop [q:nat; qlist:natlist]: natlist :=
   Cases qlist of
      Nil         => (Nil nat)
    | (Cons q' l) => (if (beq_nat q q') then l else (Cons nat q' (drop q l)))
   end.

(* Multiply all elements of qlist, except for (first occurance of) q *)

Definition multDrop := [q:nat; l:natlist](product (drop q l)).

Lemma multdrop_cons_eq:
   (q:nat; l:natlist)(multDrop q (Cons nat q l))=(product l).
Proof.
   Unfold multDrop. Simpl. Intros. Elim (beq_nat_eq q q). Intros.
   Rewrite H. Reflexivity. Reflexivity.
Qed.

Lemma multdrop_cons_neq:
   (p,q:nat; l:natlist)
      ~p=q->
         (multDrop p (Cons nat q l))=(mult q (multDrop p l)).
Proof.
   Unfold multDrop. Simpl. Intros. Elim (beq_nat_neq p q). Intros.
   Rewrite H0. Simpl. Reflexivity. Assumption.
Qed.

Lemma multdrop_mult:
   (qlist:natlist; q:nat)
      (inlist nat q qlist)->(mult q (multDrop q qlist))=(product qlist).
Proof.
   Induction qlist.
   Simpl. Intros. Elim H.
   Simpl. Intros q1 l IH. Intros. Elim (eqdec q q1).

   (* case q=q1 *)
   Intro. Rewrite H0. Rewrite multdrop_cons_eq. Reflexivity.

   (* case ~q=q1 *)
   Intro. Rewrite multdrop_cons_neq.
   Rewrite <- (IH q). Rewrite mult_assoc_l.
   Rewrite (mult_sym q q1). Rewrite mult_assoc_l. Reflexivity.
   Unfold inlist in H. Simpl in H. Elim H.
   Intro. Elim H0. Assumption.  
   Intro. Assumption.
   Assumption.
Qed.


(**
 * Lists of integers.
 *)

Definition Zlist := (list Z).

(* Multiply all elements of a Zlist *)

Fixpoint zproduct [l:Zlist] : Z :=
   Cases l of
      Nil        => `1`
    | (Cons x t) => `x*(zproduct t)`
   end.

(* Drop an element from a Zlist *)

Fixpoint zdrop [x:Z; l:Zlist]: Zlist :=
   Cases l of
      Nil        => (Nil Z)
    | (Cons h t) => (if (Zeq_bool x h) then t else (Cons Z h (zdrop x t)))
   end.

Lemma zdrop_head_eq:
   (x,y:Z; l:Zlist)x=y->(zdrop x (Cons Z y l))=l.
Proof.
   Simpl. Intros. Elim (zeq_bool_eq x y). Intros.
   Rewrite H0. Reflexivity. Assumption.
Qed.

Lemma zdrop_head_neq:
   (x,y:Z; l:Zlist)~x=y->(zdrop x (Cons Z y l))=(Cons Z y (zdrop x l)).
Proof.
   Simpl. Intros. Elim (zeq_bool_neq x y). Intros.
   Rewrite H0. Reflexivity. Assumption.
Qed.

Lemma length_zdrop:
   (x:Z; l:Zlist)
      (inlist Z x l)->(S (length Z (zdrop x l)))=(length Z l).
Proof.
   Induction l.
   Unfold inlist. Simpl. Intros. Elim H.
   Intros h t IH. Intros. Elim (zeqdec x h).

   (* case x=h *)
   Intro. Simpl. Elim (zeq_bool_eq x h).
   Intros. Rewrite H1. Reflexivity. Assumption.

   (* case x<>h *)
   Intro. Simpl. Elim (zeq_bool_neq x h).
   Intros. Rewrite H1. Simpl. Rewrite IH. Reflexivity.
   Elim H. Intros. Elim H0. Assumption. Intros. Assumption. Assumption.
Qed.

Lemma zdrop_inlist_preserve:
   (x,y:Z; l:Zlist)(inlist Z x (zdrop y l))->(inlist Z x l).
Proof.
   Induction l.
   Unfold inlist. Simpl. Intro. Assumption.
   Intros h t IH. Intros.
   Elim (zeqdec x h).
   Intro. Rewrite H0. Unfold inlist. Simpl. Left. Reflexivity.
   Intro. Elim (zeqdec y h).
   Intro. Rewrite H1 in H. Rewrite zdrop_head_eq in H.
   Apply inlist_tail. Assumption. Reflexivity.
   Intro. Rewrite zdrop_head_neq in H.
   Unfold inlist in H. Simpl in H. Elim H.
   Intro. Elim H0. Assumption.
   Intros. Apply inlist_tail. Apply IH. Assumption.
   Assumption.
Qed.


(* Multiply all elements except first occurance of x *)

Definition zmultDrop := [x:Z; l:Zlist](zproduct (zdrop x l)).

Lemma zmultdrop_cons_eq:
   (q:Z; l:Zlist)(zmultDrop q (Cons Z q l))=(zproduct l).
Proof.
   Unfold zmultDrop. Simpl. Intros. Elim (zeq_bool_eq q q). Intros.
   Rewrite H. Reflexivity. Reflexivity.
Qed.

Lemma zmultdrop_cons_neq:
   (p,q:Z; l:Zlist)
      ~p=q->
         (zmultDrop p (Cons Z q l))= (Zmult q (zmultDrop p l)).
Proof.
   Unfold zmultDrop. Simpl. Intros. Elim (zeq_bool_neq p q). Intros.
   Rewrite H0. Simpl. Reflexivity. Assumption.
Qed.

Lemma zmultdrop_mult:
   (qlist:Zlist; q:Z)
      (inlist Z q qlist)->(Zmult q (zmultDrop q qlist))=(zproduct qlist).
Proof.
   Induction qlist.
   Simpl. Intros. Elim H.
   Simpl. Intros q1 l IH. Intros. Elim (zeqdec q q1).

   (* case q=q1 *)
   Intro. Rewrite H0. Rewrite zmultdrop_cons_eq. Reflexivity.

   (* case ~q=q1 *)
   Intro. Rewrite zmultdrop_cons_neq.
   Rewrite <- (IH q). Rewrite Zmult_assoc_l.
   Rewrite (Zmult_sym q q1). Rewrite Zmult_assoc_l. Reflexivity.
   Unfold inlist in H. Simpl in H. Elim H.
   Intro. Elim H0. Assumption.
   Intro. Assumption.
   Assumption.
Qed.

(* Multiply all elements in list with a *)

Definition mapmult := [a:Z; l:Zlist](map Z Z [x:Z]`a*x` l).

Lemma mapmult_image:
   (a:Z)(l:Zlist)(x:Z)(inlist Z x l)->(inlist Z `a*x` (mapmult a l)).
Proof.
   Unfold mapmult. Unfold inlist. Induction l.
   Simpl. Intros. Assumption.
   Simpl. Intros h t IH. Intros. Elim H.
   Left. Rewrite H0. Reflexivity.
   Right. Apply IH. Assumption.
Qed.

Lemma mapmult_orig:
   (a:Z)(l:Zlist)
      (y:Z)(inlist Z y (mapmult a l))->
         (EX x:Z | (inlist Z x l) /\ `y=a*x`).
Proof.
   Unfold mapmult. Unfold inlist. Induction l.
   Simpl. Intros. Elim H.
   Simpl. Intros h t IH. Intros.
   Elim H.
   Intro. Split with h. Split. Left. Reflexivity. Assumption.
   Intro. Elim (IH y). Intros. Elim H1. Intros.
   Split with x. Split. Right.
   Assumption. Assumption. Assumption.
Qed.