(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch L13 (lists) The material in this file contains coq proofs which can be read and animated with coqide or xemacs+proofgeneral. **) Section l13. Set Implicit Arguments. Require Import Coq.Lists.List. Check (nil : list nat). Definition l23 : list nat := 2 :: 3 :: nil. Definition l123 : list nat := 1 :: l23. Eval compute in l123. Eval compute in 1 :: l123. Definition ll1 : list (list nat) := l23 :: l123 :: nil. Eval compute in ll1. Eval compute in nil :: ll1. Definition hd (ns : list nat) : nat := match ns with | nil => 0 | n :: ns' => n end. Eval compute in hd l123. Definition hd' (A : Set)(bs : list A) : unit + A := match bs with | nil => inl A tt | a :: as' => inr unit a end. Eval compute in hd' l123. Eval compute in hd' (nil : list nat). Eval compute in hd' ll1. Fixpoint length (A:Set)(l:list A){struct l} : nat := match l with | nil => 0 | a :: m => S (length m) end. Eval compute in (length l123). Eval compute in (length ll1). Fixpoint app (A : Set)(l m:list A) {struct l} : list A := match l with | nil => m | cons a l' => cons a (app l' m) end. (* ++ = app, defined in the library. *) Eval compute in (l123 ++ l23). Eval compute in (l23 ++ l123). Lemma nilApp : forall (A:Set)(l:list A), nil ++ l = l. intros. simpl. reflexivity. Qed. Lemma appNil : forall (A:Set)(l:list A), l ++ nil = l. intros. induction l. simpl. reflexivity. simpl. rewrite IHl. reflexivity. Qed. Lemma assocApp : forall (A:Set)(l1 l2 l3:list A), (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3). induction l1. simpl. intros. reflexivity. intros. simpl. rewrite IHl1. reflexivity. Qed. Fixpoint snoc (A:Set) (l : list A)(a : A) {struct l} : list A := match l with | nil => a :: nil | b :: m => b :: (snoc m a) end. Eval compute in (snoc l123 4). Fixpoint rev (A:Set)(l : list A) {struct l} : list A := match l with | nil => nil | a :: m => snoc (rev m) a end. Eval compute in rev l123. Eval compute in rev (rev l123). Lemma revsnoc : forall (A:Set)(l:list A)(a:A), rev (snoc l a) = a :: (rev l). intros. induction l. simpl. reflexivity. simpl. rewrite IHl. simpl. reflexivity. Qed. Lemma revrev : forall (A:Set)(l:list A),rev (rev l) = l. intros. induction l. simpl. reflexivity. simpl. rewrite revsnoc. rewrite IHl. reflexivity. Qed.