Require Import List. Import ListNotations. Require Import PeanoNat. Import Nat. Require Import Arith.Compare_dec. Require Import Coq.Init.Wf. (* Order Class of decidable totally ordered types *) Class OrderSig (A : Type) := { le : A -> A -> Prop }. Infix "<~" := (le) (at level 50). Class Order (A : Type) := { sig :> OrderSig A; dec : forall (x y : A), {x <~ y} + {~(x <~ y)}; refl : forall (x : A), x <~ x; trans : forall (x y z : A), x <~ y -> y <~ z -> x <~ z; anti_sym : forall (x y : A), x <~ y -> y <~ x -> x = y; total : forall(x y : A), x <~ y \/ y <~ x }. Definition leeb `{O : Order} : A -> A -> bool := fun x y => if dec x y then true else false. Infix "<~?" := (leeb) (at level 50). (* Nat as instance of Order *) Instance ONatSig : OrderSig nat := {| le := Nat.le |}. Instance ONat : Order nat := {| sig := ONatSig; |}. Proof. apply le_dec. apply le_refl. apply le_trans. apply le_antisymm. apply le_ge_cases. Defined. Section mergeSort. Context `{O : Order}. Fixpoint insert (x : A) (ls : list A) : list A := match ls with | [] => [x] | y::ls' => if x <~? y then x::y::ls' else y::insert x ls' end. Fixpoint merge (ls1 ls2 : list A) : list A := match ls1 with | [] => ls2 | y::ls1' => insert y (merge ls1' ls2) end. Fixpoint split (ls : list A) : list A * list A := match ls with | [] => ([],[]) | [x] => ([x],[]) | x::y::ls' => (x::fst (split ls'),y::snd (split ls')) end. Definition lengthOrder (ls1 ls2 : list A) : Prop := length ls1 < length ls2. Lemma lengthOrder_wf' : forall (len : nat) (ls : list A), length ls <= len -> Acc lengthOrder ls. Proof. assert (BC : Acc lengthOrder []). apply Acc_intro; intros ls' H. unfold lengthOrder in H; simpl in H. apply nlt_0_r in H. contradiction. induction len; intros. apply le_0_r in H. rewrite length_zero_iff_nil in H. rewrite H; trivial. destruct ls; trivial. simpl in H. apply le_S_n in H. apply Acc_intro; intros ls' H0. apply IHlen. unfold lengthOrder in H0; simpl in H0. rewrite lt_succ_r in H0. rewrite H0; trivial. Defined. Theorem lengthOrder_wf : well_founded lengthOrder. Proof. unfold well_founded. intros ls. apply (lengthOrder_wf' (length ls)). trivial. Defined. Lemma split_length_decreasing : forall (len : nat) (ls : list A), length ls <= len -> length (fst (split ls)) <= length ls /\ length (snd (split ls)) <= length ls. Proof. induction len; intros. rewrite le_0_r in H. rewrite length_zero_iff_nil in H. rewrite H. simpl. split; trivial. destruct ls. simpl. split; trivial. destruct ls. simpl. split; intuition. simpl. rewrite <- ?succ_le_mono. simpl in H. rewrite <- ?succ_le_mono in H. rewrite <- le_succ_diag_r in H. apply IHlen in H. rewrite <- le_succ_diag_r. trivial. Defined. Lemma split_length_strictly_decreasing : forall (len : nat) (ls : list A), 2 <= length ls <= len -> lengthOrder (fst (split ls)) ls /\ lengthOrder (snd (split ls)) ls. Proof. intros. destruct len. destruct H. apply (le_trans _ _ _ H) in H0. apply (nle_succ_0 1) in H0; contradiction. unfold lengthOrder. destruct ls. destruct H; simpl in H. apply (nle_succ_0 1) in H; contradiction. simpl in H. destruct ls. destruct H; simpl in H. apply le_S_n in H. apply (nle_succ_0 0) in H; contradiction. simpl in *. rewrite <- ?succ_lt_mono. rewrite ?lt_succ_r. apply (split_length_decreasing len). destruct H. rewrite <- ?succ_le_mono in H0. rewrite <- H0. apply le_succ_diag_r. Defined. Lemma split_wf1 : forall ls, 2 <= length ls -> lengthOrder (fst (split ls)) ls. Proof. intros. assert (H0 := split_length_strictly_decreasing (length ls) ls (conj H (le_refl (length ls)))). destruct (split ls). intuition. Defined. Lemma split_wf2 : forall ls, 2 <= length ls -> lengthOrder (snd (split ls)) ls. Proof. intros. assert (H0 := split_length_strictly_decreasing (length ls) ls (conj H (le_refl (length ls)))). destruct (split ls). intuition. Defined. Definition mergeSort : list A -> list A := Fix lengthOrder_wf (fun _ => list A) (fun (ls : list A) (mergeSort : forall ls' : list A, lengthOrder ls' ls -> list A) => match le_lt_dec 2 (length ls) with | left le_true => let lss := split ls in merge (mergeSort (fst lss) (split_wf1 _ le_true)) (mergeSort (snd lss) (split_wf2 _ le_true)) | _ => ls end). Require Import Program.Wf. Program Fixpoint mergeSort2 (ls : list A) {wf lengthOrder ls} : list A := if le_lt_dec 2 (length ls) then merge (mergeSort2 (fst (split ls))) (mergeSort2 (snd (split ls))) else ls. Next Obligation. apply (split_wf1 _ H). Qed. Next Obligation. apply (split_wf2 _ H). Qed. Next Obligation. apply lengthOrder_wf. Defined. Inductive Sorted : list A -> Prop := | EmptySorted : Sorted [] | SingletonSorted : forall (x : A), Sorted [x] | RecSorted : forall (x y : A) (l : list A), Sorted (y::l) -> x <~ y -> Sorted (x::y::l). Lemma leeb_true_leeq : forall (x y : A), x <~? y = true <-> x <~ y. Proof. split; intros. unfold leeb in H. case_eq (dec x y); intros. trivial. rewrite H0 in H; discriminate. unfold leeb. case_eq (dec x y); intros. trivial. contradiction. Qed. Lemma leeb_false_nleeq : forall (x y : A), x <~? y = false <-> ~ (x <~ y). Proof. split; intros. unfold leeb in H. case_eq (dec x y); intros. rewrite H0 in H; discriminate. trivial. unfold leeb. case_eq (dec x y); intros. contradiction. trivial. Qed. Lemma nleeq_geeq : forall (x y : A), ~ (x <~ y) -> (y <~ x). Proof. intros. destruct (total y x). trivial. contradiction. Qed. Lemma insert_sorted : forall (x : A) (l : list A), Sorted l -> Sorted (insert x l). Proof. intros. elim H; simpl. apply SingletonSorted. intros. case_eq (x <~? x0); intros. apply RecSorted. apply SingletonSorted. rewrite leeb_true_leeq in H0; trivial. apply RecSorted. apply SingletonSorted. rewrite leeb_false_nleeq in H0. apply nleeq_geeq. trivial. intros. case_eq (x <~? x0); intros. apply leeb_true_leeq in H3. apply RecSorted; [ apply RecSorted | idtac ]; trivial. case_eq (x <~? y); intros. apply leeb_false_nleeq in H3. apply leeb_true_leeq in H4. apply RecSorted; [ apply RecSorted | apply nleeq_geeq ]; trivial. rewrite H4 in H1. apply RecSorted; trivial. Qed. Lemma insert_elements : forall (x a : A) (l : list A), a = x \/ In x l <-> In x (insert a l). Proof. intros x a. induction l; simpl. intuition. case (a <~? a0); simpl. intuition. rewrite or_comm, or_assoc. apply or_iff_compat_l. rewrite or_comm. apply IHl. Qed. Lemma merge_sorted : forall (l1 l2 : list A), Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2). Proof. intros. elim H; simpl. trivial. intros. apply insert_sorted; trivial. intros. apply insert_sorted; trivial. Qed. Lemma merge_elements : forall (x : A) (l1 l2 : list A), In x l1 \/ In x l2 <-> In x (merge l1 l2). Proof. intros. induction l1; simpl. intuition. rewrite <- insert_elements. rewrite or_assoc. apply or_iff_compat_l. apply IHl1. Qed. Lemma split_elements' : forall (len : nat) (x : A) (l : list A), length l <= len -> (In x l <-> In x (fst (split l)) \/ In x (snd (split l))). Proof. induction len; intros. rewrite le_0_r in H. rewrite length_zero_iff_nil in H. rewrite H; simpl; intuition. destruct l. simpl; intuition. simpl in H. apply succ_le_mono in H. destruct l. simpl; intuition. simpl in H. rewrite <- le_succ_diag_r in H. simpl. rewrite <- or_assoc. rewrite (or_assoc _ (In x (fst (split l)))), <- (or_assoc _ (a0=x)), (or_comm (In x (fst (split l)))), (or_assoc (a0=x)), <- or_assoc. apply or_iff_compat_l. apply IHlen; trivial. Qed. Lemma split_elements : forall (x : A) (l : list A), In x l <-> In x (fst (split l)) \/ In x (snd (split l)). Proof. intros. apply (split_elements' (length l)); trivial. Qed. Ltac unfoldRec f x := unfold f; WfExtensionality.unfold_sub f x; repeat (fold_sub f). Lemma mergeSort_sorted : forall (l : list A), Sorted (mergeSort2 l). Proof. apply (well_founded_ind lengthOrder_wf). intros l IH. unfoldRec mergeSort2 l. case (le_lt_dec 2 (length l)); intros. apply merge_sorted. apply IH. apply split_wf1; trivial. apply IH. apply split_wf2; trivial. destruct l. apply EmptySorted. destruct l. apply SingletonSorted. simpl in l0. rewrite <- ?succ_lt_mono in l0. apply nlt_0_r in l0; contradiction. Qed. Lemma mergeSort_elements : forall (x : A) (l : list A), In x l <-> In x (mergeSort2 l). Proof. intro x. apply (well_founded_ind lengthOrder_wf). intros l IH. unfoldRec mergeSort2 l. case (le_lt_dec 2 (length l)); intros. rewrite <- merge_elements. rewrite <- (IH (fst (split l))). rewrite <- (IH (snd (split l))). apply split_elements. apply split_wf2; trivial. apply split_wf1; trivial. intuition. Qed. End mergeSort. Eval compute in mergeSort2 [1;5;2;4;3]. (* Strings with lexicographical order as instance or Order *) Section LexOrder. Require Import Ascii. Require Import String. Open Scope string. Inductive lexOrder : string -> string -> Prop := | lexEmpty : forall (s : string), lexOrder "" s | lexHead : forall (a b : ascii) (s s' : string), nat_of_ascii a < nat_of_ascii b -> lexOrder (String a s) (String b s') | lexTail : forall (a : ascii) (s s' : string), lexOrder s s' -> lexOrder (String a s) (String a s'). Lemma lexOrder_dec : forall (s1 s2 : string), {lexOrder s1 s2} + {~ lexOrder s1 s2}. Proof. induction s1; intros. left; apply lexEmpty; trivial. destruct s2 as [ | b s2]. right. intro. inversion H. specialize IHs1 with s2. destruct IHs1 as [H | H]. case_eq (nat_of_ascii a <=? nat_of_ascii b); intros. apply leb_le in H0. apply lt_eq_cases in H0. left. destruct H0. apply (lexHead _ _ _ _ H0). apply (f_equal ascii_of_nat) in H0. rewrite ?ascii_nat_embedding in H0. rewrite H0. apply (lexTail _ _ _ H). apply leb_nle in H0. right. contradict H0. inversion H0. apply (lt_le_incl _ _ H2). reflexivity. case_eq (nat_of_ascii a