Software Foundations: Polymorphism and Higher-Order Functions

Poly.v

Require Import Basics.
Require Import List.

Lemma map_app : forall (A B : Type) (f : A -> B) (l1 l2 : list A),
  map f (l1 ++ l2) = map f l1 ++ map f l2.
Proof.
  intros A B f l1 l2.
  induction l1.
  - reflexivity.
  - simpl. rewrite -> IHl1. reflexivity.
Qed.

Theorem map_rev : forall (A B : Type) (f : A -> B) (l : list A),
  map f (rev l) = rev (map f l).
Proof.
  intros A B f l.
  induction l.
  - reflexivity.
  - simpl. rewrite -> map_app. rewrite -> IHl. reflexivity.
Qed.

Theorem fold_length : forall (A : Type) (l : list A),
  fold_right (const S) 0 l = length l.
Proof.
  intros A l.
  induction l.
  - reflexivity.
  - simpl. rewrite -> IHl. reflexivity.
Qed.

Theorem fold_map : forall (A B : Type) (f : A -> B) (l : list A),
  fold_right (fun a l => f a :: l) nil l = map f l.
Proof.
  intros A B f l.
  induction l.
  - reflexivity.
  - simpl. rewrite -> IHl. reflexivity.
Qed.

Theorem length_error : forall {A : Type} (l : list A) (n : nat),
  length l = n -> nth_error l n = None.
Proof.
  intros A l.
  induction l.
  - intros []. reflexivity. reflexivity.
  - intros [] H.
    + discriminate H.
    + injection H. apply IHl.
Qed.