From LF Require Export Lists.

Inductive list (X : Type) : Type :=
| nil
| cons (x : X) (l : list X).

Fixpoint repeat X x count : list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat X x count')
  end.

Arguments nil {X}.
Arguments cons {X}.
Arguments repeat {X}.

Fixpoint app {X : Type} (l1 l2 : list X) : list X :=
  match l1 with
  | nil => l2
  | cons h t => cons h (app t l2)
  end.

Fixpoint rev {X : Type} (l: list X) : list X :=
  match l with
  | nil => nil
  | cons h t => app (rev t) (cons h nil)
  end.

Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil => 0
  | cons _ l' => S (length l')
  end.

Notation "x :: y" := (cons x y)
                       (at level 60, right associativity).

Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                       (at level 60, right associativity).

Theorem app_nil_r : forall (X: Type), forall l:list X,
    l ++ [] = l.
Proof.
  intros X.
  induction l as [ | h t IHt].
  - reflexivity.
  - simpl.
    rewrite IHt.
    reflexivity.
Qed.

Theorem app_assoc : forall A (l m n: list A),
    l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n.
  induction l as [ | h t IHt].
  - reflexivity.
  - simpl.
    rewrite IHt.
    reflexivity.
Qed.

Lemma app_length : forall X (l1 l2 : list X),
    length (l1 ++ l2) = length l1 + length l2.
Proof.
  intros X l1 l2.
  induction l1 as [ | h t IHt].
  - reflexivity.
  - simpl. rewrite IHt. reflexivity.
Qed.

Theorem rev_app_distr: forall X (l1 l2 : list X),
    rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros X l1 l2.
  induction l1 as [ | h t IHt].
  - simpl.
    rewrite app_nil_r.
    reflexivity.
  - simpl.
    rewrite IHt.
    rewrite app_assoc.
    reflexivity.
Qed.

Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y).

Arguments pair {X Y}.

Notation "( x , y )" := (pair x y).
Notation "X * Y" := (prod X Y) : type_scope.

Definition fst {X Y : Type} (p : X * Y) : X :=
  match p with
  | (x, y) => x
  end.

Definition snd {X Y : Type} (p : X * Y) : Y :=
  match p with
  | (x, y) => y
  end.

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y) : list (X * Y) :=
  match lx, ly with
  | [], _ => []
  | _, [] => []
  | x :: tx, y :: ty => (x, y) :: (combine tx ty)
  end.

Fixpoint split {X Y : Type} (l : list (X * Y)) : (list X) * (list Y) :=
  match l with
  | [] => ([], [])
  | (x, y) :: rest => match split rest with
                      | (xs, ys) => (x :: xs, y :: ys)
                      end
  end.

Fixpoint nth_error {X : Type} (l : list X) (n : nat) : option X :=
  match l with
  | nil => None
  | a :: l' => match n with
               | O => Some a
               | S n' => nth_error l' n'
               end
  end.

Definition hd_error {X : Type} (l : list X) : option X :=
  match l with
  | [] => None
  | h :: _ => Some h
  end.

Definition doit3times {X : Type} (f : X -> X) (n : X) : X :=
  f (f (f n)).

Fixpoint filter {X : Type} (test : X -> bool) (l : list X) : list X :=
  match l with
  | [] => []
  | h :: t => if test h
              then h :: (filter test t)
              else filter test t
  end.

Definition filter_even_gt_7 : list nat -> list nat :=
  filter (fun n => even n && (7 <? n)).

Definition partition {X : Type}
  (test : X -> bool)
  (l : list X)
  : list X * list X :=
  match l with
  | [] => ([], [])
  | h :: t => if test h
              then (h :: filter test t, filter (fun y => negb (test y)) t)
              else (filter test t, h :: filter (fun y => negb (test y)) t)
  end.

Fixpoint map {X Y : Type} (f : X -> Y) (l : list X) : list Y :=
  match l with
  | [] => []
  | h :: t => f h :: map f t
  end.

Theorem map_app : forall (X Y : Type) (f : X -> Y) (l1 l2 : list X),
    map f (l1 ++ l2) = map f l1 ++ map f l2.
Proof.
  intros X Y f l1 l2.
  induction l1 as [ | h t IHt].
  - reflexivity.
  - simpl.
    rewrite IHt.
    reflexivity.
Qed.
    
Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
    map f (rev l) = rev (map f l).
Proof.
  intros X Y f.
  induction l as [ | h t IHt].
  - reflexivity.
  - simpl.
    rewrite map_app.
    simpl.
    rewrite IHt.
    reflexivity.
Qed.

Fixpoint flat_map {X Y : Type} (f : X -> list Y) (l : list X) : list Y :=
  match l with
  | [] => []
  | h :: t => f h ++ flat_map f t
  end.

Definition option_map {X Y : Type} (f : X -> Y) (xo : option X) : option Y :=
  match xo with
  | None => None
  | Some x => Some (f x)
  end.

Fixpoint fold {X Y : Type} (f : X -> Y -> Y) (l : list X) (b : Y) : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

Definition constfun {X : Type} (x : X) : nat -> X :=
  fun (k : nat) => x.

Module Exercises.
  Definition fold_length {X : Type} (l : list X) : nat :=
    fold (fun _ n => S n) l 0.

  Theorem fold_length_correct : forall X (l : list X),
      fold_length l = length l.
  Proof.
    intros X.
    induction l as [ | h t IHt].
    - reflexivity.
    - simpl.
      rewrite <- IHt.
      reflexivity.
  Qed.

  Definition fold_map {X Y : Type} (f : X -> Y) (l : list X) : list Y :=
    fold (fun x acc => f x :: acc) l [].

  Theorem fold_map_correct : forall X Y (f : X -> Y) (l : list X),
      fold_map f l = map f l.
  Proof.
    intros X Y f.
    induction l as [ | h t IHt].
    - reflexivity.
    - simpl.
      rewrite <- IHt.
      reflexivity.
  Qed.

  Definition prod_curry {X Y Z : Type}
    (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).

  Definition prod_uncurry {X Y Z : Type}
    (f : X -> Y -> Z) (p : X * Y) : Z :=
    match p with
    | (x, y) => f x y
    end.

  Theorem uncurry_curry : forall (X Y Z : Type)
                                 (f : X -> Y -> Z)
                                 x y,
      prod_curry (prod_uncurry f) x y = f x y.
  Proof.
    intros X Y Z f x y.
    unfold prod_uncurry.
    unfold prod_curry.
    reflexivity.
  Qed.

  Theorem curry_uncurry : forall (X Y Z : Type)
                                 (f : X * Y -> Z)
                                 x y,
      prod_uncurry (prod_curry f) (x, y) = f (x, y).
  Proof.
    intros X Y Z f x y.
    unfold prod_uncurry, prod_curry.
    reflexivity.
  Qed.
  
  Module Church.
    Definition cnat := forall X : Type, (X -> X) -> X -> X.

    Definition zero : cnat :=
      fun (X : Type) (f : X -> X) (x : X) => x.

    Definition scc (n : cnat) : cnat :=
      fun (X : Type) (f : X -> X) (x : X) => f ((n X f) x).

    Definition one := scc zero.
    Definition two := scc one.

    Definition plus (n m : cnat) : cnat :=
      fun (X : Type) (f : X -> X) (x : X) => (n X f) ((m X f) x).

    Definition mult (n m : cnat) : cnat :=
      fun (X : Type) (f : X -> X) (x : X) =>
        (m X (n X f)) x.

  End Church.
End Exercises.