Lemma FirstLemma (A B C : Prop): (A -> B) -> (B -> C) -> (A -> C). Proof. intros. apply H0. apply H. trivial. Defined. Definition FirstDefinition (A B C : Prop): (A -> B) -> (B -> C) -> (A -> C) := fun f g x => g (f x). Eval unfold FirstLemma in (FirstLemma). Goal forall (A B C : Prop), (A -> B) -> (B -> C) -> (A -> C). (* apply FirstLemma. *) apply FirstDefinition. Qed. (* Lists, Map and Concat *) Inductive list (A : Type) : Type := | Nil : list A | Cons : A -> list A -> list A. Notation " [ ] " := (Nil _) (format "[ ]"). Infix "::" := (Cons _) (at level 60, right associativity). Fixpoint map {A B : Type} (f : A -> B) (l : list A) : list B := match l with | [] => [] | a :: t => (f a) :: (map f t) end. Definition concat (A : Type) : list A -> list A -> list A := fix concat l1 l2 := match l1 with | [] => l2 | a :: l1' => a :: concat l1' l2 end. Infix "++" := (concat _) (right associativity, at level 60) . Lemma MapConcat (A B : Type) : forall (f : A -> B) (l1 l2 : list A), map f (l1 ++ l2) = map f l1 ++ map f l2. Proof. intros. induction l1. simpl. trivial. simpl. rewrite IHl1. trivial. Qed. (* Insertion into a sorted list *) Require Import PeanoNat. Import Nat. Require Import Bool. Fixpoint insert (n : nat) (l : list nat) : list nat := match l with | [] => n::[] | m :: l' => if n <=? m then n::m::l' else m::insert n l' end. Inductive Sorted : list nat -> Prop := | EmptySorted : Sorted [] | SingletonSorted : forall (n : nat), Sorted (n::[]) | RecSorted : forall (m n : nat) (l : list nat), Sorted (m::l) -> n <= m -> Sorted (n::m::l). Lemma InsertSort: forall (n : nat) (l : list nat), Sorted l -> Sorted (insert n l). Proof. intros. elim H; intros; simpl. apply SingletonSorted. case_eq (n <=? n0); intros. rewrite leb_le in H0. apply (RecSorted _ _ _ (SingletonSorted n0) H0). rewrite leb_gt in H0. apply (@or_introl _ (n0=n)) in H0; rewrite <- lt_eq_cases in H0. apply (RecSorted _ _ _ (SingletonSorted n) H0). case_eq (n <=? n0); intros; simpl. rewrite leb_le in H3. apply (RecSorted _ _ _ (RecSorted _ _ _ H0 H2) H3). case_eq (n <=? m); intros; simpl. rewrite leb_gt in H3. apply (@or_introl _ (n0=n)) in H3; rewrite <- lt_eq_cases in H3. rewrite leb_le in H4. apply (RecSorted _ _ _ (RecSorted _ _ _ H0 H4) H3). simpl in H1. rewrite H4 in H1. apply (RecSorted _ _ _ H1 H2). Qed. (* Induction on l leads nowhere Lemma InsertSort: forall (n : nat) (l : list nat), Sorted l -> Sorted (insert n l). Proof. intros. induction l. simpl. apply SingletonSorted. simpl. case_eq (n <=? a); intros. rewrite leb_le in H0. apply (RecSorted _ _ _ H H0). *) Fixpoint insertSort (l : list nat) : list nat := match l with | [] => [] | n :: l' => insert n (insertSort l') end. Lemma insertSortCorrect : forall (l : list nat), Sorted (insertSort l). Proof. intros. induction l; simpl. apply EmptySorted. apply (InsertSort _ _ IHl). Qed.