(*****************************************************************************) (* introduction to Coq *) (*****************************************************************************) (*************) (* datatypes *) (*************) Inductive bool : Set := true : bool | false : bool. Check bool. Check true. Check bool_ind. Print bool_rect. Inductive nat : Set := O : nat | S : nat -> nat. Check nat. Check O. Check (S O). Check nat_ind. Print nat_rect. (*************) (* functions *) (*************) (* recursive functions *) Fixpoint plus (n m:nat) {struct n} : nat := match n with O => m | S n' => S (plus n' m) end. Eval compute in plus (S O) (S (S O)). (* definitions *) Definition double (n:nat) : nat := plus n n. Eval compute in double (S (S O)). (**************) (* predicates *) (**************) (* pencil-and-paper definition of the relation "<=": n <= m -------- [le_n] ---------- [le_S ] n <= n n <= S m *) Inductive le (n : nat) : nat -> Prop := le_n : le n n | le_S : forall m : nat, le n m -> le n (S m). Check le. Check (le O (S O)). Check (le (S O) O). Check le_n. Check (le_n O). Check (le_S O O (le_n O)). Reset Initial. Check le. Check (0 <= 1). (**********) (* proofs *) (**********) Lemma min0 : 0 <= 1. (*exact (le_S O O (le_n O)).*) apply le_S. apply le_n. Show Proof. Qed. Lemma min : forall n:nat, 0 <= n. induction n. (* base case *) apply le_n. (* inductive case *) apply le_S. auto. Show Proof. Qed. (*********************************************************************************) (*****************************************************************************) (* verification of the sorting algorithm *) (*****************************************************************************) Require Import Arith. Require Import Omega. Require Import List. Section GenericSort. Variable A : Set. Variable A_dec : forall (a b:A), { a = b } + { a <> b }. Variable R : A -> A -> Prop. Variable R_dec : forall (a b:A), { R a b } + { ~ R a b }. Variable R_total : forall a b, R a b \/ R b a. Fixpoint insert (a:A) (l:list A) {struct l} : list A := match l with nil => a::nil | b::l' => if R_dec a b then a::b::l' else b::(insert a l') end. Fixpoint sort (l:list A) : list A := match l with nil => nil | a::l' => insert a (sort l') end. (* End GenericSort. Check sort. Check (sort nat le). Lemma le_nat_dec : forall m n, { m <= n } + { ~(m <= n) }. intros. generalize (le_gt_dec m n). intros. inversion_clear H. auto. right. omega. Defined. Check (sort nat le le_nat_dec). Eval simpl in (sort nat le le_nat_dec (5::7::3::5::3::0::6::1::nil)). Recursive Extraction le_nat_dec sort. *) (* we want to check that "sort" returns: - a sorted list - with the same elements *) Inductive Sorted : list A -> Prop := sorted_nil : Sorted nil | sorted_one : forall a, Sorted (a::nil) | sorted_cons : forall a b l, R a b -> Sorted (b::l) -> Sorted (a::b::l). Theorem Sorted_sort : forall l, Sorted (sort l). induction l. simpl. apply sorted_nil. simpl. Lemma Sorted_insert : forall l a, Sorted l -> Sorted (insert a l). induction l. simpl. intros. constructor. simpl. intros. case (R_dec a0 a). intros. constructor. auto. auto. intro. Lemma Sorted_insert' : forall l a b, ~ R b a -> Sorted (a::l) -> Sorted (a::(insert b l)). induction l. simpl. intros. constructor. generalize (R_total a b). tauto. constructor. simpl. intros. case (R_dec b a). intro. constructor. generalize (R_total a0 b). tauto. constructor. auto. inversion_clear H0. auto. intros. constructor. inversion_clear H0. auto. apply IHl. auto. inversion_clear H0. auto. Qed. apply Sorted_insert'. auto. auto. Qed. apply Sorted_insert. auto. Qed. Fixpoint multiplicity (lst:list A) (a:A) {struct lst} : nat := match lst with nil => O | hd::tl => match A_dec hd a with left _ => 1 + multiplicity tl a | _ => multiplicity tl a end end. Theorem no_more_no_less : forall (lst:list A) a, multiplicity lst a = multiplicity (sort lst) a. induction lst; simpl; intros; auto. case (A_dec a a0). intros. subst a0. rewrite IHlst. Lemma multiplicity_insert : forall (lst:list A) a, multiplicity (insert a lst) a = 1 + multiplicity lst a. induction lst; simpl; intros; auto. case (A_dec a a). auto. tauto. case (R_dec a0 a); intro. simpl. case (A_dec a0 a0). auto. tauto. simpl. case (A_dec a a0). intros. subst a0. rewrite IHlst. auto. intro. rewrite IHlst. auto. Qed. rewrite multiplicity_insert. auto. intro. Lemma multiplicity_insert' : forall (lst:list A) a b, a <> b -> multiplicity (insert a lst) b = multiplicity lst b. induction lst; simpl; intros; auto. case (A_dec a b). tauto. auto. case (R_dec a0 a); intro. simpl. case (A_dec a0 b). tauto. auto. simpl. case (A_dec a b). intros. subst b. rewrite IHlst. auto. auto. intro. rewrite IHlst. auto. auto. Qed. rewrite multiplicity_insert'. rewrite IHlst. auto. auto. Qed. End GenericSort.