Lecture 02 Exercises

infer some type arguments automatically

Set Implicit Arguments.

Inductive list (A: Set) : Set :=
| nil : list A
| cons : A -> list A -> list A.

Arguments nil {A}.

Fixpoint length (A: Set) (l: list A) : nat :=
  match l with
  | nil => O
  | cons x xs => S (length xs)
  end.

add one list to the end of another

Fixpoint app (A: Set) (l1: list A) (l2: list A) : list A :=
  match l1 with
  | nil => l2
  | cons x xs => cons x (app xs l2)
  end.

Theorem app_nil:
  forall A (l: list A),
  app l nil = l.
Proof.
  intros.
  induction l.
  + simpl. reflexivity.
  + simpl. rewrite IHl. reflexivity.
Qed.

Theorem app_assoc:
  forall A (l1 l2 l3: list A),
  app (app l1 l2) l3 = app l1 (app l2 l3).
Proof.
  intros.
  induction l1.
  + simpl. reflexivity.
  + simpl. rewrite IHl1. reflexivity.
Qed.

simple but inefficient way to reverse a list

Fixpoint rev (A: Set) (l: list A) : list A :=
  match l with
  | nil => nil
  | cons x xs => app (rev xs) (cons x nil)
  end.

tail recursion is faster, but more complicated

Fixpoint fast_rev_aux (A: Set) (l: list A) (acc: list A) : list A :=
  match l with
  | nil => acc
  | cons x xs => fast_rev_aux xs (cons x acc)
  end.

Definition fast_rev (A: Set) (l: list A) : list A :=
  fast_rev_aux l nil.

add an element to the end of a list

Fixpoint snoc (A: Set) (l: list A) (x: A) : list A :=
  match l with
  | nil => cons x nil
  | cons y ys => cons y (snoc ys x)
  end.

Theorem snoc_app_singleton:
  forall A (l: list A) (x: A),
  snoc l x = app l (cons x nil).
Proof.

TODO

Admitted.

Theorem app_snoc_l:
forall A (l1: list A) (l2: list A) (x: A),
app (snoc l1 x) l2 = app l1 (cons x l2).
Proof.

TODO

Admitted.

Theorem app_snoc_r:
forall A (l1: list A) (l2: list A) (x: A),
app l1 (snoc l2 x) = snoc (app l1 l2) x.
Proof.

TODO

Admitted.

simple but inefficient way to reverse a list

Fixpoint rev_snoc (A: Set) (l: list A) : list A :=
  match l with
  | nil => nil
  | cons x xs => snoc (rev_snoc xs) x
  end.

Lemma fast_rev_ok_snoc:
  forall A (l: list A),
  fast_rev l = rev_snoc l.
Proof.

TODO -- you will need to define a helper lemma very similar to how we proved fast_ref_ok

Admitted.

useful in proving rev_length below

Lemma plus_1_S:
  forall n,
  plus n 1 = S n.
Proof.
  intros.
  induction n.
  + simpl. reflexivity.
  + simpl. rewrite IHn. reflexivity.
Qed.

Lemma rev_length:
  forall A (l: list A),
  length (rev l) = length l.
Proof.

TODO -- you will need to define a helper lemma that relates length and app

Admitted.

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

TODO -- you will need to define a helper lemma that relates rev and app, its proof should use app_assoc

Admitted.

This page has been generated by coqdoc