Require Import ssreflect ssrnat ssrbool. Require Import List. Inductive permut_step (a b:list nat) : Prop := C_permut_step : forall l x m y n, a = (l++x::m++y::n )/\ b = (l++y::m++x::n) -> permut_step a b. Lemma D_permut_step : forall l x m y n, permut_step (l++x::m++y::n ) (l++y::m++x::n). Proof. move=>*; eapply C_permut_step; split; reflexivity. Qed. Hint Resolve D_permut_step. Inductive permut (l:list nat) : list nat -> Prop := | permut_refl : permut l l | permut_st : forall m n, permut l m -> permut_step m n -> permut l n. Lemma step_permut : forall a b, permut_step a b -> permut a b. Proof. move => a b ab; apply permut_st with a; last done. apply permut_refl. Qed. Hint Resolve permut_refl permut_st step_permut. Lemma permut_trans : forall a b c, permut a b -> permut b c -> permut a c. Proof. move => a b c ab; elim; first done. by move => {c} c d _ ac cd; eauto. Qed. Lemma step_sym : forall a b, permut_step a b -> permut_step b a. Proof. move => a b [l x m y n [-> ->]] //=. Qed. Lemma permut_sym : forall a b, permut a b -> permut b a. Proof. move => a b; elim => [//=| {b} b c ab ba bc]. apply permut_trans with b; last done. by apply step_permut; apply step_sym. Qed. Lemma permut_step_hd : forall a l1 l2, permut_step l1 l2 -> permut_step (a::l1) (a::l2). Proof. move => a l1 l2 [l x m y n [-> ->] ]. rewrite app_comm_cons (app_comm_cons _ _ a). apply D_permut_step. Qed. Lemma permut_hd : forall a l1 l2, permut l1 l2 -> permut (a::l1) (a::l2). move => a l1 l2; elim => [//=|m n l1m ap mn]. by apply permut_st with (a::m) => //=; apply permut_step_hd. Qed. Lemma permut_swap1 : forall a b l1, permut (a::b::l1) (b::a::l1). Proof. move => a b l1. apply step_permut. apply D_permut_step with (l:=nil)(m:=nil). Qed. Lemma permut_swap : forall a b l1 l2, permut (a::b::l1) l2 -> permut (b::a::l1) l2. Proof. move => a b l1 l2 p. apply permut_trans with (a::b::l1); last done. apply permut_swap1. Qed. Lemma permut_middle : forall x l1 l2, permut (x::l1++l2)(l1++x::l2). Proof. move => x; elim => /= [//=|y l1 Hl1] l2. apply permut_swap. by apply permut_hd. Qed. Lemma permut_middle' : forall x l1 l2 l3, permut (x::l1++l2) l3 -> permut (l1++x::l2) l3. Proof. move => x l1 l2 l3 p; eapply permut_trans. apply permut_sym, permut_middle. done. Qed. Lemma permut_switch : forall x1 l1 x2 l2 l3, permut (x1 :: l1 ++ x2 :: l2) l3 -> permut (x2 :: l1 ++ x1 :: l2) l3. Proof. move => x1 l1 x2 l2 l3 p. apply permut_trans with (l1++x1::x2::l2). by move: (permut_middle x2 (l1++x1::nil) l2); rewrite -!app_assoc. by apply permut_middle'. Qed. Lemma permut_app : forall l1 l2, permut (l1++l2) (l2++l1). Proof. elim => /= [|x1 l1 Hl1] l2; first by rewrite app_nil_r. apply permut_trans with ((x1 :: l2) ++ l1); first by apply permut_hd. apply permut_middle. Qed. Lemma permut_app_r : forall l1 l2 l, permut l1 l2 -> permut (l++l1) (l++l2). Proof. move => l1 l2; elim => [//=|x l Hl] p; apply permut_hd; auto. Qed. Hint Resolve permut_hd permut_middle permut_app permut_app_r permut_swap. Lemma permut_app_l : forall l1 l2 l, permut l1 l2 -> permut (l1++l) (l2++l). Proof. move => l1 l2; elim => [|x l Hl] p12; first by rewrite !app_nil_r. apply permut_trans with (x::l1++l); first by apply permut_sym, permut_middle. apply permut_sym, permut_trans with (x::l2++l). by apply permut_sym, permut_middle. apply permut_hd, permut_sym; auto. Qed. Hint Resolve permut_app_l. Definition ord1 n l := match l with | nil => true | m::_ => n<=m end. Fixpoint sorted (l:list nat) := match l with | n::l => ord1 n l /\ sorted l | nil => True end. Fixpoint insert (n:nat)(l:list nat) := match l with | nil => (cons n nil) | m::l' => if n n ; elim => [//=|m l hl] /=. case: (_ < _); first done. by apply permut_swap, permut_hd. Qed. Lemma insert_sorted : forall n l, sorted l -> (sorted (insert n l)) /\(forall m, m<=n -> ord1 m l -> ord1 m (insert n l)). Proof. move => n; elim => /= [//= | m l Hl][ml Sl] /=. move: (Hl Sl)=> [h1 h2]. case nm : (_ < _) => /=; split; try done. - by do 2 (split; auto). - split; auto; apply h2; last done. by rewrite leqNgt; move: nm; case: (_ < _). Qed. Fixpoint sort (l:list nat) := match l with | nil => nil | x::l => insert x (sort l) end. Lemma sort_sorted : forall l, sorted (sort l). Proof. elim => [//= | x l Hl /=]; by apply insert_sorted. Qed. Lemma sort_permut : forall l, permut l (sort l). Proof. elim => [//=| x l Hl] /=. apply permut_trans with (x::(sort l)); first by auto. apply insert_perm. Qed. (* mergesort *) Print insert. Fixpoint merge (l1:list nat): list nat -> list nat := let aux := fix aux (l2:list nat) := match l1,l2 with | nil, _ => l2 | _,nil => l1 | x1::l1', x2::l2' => if x1 (x1::l1) | y::l' => if x1 < y then x1::(merge l1 l) else y::(aux l') end in aux l2 = merge (x1::l1) l2. Proof. by move => l1; elim. Qed. Lemma merge_permut : forall l1 l2, permut (merge l1 l2) (l1++l2). Proof. elim => [//=| x1 l1 Hl1]; elim => [//=|x2 l2 Hl2] //=. by rewrite app_nil_r. rewrite aux. case: (_<_); first by auto. apply permut_trans with (x2 :: x1 :: l1 ++ l2); auto. Qed. Lemma sort_ord : forall a b l, a<=b -> sorted (b::l) -> ord1 a l. Proof. by move => a b [//=| c l] ab /= [h1 h2]; apply leq_trans with b. Qed. Lemma ord1_trans : forall a b l, ord1 a l -> b <= a -> ord1 b l. Proof. by move => a b [//=|x l] al ba; apply leq_trans with a. Qed. Lemma merge_sorted : forall l1 l2, sorted l1 -> sorted l2 -> (sorted (merge l1 l2)) /\(forall x, ord1 x l1 -> ord1 x l2 -> ord1 x (merge l1 l2)). Proof. elim => [|x1 l1 hl1]; elim => [|x2 l2 hl2] //=; rewrite aux. case h : (_<_). - move => [hl11 hl12] h2; move: (hl1 (x2::l2) hl12 h2) => [hr1 hr2]. by do 2 (split; last done); apply hr2 => //=; apply ltnW. - move => h1 [h21 h22]; move: (hl2 h1 h22) => [hr1 hr2]. do 2 (split; last done); apply hr2; last done. by rewrite /= leqNgt; move: h; case: (_ < _). Qed. Hint Resolve merge_sorted. Fixpoint step_merge (l:list (list nat)) := match l with | x::y::l => (merge x y)::(step_merge l) | l => l end. Definition stack := list (option (list nat)). Fixpoint add (l:list nat)(L:stack) := match L with | nil => (Some l)::nil | (Some l1)::L => None::(add (merge l l1) L) | None::L => (Some l)::L end. Fixpoint to_stack (l:list nat) := match l with | nil => nil | x::l => add (x::nil)(to_stack l) end. Eval compute in (to_stack (2::3::1::5::6::4::7::nil)). Fixpoint flat (L:stack) := match L with | nil => nil | None::L => flat L | Some l :: L => merge l (flat L) end. Definition merge_sort l := (flat (to_stack l)). Lemma merge_nil : forall l, merge l nil = l. Proof. by case. Qed. Hint Resolve merge_permut. Lemma add_permut : forall L l, permut (flat (add l L))(l++(flat L)). Proof. elim => [|[l1|]L HL] l//=. apply permut_trans with ((merge l l1)++(flat L)); first done. apply permut_trans with (l++l1++(flat L)). by rewrite !app_assoc; auto. apply permut_sym; auto. Qed. Lemma merge_sort_permut : forall l, permut l (merge_sort l). Proof. elim => [//=|x l Hl]/=. rewrite /merge_sort /=. apply permut_trans with ((x::nil)++(merge_sort l)). by apply permut_hd. apply permut_sym, add_permut. Qed. Fixpoint l_sorted (L:stack) := match L with | nil => True | None :: L => l_sorted L | Some l::L => (sorted l) /\ l_sorted L end. Hint Resolve merge_sorted. Lemma add_sorted : forall L l, sorted l -> l_sorted L -> l_sorted (add l L). Proof. elim => [//=|[l1|//=] L HL] l sl [sl1 sL] //=. apply HL; auto. by apply merge_sorted. Qed. Lemma flat_sorted : forall L, l_sorted L -> sorted (flat L). Proof. elim => [//=|[l1|//=] L HL] [*]//=. by apply merge_sorted; auto. Qed. Lemma stack_sorted : forall l, l_sorted (to_stack l). Proof. by elim => [//|x l] ; apply add_sorted. Qed. Lemma merge_sorte_sorted : forall l, sorted (merge_sort l). Proof. move => l; apply flat_sorted, stack_sorted. Qed.