autoperm.v

Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Perm.

Variable (A : eqType) (le : A -> A -> bool).

Definition condrev (r : bool) (xs : seq A) :=
  if r then rev xs else xs.

Lemma perm_catrev (xs ys : seq A) : perm_eq (catrev xs ys) (xs ++ ys).
Proof.
by elim: xs ys => //= x xs IH ys; apply (perm_eq_trans (IH _));
  rewrite -cat_rcons -cat_cons perm_cat2r perm_rcons.
Qed.

Lemma perm_rev (xs : seq A) : perm_eq (rev xs) xs.
Proof. by rewrite -{2}(cats0 xs) perm_catrev. Qed.

Lemma perm_condrev (r : bool) (xs : seq A) : perm_eq (condrev r xs) xs.
Proof. by case: r => //=; apply perm_rev. Qed.

Lemma count_flatten (xss : seq (seq A)) x:
  count x (flatten xss) = \sum_(xs <- xss) (count x xs).
Proof.
elim: xss => //= [| xs xss IH]; first by rewrite big_nil.
by rewrite count_cat big_cons IH.
Qed.

Lemma perm_flatten (xs ys : seq (seq A)) :
  perm_eq xs ys -> perm_eq (flatten xs) (flatten ys).
Proof.
by move => H; apply/perm_eqP => x; rewrite !count_flatten; apply eq_big_perm.
Qed.

Fixpoint perm_common (xs : seq A) : seq A -> seq A :=
  if xs isn't x :: xs
  then fun _ => [::]
  else fix perm_common' (ys : seq A) :=
    if ys isn't y :: ys
    then [::]
    else if x == y
         then x :: perm_common xs ys
         else if le x y
              then perm_common xs (y :: ys)
              else perm_common' ys.

Fixpoint perm_elim (xs : seq A) : seq A -> seq A * seq A :=
  if xs isn't x :: xs
  then fun ys => ([::], ys)
  else fix perm_elim' (ys : seq A) :=
    if ys isn't y :: ys
    then (x :: xs, [::])
    else if x == y
         then perm_elim xs ys
         else if le x y
              then let (xs', ys') := perm_elim xs (y :: ys) in
                   (x :: xs', ys')
              else let (xs', ys') := perm_elim' ys in (xs', y :: ys').

Lemma perm_elim_perm (xs ys : seq A) :
  let (xs', ys') := perm_elim xs ys in
  perm_eq xs (perm_common xs ys ++ xs') /\
  perm_eq ys (perm_common xs ys ++ ys').
Proof.
elim: xs ys => //= x xs IHx; elim => // y ys IHy.
case: eqP => [-> | _]; first by
  case: {IHx IHy} (perm_elim xs ys) (IHx ys) => /= xs' ys'; rewrite !perm_cons.
case: ifP => _; first by
  case: (perm_elim xs (y :: ys)) (IHx (y :: ys)) => /= xs' ys' [H ->];
    split => //; move/perm_eqlP/perm_eqrP:
      (perm_catC (perm_common xs (y :: ys)) (x :: xs')) => -> /=;
    rewrite perm_cons; move/perm_eqlP: H => ->; apply/perm_eqlP/perm_catC.
case: (_ ys) {IHx} IHy => xs' ys' [->].
set c := (fix perm_common' (ys : seq A) : seq A := _).
move => H; split => //.
move/perm_eqlP/perm_eqrP: (perm_catC (c ys) (y :: ys')) => -> /=.
by rewrite perm_cons; move/perm_eqlP: H => ->; apply/perm_eqlP/perm_catC.
Qed.

End Perm.

Section PermSyntax.

Variable (A : Type).

Inductive Seq : Type :=
  | SeqEmbed  of seq A
  | SeqNil
  | SeqCons   of A & Seq
  | SeqRcons  of Seq & A
  | SeqCat    of Seq & Seq
  | SeqCatrev of Seq & Seq
  | SeqRev    of Seq.

Fixpoint denote_Seq (xs : Seq) : seq A :=
  match xs with
    | SeqEmbed xs => xs
    | SeqNil => [::]
    | SeqCons x xs => x :: denote_Seq xs
    | SeqRcons xs x => rcons (denote_Seq xs) x
    | SeqCat xs ys => denote_Seq xs ++ denote_Seq ys
    | SeqCatrev xs ys => catrev (denote_Seq xs) (denote_Seq ys)
    | SeqRev xs => rev (denote_Seq xs)
  end.

Fixpoint norm_Seq (r : bool) (xs : Seq) (acc : seq (bool * seq A)) :
  seq (bool * seq A) :=
  match xs with
    | SeqEmbed xs => (r, xs) :: acc
    | SeqNil => acc
    | SeqCons x xs =>
      if r
        then norm_Seq true xs ((false, [:: x]) :: acc)
        else (false, [:: x]) :: norm_Seq false xs acc
    | SeqRcons xs x =>
      if r
        then (false, [:: x]) :: norm_Seq true xs acc
        else norm_Seq false xs ((false, [:: x]) :: acc)
    | SeqCat xs ys =>
      if r
        then norm_Seq true ys (norm_Seq true xs acc)
        else norm_Seq false xs (norm_Seq false ys acc)
    | SeqCatrev xs ys =>
      if r
        then norm_Seq true ys (norm_Seq false xs acc)
        else norm_Seq true xs (norm_Seq false ys acc)
    | SeqRev xs => norm_Seq (~~ r) xs acc
  end.

End PermSyntax.

Section PermReflection.

Variable (A : eqType).

Lemma norm_SeqE (r : bool) (xs : Seq A) (acc : seq (bool * seq A)) :
  flatten [seq condrev e.1 e.2 | e <- norm_Seq r xs acc] =
  condrev r (denote_Seq xs) ++ flatten [seq condrev e.1 e.2 | e <- acc].
Proof.
by elim: xs r acc =>
  [xs || x xs IH | xs IH x | xs IHl ys IHr | xs IHl ys IHr | xs IH] [] acc //=;
  (rewrite IH || rewrite ?(IHl, IHr));
  rewrite ?(catrevE, rev_cons, rev_rcons, rev_cat, revK, cat_rcons, catA) //=.
Qed.

Lemma norm_Seq_perm (xs : Seq A) :
  perm_eq (denote_Seq xs) (flatten (map snd (norm_Seq false xs [::]))).
Proof.
rewrite -(cats0 (denote_Seq xs)) -/(condrev false (denote_Seq xs))
        (_ : [::] = flatten [seq condrev e.1 e.2 | e <- [::]]) // -norm_SeqE.
by elim: (norm_Seq _ _ _) => //= {xs} -[r xs] ys /=; rewrite -(perm_cat2l xs);
  apply perm_eq_trans; rewrite perm_cat2r perm_condrev.
Qed.

Lemma perm_Seq_flatten (xs ys : Seq A) :
  perm_eq (denote_Seq xs) (denote_Seq ys) =
  perm_eq (flatten (map snd (norm_Seq false xs [::])))
          (flatten (map snd (norm_Seq false ys [::]))).
Proof.
apply/idP; case: ifP;
  last (move/negP => H H0; apply/H => {H}; move: H0); move => H.
- by rewrite (perm_eqlP (norm_Seq_perm _))
             (perm_eqlP H) perm_eq_sym norm_Seq_perm.
- by rewrite -(perm_eqrP (norm_Seq_perm ys))
             -(perm_eqrP H) perm_eq_sym norm_Seq_perm.
Qed.

Lemma perm_fm_sort_elim (f : nat -> seq A) (xs ys : seq nat) :
  perm_eq (flatten (map f xs)) (flatten (map f ys)) =
  let (xs', ys') := perm_elim geq (sort geq xs) (sort geq ys) in
  perm_eq (flatten (map f xs')) (flatten (map f ys')).
Proof.
case: (perm_elim _ _ _) (perm_elim_perm geq (sort geq xs) (sort geq ys))
  => xs' ys' [].
rewrite !perm_sort => /(perm_map f) /perm_flatten /perm_eqlP ->
                       /(perm_map f) /perm_flatten /perm_eqrP ->.
by rewrite !map_cat !flatten_cat perm_cat2l.
Qed.

End PermReflection.

Ltac seqReify xs :=
  match xs with
    | @nil ?A => constr:(SeqNil A)
    | ?x :: ?xs => let xs' := seqReify xs in constr:(SeqCons x xs')
    | rcons ?xs ?x => let xs' := seqReify xs in constr:(SeqRcons xs' x)
    | ?xs ++ ?ys =>
      let xs' := seqReify xs in
      let ys' := seqReify ys in
      constr:(SeqCat xs' ys')
    | catrev ?xs ?ys =>
      let xs' := seqReify xs in
      let ys' := seqReify ys in
      constr:(SeqCatrev xs' ys')
    | rev ?xs => let xs' := seqReify xs in constr:(SeqRev xs')
    | _ => constr:(SeqEmbed xs)
  end.

Ltac autoperm :=
  let rec num_rec f xss :=
    match xss with
      | [::] => idtac
      | ?xs :: ?xss =>
        let f' := fresh "f" in
        rename f into f';
        pose f := (fun n : nat => if n is n'.+1 then f' n' else xs);
        rewrite (_ : xs = f 0) // ?(_ : forall n : nat, f' n = f n.+1) //;
        subst f'; num_rec f xss
      | _ :: ?xss => num_rec f xss
    end
  in
  repeat match goal with [|- context [@perm_eq ?A ?xs ?ys]] =>
    match xs with flatten _ => fail 1 | _ => idtac end;
    let f := fresh "f" in
    let xs' := seqReify xs in
    let ys' := seqReify ys in
    let zs := eval simpl in
      (map snd (norm_Seq false xs' [::] ++ norm_Seq false ys' [::])) in
    rewrite (_ : perm_eq xs ys = perm_eq (denote_Seq xs') (denote_Seq ys'))
            // perm_Seq_flatten ![map snd (norm_Seq false _ [::])]/=;
    pose f := (fun n : nat => [::] : seq A);
    num_rec f zs;
    rewrite -/(map f [::]) -?(map_cons f) !perm_fm_sort_elim
            (lock (@flatten)) /= -(lock (@flatten)) {f}
  end;
  rewrite ![perm_eq (flatten _) (flatten _)]/= ?cats0.

Module PermExamples.

Example ex1 (A : eqType) (x y z : A) (xs ys zs zs' : seq A) :
  perm_eq (xs ++ zs) (zs' ++ xs) ->
  perm_eq (x :: xs ++ y :: ys ++ z :: zs)
          (rev zs' ++ [:: x; y] ++ ys ++ z :: rev xs).
Proof.
Time autoperm.
done.
Qed.

Example ex2 (A : eqType) (xs ys zs xs' ys' zs' : seq A) :
  perm_eq xs xs' -> perm_eq ys ys' -> perm_eq zs zs' ->
  perm_eq (catrev xs ys ++ zs) (xs' ++ rev ys' ++ zs').
Proof.
Time autoperm. (* preserves the order of terms. *)
rewrite -(perm_cat2r (ys ++ zs)) => /perm_eqlP ->.
rewrite perm_cat2l -(perm_cat2r zs) => /perm_eqlP ->.
by rewrite perm_cat2l.
Qed.

Example ex3 (A B : eqType) (f : A -> B) (xs ys xs' : seq A) (zs : seq B) :
  perm_eq (xs ++ xs) (xs' ++ xs) ->
  perm_eq (map f (xs ++ ys) ++ zs) (map f ys ++ zs ++ map f xs').
Proof.
rewrite map_cat.
Time autoperm.
apply perm_map.
Qed.

End PermExamples.

(* Mergesort *)

Lemma total_asym (T : Type) (R : rel T) :
  total R -> forall x y : T, ~~ R x y -> R y x.
Proof. by move => H x y /negPf H0; move: (H x y); rewrite H0. Qed.

Module Mergesort.
Section Mergesort.

Variables (A : eqType) (cmp : A -> A -> bool).

Fixpoint merge xs :=
  match xs with
    | [::] => id
    | x :: xs' =>
      fix merge' ys {struct ys} :=
        if ys is y :: ys'
          then if cmp x y then x :: merge xs' ys else y :: merge' ys'
          else xs
  end.

Fixpoint merge_pair xs :=
  match xs with
    | [::] => [::]
    | [:: x] => [:: x]
    | (x :: x' :: xs) => merge x x' :: merge_pair xs
  end.

Fixpoint list2_rec (A : Type) (P : seq A -> Set)
  (c1 : P [::]) (c2 : forall x, P [:: x])
  (c3 : forall x x' xs, P xs -> P [:: x, x' & xs]) (xs : seq A) : P xs :=
  match xs with
    | [::] => c1
    | [:: x] => c2 x
    | [:: x, x' & xs] => c3 x x' xs (list2_rec c1 c2 c3 xs)
  end.

Lemma merge_pair_leq xs : size (merge_pair xs) <= (size xs).
Proof. by elim/list2_rec: xs => //= _ _ xs /leqW; rewrite ltnS. Qed.

Lemma Acc_ltsize T : well_founded (fun (x y : seq T) => size x < size y).
Proof.
move => xs.
elim: {xs} (size xs) {1 3}xs (leqnn (size xs)) => [[] // |] n IH xs H.
constructor => ys /(fun H0 => leq_trans H0 H) {H}; rewrite ltnS.
apply IH.
Qed.

Definition sort (xs : seq A) : seq A :=
  Fix (@Acc_ltsize (seq A)) (fun _ => seq A)
    (fun xss : seq (seq A) =>
      match xss return (forall yss, size yss < size xss -> seq A) -> seq A with
        | [::] => fun _ => [::]
        | [:: xs] => fun _ => xs
        | (xs :: xs' :: xss') as xss =>
          fun (H : forall yss, size yss <= (size xss').+1 -> seq A) =>
            H (merge_pair xss) (merge_pair_leq xss')
      end)
  (map (fun x => [:: x]) xs).

Lemma sort_sorted (xs : seq A) : total cmp -> sorted cmp (sort xs).
Proof.
rewrite /sort /Fix => Hcmp.
set xss := map _ _.
have H: all (sorted cmp) xss by rewrite {}/xss; elim: xs.
move: (Acc_ltsize _) => Hi.
elim/Acc_ind: xss / Hi (Hi) H => {xs} -[| xs [| xs' xss]] _ IH Hi;
  rewrite -Fix_F_eq //; first by rewrite /= andbT.
move => H; apply IH; first by rewrite !ltnS merge_pair_leq.
elim/list2_rec: {xs xs' xss H Hi IH} [:: _, _ & _] H =>
  //= xs xs' xss IH /and3P [H H0 H1]; rewrite {}IH // andbT.
by elim: xs xs' H H0 {xss H1} => // x xs IHx;
  elim => // y ys IHy /= H H0; case: ifPn => [| /(total_asym Hcmp)] H1;
  [ case: xs {IHx IHy} H (IHx (y :: ys) (path_sorted H) H0) => /= [| x' xs] |
    case: ys {IHy} H0 (IHy H (path_sorted H0)) => /= [| y' ys] ];
  rewrite ?H1 //; case: ifPn => [| /(total_asym Hcmp)] H2 /= /andP [H3 _];
  rewrite ?H1 ?H3.
Qed.

Lemma perm_sort (xs : seq A) : perm_eq xs (sort xs).
Proof.
rewrite /sort /Fix.
set xss := map _ _.
have {1}->: xs = flatten xss by rewrite {}/xss; elim: xs => //= x xs {1}->.
move: (Acc_ltsize _) => Hi.
elim/Acc_ind: xss / Hi (Hi) => {xs} -[| xs [| xs' xss]] _ IH Hi;
  rewrite -Fix_F_eq //; first by rewrite /= cats0.
apply perm_eq_trans with (flatten (merge_pair (xs :: xs' :: xss)));
  last by apply IH; rewrite /= !ltnS merge_pair_leq.
elim/list2_rec: {xs xs' xss IH Hi} [:: _, _ & _] => //= xs xs' xss.
rewrite -(perm_cat2l (merge xs xs')) => /perm_eqrP <-; autoperm.
by elim: xs xs' {xss} => // x xs IHx;
  elim => [| y ys IHy /=]; last case: ifP; autoperm.
Qed.

Definition sort_finfun (I : finType) (a : {ffun I -> A}) : {ffun I -> A} :=
  let '(Tuple xs Hxs) := fgraph a in
  Finfun
    (@Tuple #|I| A (sort xs)
                   (eq_ind _ (eq_op ^~ #|I|) Hxs _
                           (perm_eq_size (perm_sort xs)))).

End Mergesort.
End Mergesort.

(* Tail-recursive Mergesort *)

Lemma flatten_filter (T : eqType) (xss : seq (seq T)) :
  flatten (filter (fun xs => xs != [::]) xss) = flatten xss.
Proof. by elim: xss => // -[| x xs] xss //= ->. Qed.

Lemma sorted_cat (A : eqType) (cmp : A -> A -> bool) (xs ys : seq A) :
  sorted cmp (xs ++ ys) =
  (sorted cmp xs && sorted cmp ys &&
   match ohead (rev xs), ohead ys with
     | Some x, Some y => cmp x y
     | _, _ => true
   end).
Proof.
rewrite -(revK xs); move: {xs} (rev xs) => xs; rewrite revK.
case: xs => [| x xs]; first by rewrite andbT.
case: ys => [| y ys]; first by rewrite /= cats0 !andbT.
rewrite rev_cons -cats1 -catA /=.
case: {xs} (rev xs) => [| x' xs]; first by rewrite andbC.
by rewrite /= !cat_path /= andbT (andbC (cmp x y)) !andbA.
Qed.

Module Mergesort_tailrec.

Fixpoint catrev' (A : Type) (xs : seq A) (y : A) (zs : seq A) :
  A * seq A :=
  if xs is x :: xs then catrev' xs x (y :: zs) else (y, zs).

Lemma catrev'E (A : Type) (xs : seq A) (y : A) (zs : seq A) :
  prod_curry cons (catrev' xs y zs) = catrev xs (y :: zs).
Proof. by elim: xs y zs => /=. Qed.

Lemma path_catrev'
      (A : eqType) (cmp : rel A) (xs : seq A) (y : A) (zs : seq A) :
  prod_curry (path cmp) (catrev' xs y zs) =
  sorted cmp (catrev xs (y :: zs)).
Proof. by rewrite -catrev'E; case: catrev'. Qed.

Section Merge.

Variables (A : eqType) (cmp : A -> A -> bool).
Hypothesis (Hcmp : total cmp).

Fixpoint merge (x : A) (xs : seq A) : A -> seq A -> seq A -> A * seq A :=
  fix merge' (y : A) (ys : seq A) (acc : seq A) {struct ys} :=
  if cmp x y
  then if xs is x' :: xs
       then merge x' xs y ys (x :: acc)
       else catrev' ys y (x :: acc)
  else if ys is y' :: ys
       then merge' y' ys (y :: acc)
       else catrev' xs x (y :: acc).

Lemma merge_perm (x y : A) (xs ys acc : seq A) :
  perm_eq (prod_curry cons (merge x xs y ys acc)) (x :: xs ++ y :: ys ++ acc).
Proof.
by elim: xs x ys y acc => [| x' xs IHl] x;
  elim => [| y' ys IHr] y acc /=; case: ifP => /= _;
  rewrite ?(perm_eqlP (IHl _ _ _ _)) ?(perm_eqlP (IHr _ _)) ?catrev'E; autoperm.
Qed.

Lemma merge_path (x y : A) (xs ys : seq A) :
  path cmp x xs -> path cmp y ys ->
  prod_curry (path (fun x y => cmp y x)) (merge x xs y ys [::]).
Proof.
move => Hxs Hys.
set acc := [::].
have: (if acc isn't a :: _ then true else cmp a x && cmp a y) by [].
have: sorted (fun x y => cmp y x) acc by [].
by elim: xs x Hxs ys y Hys acc => /= [x _ | x' xs IHx x /andP [Hx Hxs]];
  elim => /= [y _ | y' ys IHy y /andP [Hy Hys]]
             [_ _ | a acc /= Ha /andP [Hax Hay]];
  case: ifPn => /= [| /(total_asym Hcmp)] H1;
  try (apply: IHx || apply: IHy); try clear IHx; try clear IHy;
  rewrite ?path_catrev' ?catrevE ?sorted_cat ?revK ?rev_sorted /=
          ?Hx ?Hy ?Ha ?Hax ?Hay ?H1 //= ?andbT
          ?(path_sorted Hxs) ?(path_sorted Hys) /=;
  try (by case: xs Hxs => //= x'' xs /andP []);
  case: ys Hys => //= y'' ys /andP [].
Qed.

CoInductive merge_spec (x y : A) (xs ys : seq A) : A * seq A -> Prop :=
  MergeSpec z zs :
    perm_eq (z :: zs) (x :: xs ++ y :: ys) ->
    (path cmp x xs -> path cmp y ys -> path (fun x' y' => cmp y' x') z zs) ->
    merge_spec x y xs ys (z, zs).

Lemma mergeP (x y : A) (xs ys : seq A) :
  merge_spec x y xs ys (merge x xs y ys [::]).
Proof.
by case: (merge _ _ _ _ _) (merge_perm x y xs ys [::]) (@merge_path x y xs ys)
  => z zs; rewrite cats0 => H H0; constructor.
Qed.

End Merge.

Section Mergesort.

Variables (A : eqType) (cmp : A -> A -> bool).
Hypothesis (Hcmp : total cmp).

Fixpoint merge_sort_push
         (r : bool) (x : A) (xs : seq A) (yss : seq (seq A)) : seq (seq A) :=
  match yss with
    | [::] :: yss' | [::] as yss' => (x :: xs) :: yss'
    | (y :: ys) :: yss =>
      let (z, zs) :=
          if r
          then merge (fun x y => cmp y x) x xs y ys [::]
          else merge cmp y ys x xs [::]
      in
      [::] :: merge_sort_push (~~ r) z zs yss
  end.

Lemma merge_sort_pushP (r : bool) (x : A) (xs : seq A) (yss : seq (seq A)) :
  path (if r then fun x y => cmp y x else cmp) x xs ->
  foldr (fun ys f r =>
           sorted (if r then fun x y => cmp y x else cmp) ys && f (~~ r))
        xpredT yss r ->
  let zss := merge_sort_push r x xs yss in
  perm_eq (x :: xs ++ flatten yss) (flatten zss) &&
  foldr (fun ys f r =>
           sorted (if r then fun x y => cmp y x else cmp) ys && f (~~ r))
        xpredT zss r.
Proof.
elim: yss r x xs => [r x xs H | [| y ys] yss IH /= r x xs H] /=;
  autoperm; try by rewrite 1?H //=; do ?move => ->.
case/andP => H0 H1; set zs := if r then _ else _.
have: perm_eq (zs.1 :: zs.2) (x :: xs ++ y :: ys) &&
      path (if ~~ r then fun x y => cmp y x else cmp) zs.1 zs.2 by
  subst zs; case: r H H0 {H1};
  case: mergeP => //= z zs /perm_eqlP -> H H0 H1; autoperm => /=; apply H.
case: zs => /= z zs {H H0} /andP [H] /IH /(_ H1) /andP [] /perm_eqrP <- H0.
by autoperm; rewrite perm_eq_sym H.
Qed.

Fixpoint merge_sort_pop'
         (r : bool) (x : A) (xs : seq A) (yss : seq (seq A)) : seq A :=
  match yss with
    | [::] => if r then rev (x :: xs) else x :: xs
    | [::] :: [::] :: yss => merge_sort_pop' r x xs yss
    | [::] :: yss =>
      let (x', xs') := catrev' xs x [::] in
      merge_sort_pop' (~~ r) x' xs' yss
    | (y :: ys) :: yss =>
      let (z, zs) :=
          if r
          then merge (fun x y => cmp y x) x xs y ys [::]
          else merge cmp y ys x xs [::]
      in
      merge_sort_pop' (~~ r) z zs yss
  end.

Lemma merge_sort_popP' (r : bool) (x : A) (xs : seq A) (yss : seq (seq A)) :
  path (if r then fun x y => cmp y x else cmp) x xs ->
  foldr (fun ys f r =>
           sorted (if r then fun x y => cmp y x else cmp) ys && f (~~ r))
        xpredT yss r ->
  perm_eq (x :: xs ++ flatten yss) (merge_sort_pop' r x xs yss) &&
  sorted cmp (merge_sort_pop' r x xs yss).
Proof.
move: yss r x xs; fix IH 1 => -[ | [[ | [yss | y ys yss]] | y ys yss]] r x xs;
  rewrite /= ?negbK; first by case: r => /=; autoperm; rewrite ?rev_sorted.
- by case: (catrev' _ _ _) (catrev'E xs x [::]) => /= x' xs' ->;
    rewrite cats0 catrevE cats1 -rev_cons revK; case: r => /=;
    autoperm; rewrite ?rev_sorted /= => ->.
- by apply IH.
- move => H /andP [H0 H1].
  case: (catrev' _ _ _) (catrev'E xs x [::]) => /= x' xs' H2.
  set zs := if ~~ r then _ else _.
  have: perm_eq (zs.1 :: zs.2) (x :: xs ++ y :: ys) &&
        path (if r then fun x y => cmp y x else cmp) zs.1 zs.2 by
    subst zs; case: r H H0 {H1} => /= H H0;
    case: mergeP => //= z zs /perm_eqlP ->;
    rewrite -/(sorted _ (x' :: _)) -cat_cons H2 catrevE cats1
            -rev_cons rev_sorted /=; autoperm => /=; apply.
  case: zs => /= {x' xs' H H0 H2} z zs /andP [H H0].
  case/andP: (IH yss r z zs H0 H1) => /perm_eqrP <- ->.
  by rewrite andbT -!cat_cons catA perm_cat2r -(perm_eqlP H).
- move => H /andP [H0 H1].
  set zs := if r then _ else _.
  have: perm_eq (zs.1 :: zs.2) (x :: xs ++ y :: ys) &&
        path (if ~~ r then fun x y => cmp y x else cmp) zs.1 zs.2 by
    subst zs; case: r H H0 {H1} => /= H H0;
    case: mergeP => //= z zs /perm_eqlP ->; autoperm => ->.
  case: zs => /= {H H0} z zs /andP [H H0].
  by case/andP: (IH _ _ _ _ H0 H1) => /perm_eqrP <- ->;
    autoperm; rewrite andbT perm_eq_sym.
Qed.

Fixpoint merge_sort_pop (r : bool) (xss : seq (seq A)) : seq A :=
  match xss with
    | [::] => [::]
    | [::] :: xss => merge_sort_pop (~~ r) xss
    | (x :: xs) :: xss =>
      let (x', xs') := catrev' xs x [::] in merge_sort_pop' (~~ r) x' xs' xss
  end.

Lemma merge_sort_popP (r : bool) (xss : seq (seq A)) :
  foldr (fun ys f r =>
           sorted (if r then fun x y => cmp y x else cmp) ys && f (~~ r))
        xpredT xss r ->
  let ys := merge_sort_pop r xss in
  perm_eq (flatten xss) ys && sorted cmp ys.
Proof.
elim: xss r => //= -[/= xss IH r H | /= x xs xss _ r /andP []];
  first by apply IH.
case: (catrev' _ _ _) (catrev'E xs x [::]) => /= x' xs'.
rewrite catrevE cats1 -rev_cons -/(sorted _ (_ :: _)) -rev_sorted
        -/((_ :: _) ++ _) -{3}(revK (x :: _)) => <- {x xs}; autoperm.
by rewrite -cat1s perm_catCA /= => H; apply merge_sort_popP'; case: r H.
Qed.

Fixpoint merge_sort_rec (xss : seq (seq A)) (xs : seq A) : seq A :=
  match xs with
    | [::] => merge_sort_pop false xss
    | x :: [::] => merge_sort_pop' false x [::] xss
    | x :: x' :: xs' =>
      let xss' :=
          if cmp x x'
          then merge_sort_push false x [:: x'] xss
          else merge_sort_push false x' [:: x] xss
      in
      merge_sort_rec xss' xs'
  end.

Definition sort := merge_sort_rec [::].

Lemma sortP (xs : seq A) : perm_eq xs (sort xs) && sorted cmp (sort xs).
Proof.
have: foldr (fun ys f r =>
               sorted (if r then fun x y => cmp y x else cmp) ys && f (~~ r))
            xpredT [::] false by [].
rewrite -{1}(cats0 xs) -/(foldr (@cat A) [::] [::]) -/(flatten _).
rewrite /sort; move: xs [::];
  fix IH 1 => -[{IH} | x [{IH} | x' xs]] xss H /=; try autoperm.
- by apply (merge_sort_popP H).
- by apply (@merge_sort_popP' false x [::]).
- by move: (IH xs) => {IH} IH; case: ifPn => [| /(total_asym Hcmp)] H0;
    [ move: (@merge_sort_pushP false x [:: x'] xss) |
      move: (@merge_sort_pushP false x' [:: x] xss) ];
    move: (merge_sort_push _ _ _ _); rewrite /= H0 H =>
      xss' /(_ erefl erefl) /andP [H1] /IH /andP [] /perm_eqrP <- ->;
    autoperm; rewrite -(perm_eqrP H1); autoperm.
Qed.

End Mergesort.

End Mergesort_tailrec.

(* Tail-recursive Mergesort - 2 *)

Module Mergesort_tailrec2.

Lemma catrevE' (T : Type) (s t : seq T) : catrev s t = rev (rev t ++ s).
Proof. by rewrite catrevE rev_cat revK. Qed.

Definition cmplex (A : Type) (cmp1 cmp2 : rel A) (x y : A) : bool :=
  cmp1 x y && (~~ cmp1 y x || cmp2 x y).

Section Merge.

Variables (A : eqType) (cmp1 cmp2 : A -> A -> bool).
Hypothesis (Hcmp1 : total cmp1).

Notation cmplex := (cmplex cmp1 cmp2).

Fixpoint merge (xs : seq A) : seq A -> seq A -> seq A :=
  if xs is x :: xs'
  then fix merge' (ys acc : seq A) :=
         if ys is y :: ys'
         then if cmp1 x y
              then merge xs' ys (x :: acc)
              else merge' ys' (y :: acc)
         else catrev xs acc
  else @catrev _.

Lemma merge_perm (xs ys acc : seq A) :
  perm_eq (merge xs ys acc) (xs ++ ys ++ acc).
Proof.
by elim: xs ys acc => [ys acc /= | x xs IHx]; last elim => [| y ys IHy] acc /=;
  last (case: ifP => _; rewrite ?(perm_eqlP (IHx _ _)) ?(perm_eqlP (IHy _)));
  autoperm.
Qed.

Lemma merge_sorted_rec (xs ys acc : seq A) :
  sorted cmplex xs -> sorted cmplex ys -> sorted (fun x y => cmplex y x) acc ->
  (forall x y : A, x \in xs -> y \in ys -> cmp2 x y) ->
  match acc with
  | [::] => true
  | a :: _ => (if xs is x :: _ then cmplex a x else true) &&
              (if ys is y :: _ then cmplex a y else true)
  end ->
  sorted (fun x y => cmplex y x) (merge xs ys acc).
Proof.
elim: xs ys acc => /= [| x xs IHx]; elim => /= [| y ys IHy]; try by
  case => [| a acc] //= Hx Hy Ha H; rewrite ?andbT => H0;
  rewrite catrevE' rev_sorted //= rev_cons cat_rcons
          sorted_cat revK rev_sorted /= ?Hx ?Hy ?Ha ?H0.
move => acc Hx Hy Ha H H0; case: ifPn => H1; [apply IHx | apply IHy] => //=.
- apply (path_sorted Hx).
- by case: acc Ha H0 => //= a acc -> /andP [] ->.
- by move => x' y' H2; rewrite inE => /orP [/eqP |] H3;
    apply H; rewrite inE ?H2 ?H3 ?eqxx ?orbT.
- by case: xs Hx H {IHx IHy} => [| x' xs] /=;
    [move => _ | case/andP => -> _] => /(_ x y);
    rewrite /cmplex H1 !inE !eqxx => -> //; rewrite orbT.
- apply (path_sorted Hy).
- by case: acc Ha H0 => //= a acc -> /andP [] _ ->.
- by move => x' y'; rewrite inE => /orP [/eqP |] H2 H3;
    apply H; rewrite inE ?H2 ?H3 ?eqxx ?orbT.
- by rewrite {1}/cmplex H1 (total_asym Hcmp1 H1) /=;
    case: ys Hy {H IHx IHy} => [| y' ys] //= /andP [] ->.
Qed.

Lemma merge_sorted (xs ys : seq A) :
  sorted cmplex xs -> sorted cmplex ys ->
  (forall x y : A, x \in xs -> y \in ys -> cmp2 x y) ->
  sorted (fun x y => cmplex y x) (merge xs ys [::]).
Proof. by move => *; apply merge_sorted_rec. Qed.

End Merge.

Section Mergesort.

Variables (A : eqType) (cmp1 cmp2 : A -> A -> bool).
Hypothesis (Hcmp1 : total cmp1) (Hcmp2 : transitive cmp2).

Notation cmplex := (cmplex cmp1 cmp2).

Fixpoint merge_sort_push
         (r : bool) (xs : seq A) (yss : seq (seq A)) : seq (seq A) :=
  match yss with
    | [::] :: yss' | [::] as yss' => xs :: yss'
    | (y :: ys') as ys :: yss =>
      let zs :=
          if r
          then merge (fun x y => cmp1 y x) xs ys [::]
          else merge cmp1 ys xs [::]
      in
      [::] :: merge_sort_push (~~ r) zs yss
  end.

Lemma merge_sort_push_perm (r : bool) (xs : seq A) (yss : seq (seq A)) :
  perm_eq (flatten (merge_sort_push r xs yss)) (xs ++ flatten yss).
Proof.
elim: yss r xs => [| [| y ys] yss IH] r xs /=; try by autoperm.
by rewrite (perm_eqlP (IH _ _)); autoperm; case: r;
  rewrite -/(merge _ (_ :: _) _) (perm_eqlP (merge_perm _ _ _ [::])); autoperm.
Qed.

Lemma merge_sort_push_sorted (r : bool) (xs : seq A) (yss : seq (seq A)) :
  sorted (if r then fun x y => cmplex y x else cmplex) xs ->
  path (fun xs ys => all (fun x => all (fun y => cmp2 y x) ys) xs) xs
    (filter (fun ys => ys != [::]) yss) ->
  foldr (fun ys f r =>
           sorted (if r then fun x y => cmplex y x else cmplex) ys && f (~~ r))
        xpredT yss r ->
  let yss' := merge_sort_push r xs yss in
  sorted (fun xs ys => all (fun x => all (fun y => cmp2 y x) ys) xs)
    (filter (fun ys => ys != [::]) yss') &&
  foldr (fun ys f r =>
           sorted (if r then fun x y => cmplex y x else cmplex) ys &&
           f (~~ r))
        xpredT yss' r.
Proof.
elim: yss r xs => [/= r xs -> |]; first case: ifP => //.
case; first by
  move => /= yss IH r xs ->; case: ifP => /= [_ | _ /path_sorted] -> ->.
move => y ys yss IH r xs H /= /andP [H0 H1] /andP [H2 H3].
rewrite -/(merge _ (_ :: _) _ _).
set xs' := if r then _ else _.
suff/andP [H4 H5]:
  sorted (if r then cmplex else fun x y => cmplex y x) xs' &&
  path (fun xs ys => all (fun x : A => all (cmp2^~ x) ys) xs) xs'
       (filter (fun ys => ys != [::]) yss) by
  move: (IH (~~ r) xs'); rewrite if_neg H3 => /(_ H4 H5 erefl) /= ->.
subst xs'; case: r H H2 {H3} => H H2;
  rewrite merge_sorted 1?(lock merge) //= -?lock.
- case: {yss IH} (filter _ yss) H1 => //= ys' yss /andP [H1 ->];
    rewrite andbT; apply/allP => x';
    rewrite (perm_eq_mem (merge_perm _ _ _ _)) cats0 mem_cat => /orP [];
    last by move: x'; apply/allP => //=.
  by case/andP: H1 => H1 _; case/(allP H0)/andP => H3 _;
    apply/allP => y' /(allP H1) H4; apply (Hcmp2 H4 H3).
- by move => x' y' /(allP H0) /andP [H3 H4];
    rewrite inE => /orP [/eqP -> | /(allP H4)].
- case: {yss IH} (filter _ yss) H1; rewrite (lock all) (lock merge)
    => //= ys' yss /andP []; rewrite -!lock => H1 ->; rewrite andbT.
  apply/allP => x'; rewrite (perm_eq_mem (merge_perm _ _ _ _)) cats0 mem_cat
    => /orP [/(allP H1) |] // /(allP H0) /andP [H3 _].
  by case/andP: H1 => H4 _;
    apply/allP => y' /(allP H4) H5; apply (Hcmp2 H5 H3).
- by move => y' x'; rewrite inE =>
    /orP [/eqP -> | H3] /(allP H0) /andP [H4] // /allP /(_ _ H3).
Qed.

Fixpoint merge_sort_pop (r : bool) (xs : seq A) (yss : seq (seq A)) : seq A :=
  match yss with
    | [::] => if r then rev xs else xs
    | [::] :: [::] :: yss => merge_sort_pop r xs yss
    | [::] :: yss => merge_sort_pop (~~ r) (rev xs) yss
    | ys :: yss =>
      let zs :=
          if r
          then merge (fun x y => cmp1 y x) xs ys [::]
          else merge cmp1 ys xs [::]
      in
      merge_sort_pop (~~ r) zs yss
  end.

Lemma merge_sort_pop_perm (r : bool) (xs : seq A) (yss : seq (seq A)) :
  perm_eq (merge_sort_pop r xs yss) (xs ++ flatten yss).
Proof.
by move: yss r xs; fix IH 1 => -[| [[| [| y ys] yss] | y ys yss]] r xs //=;
  (try by case: r => /=; autoperm);
  rewrite ?negbK ?if_neg (perm_eqlP (IH _ _ _)); autoperm;
  case: r; rewrite -/(merge _ (_ :: _) _) (perm_eqlP (merge_perm _ _ _ _));
  autoperm.
Qed.

Lemma merge_sort_pop_sorted (r : bool) (xs : seq A) (yss : seq (seq A)) :
  sorted (if r then fun x y => cmplex y x else cmplex) xs ->
  path (fun xs ys => all (fun x => all (fun y => cmp2 y x) ys) xs) xs
    (filter (fun ys => ys != [::]) yss) ->
  foldr (fun ys f r =>
           sorted (if r then fun x y => cmplex y x else cmplex) ys && f (~~ r))
        xpredT yss r ->
  sorted cmplex (merge_sort_pop r xs yss).
Proof.
move: yss r xs; fix IH 1 => -[| [[| [| y ys] yss] | y ys yss]] r xs //=.
- by case: r; rewrite //= rev_sorted.
- by rewrite revK; case: r => //=; rewrite rev_sorted.
- by rewrite negbK; apply IH.
- rewrite negbK => H /andP [H0 H1] /andP [H2 H3].
  rewrite -/(merge _ (_ :: _) _ _) (lock merge); apply IH => //.
  + case: r H H2 {H3} => /=; rewrite -lock => H H2; apply merge_sorted;
      rewrite ?rev_sorted // => x' y'; rewrite mem_rev inE.
    * by case/orP => [/eqP -> | H3] /(allP H0) /andP [] // _ /allP /(_ _ H3).
    * by case/(allP H0)/andP => H3 H4 /orP [/eqP -> | /(allP H4)].
  + case: {yss H3} (filter _ yss) H1 =>
      // ys' yss /= /andP [] /andP [] H1 H3 ->; rewrite andbT; apply/allP => x.
    rewrite
      -lock (fun_if (fun xs => x \in xs)) !(perm_eq_mem (merge_perm _ _ _ _))
      !cats0 (perm_eq_mem (introT perm_eqlP (perm_catC _ _)))
      if_same mem_cat mem_rev inE -orbA.
    by move => /or3P [/eqP -> | /(allP H3) |] // /(allP H0) /andP [H4 _];
      apply/allP => y' /(allP H1) H5; apply (Hcmp2 H5 H4).
- move => H /andP [H0 H1] /andP [H2 H3].
  rewrite -/(merge _ (_ :: _) _ _) (lock merge); apply IH => //.
  + case: r H H2 {H3} => /=; rewrite -lock => H H2;
      apply merge_sorted => // x' y'; rewrite inE.
    * by case/(allP H0)/andP => H3 H4 /orP [/eqP -> | /(allP H4)].
    * by case/orP => [/eqP -> | H3] /(allP H0) /andP [] // _ /allP /(_ _ H3).
  + case: {yss H3} (filter _ yss) H1 =>
      // ys' yss /= /andP [] /andP [] H1 H3 ->; rewrite andbT; apply/allP => x.
    rewrite
      -lock (fun_if (fun xs => x \in xs)) !(perm_eq_mem (merge_perm _ _ _ _))
      !cats0 (perm_eq_mem (introT perm_eqlP (perm_catC _ _)))
      if_same mem_cat inE -orbA.
    by move => /or3P [/eqP -> | /(allP H3) |] // /(allP H0) /andP [H4 _];
      apply/allP => y' /(allP H1) H5; apply (Hcmp2 H5 H4).
Qed.

Fixpoint merge_sort_rec (xss : seq (seq A)) (xs : seq A) : seq A :=
  match xs with
    | [::] => merge_sort_pop false [::] xss
    | x :: [::] => merge_sort_pop false [:: x] xss
    | x :: x' :: xs' =>
      merge_sort_rec
        (merge_sort_push
           false (if cmp1 x x' then [:: x; x'] else [:: x'; x]) xss)
        xs'
  end.

Lemma merge_sort_rec_perm (xss : seq (seq A)) (xs : seq A) :
  perm_eq (merge_sort_rec xss xs) (xs ++ flatten xss).
Proof.
move: xs xss; fix IH 1 => -[| x [| x' xs]] xss /=;
  rewrite ?(perm_eqlP (merge_sort_pop_perm _ _ _)); autoperm => //.
by case: ifP => _; rewrite (perm_eqlP (IH _ _)); autoperm;
  rewrite (perm_eqlP (merge_sort_push_perm _ _ _)); autoperm.
Qed.

Lemma merge_sort_rec_sorted (xss : seq (seq A)) (xs : seq A) :
  sorted cmp2 xs ->
  path (fun xs ys => all (fun x => all (fun y => cmp2 y x) ys) xs) xs
    (filter (fun xs => xs != [::]) xss) ->
  foldr (fun xs f r =>
           sorted (if r then fun x y => cmplex y x else cmplex) xs && f (~~ r))
        xpredT xss false ->
  sorted cmplex (merge_sort_rec xss xs).
Proof.
move: xs xss; fix IH 1 => -[| x [| x' xs]] xss /=;
  try by move => *; apply merge_sort_pop_sorted.
case/andP => H H0 H1 H2.
have H3: sorted cmplex (if cmp1 x x' then [:: x; x'] else [:: x'; x])
  by case: ifPn => /= H3; rewrite /cmplex H3 ?H ?orbT ?(total_asym Hcmp1 H3).
have H4:
  path (fun xs ys => all (fun x => all (fun y => cmp2 y x) ys) xs)
    (if cmp1 x x' then [:: x; x'] else [:: x'; x]) [seq ys <- xss | ys != [::]]
  by case: {xss H2 H3} (filter _ _) H1 => //= xs' xss'; rewrite -!andbA
    => /and4P [H1 H2 H3 ->]; rewrite andbT; apply/allP => ?;
    rewrite (fun_if (fun xs => _ \in xs)) !inE orbC if_same => /orP [] /eqP ->.
move: (merge_sort_push_sorted (r := false) H3 H4 H2) => /= /andP [] H5 H6.
apply: IH => // {H2 H3 H4 H6}; first by apply (path_sorted H0).
move: H5; set xss' := filter _ _.
have: perm_eq (flatten xss') (x' :: x :: flatten xss) by
  rewrite flatten_filter (perm_eqlP (merge_sort_push_perm _ _ _));
  case: ifP; autoperm.
case: xss' => //= xs' xss' H2 ->; rewrite andbT.
apply/allP => y /(allP (order_path_min Hcmp2 H0)) H3; apply/allP => x''.
move/(@or_introl _ (x'' \in flatten xss'))/orP;
  rewrite -mem_cat (perm_eq_mem H2) !inE => /or3P [/eqP -> // | /eqP -> | H4];
  apply: (Hcmp2 _ H3) => // {xs' xss' y H H0 H2 H3}.
have H: x' \in [:: x, x' & xs] by rewrite !inE eqxx orbT.
elim: {x xs} xss x' [:: x, x' & xs] H1 H H4
    => // -[] //= x xs xss IH x' xs' /andP [H H0] /(allP H) /andP [H1 H2];
  rewrite -/(all _ (_ :: _)) -/((_ :: _) ++ _) mem_cat
    => /orP [/(allP (s := _ :: _) (introT andP (conj H1 H2))) | H3] //.
by apply: (Hcmp2 _ H1); apply (IH _ (x :: xs)) => //; rewrite inE eqxx.
Qed.

Definition sort := merge_sort_rec [::].

Lemma perm_sort (xs : seq A) : perm_eq (sort xs) xs.
Proof. by rewrite /sort (perm_eqlP (merge_sort_rec_perm _ _)) cats0. Qed.

Lemma sort_sorted (xs : seq A) : sorted cmp2 xs -> sorted cmplex (sort xs).
Proof. by rewrite /sort => H; apply merge_sort_rec_sorted. Qed.

End Mergesort.

End Mergesort_tailrec2.

Goal sort leq (iota 0 24) = [::].
Proof.
rewrite /iota /sort /merge_sort_rec /leq eqxx -/leq.
rewrite (lock merge_sort_push); set push := locked _.
rewrite {12}/push -lock /=.
rewrite {11}/push -lock /=.
rewrite {10}/push -lock /=.
rewrite {9}/push -lock /=.
rewrite {8}/push -lock /=.
rewrite {7}/push -lock /=.
rewrite {6}/push -lock /=.
rewrite {5}/push -lock /=.
rewrite {4}/push -lock /=.
rewrite {3}/push -lock /=.
rewrite {2}/push -lock /=.
rewrite /push -lock /=.
Abort.

Goal Mergesort_tailrec.sort leq (iota 0 24) = [::].
Proof.
rewrite /iota /Mergesort_tailrec.sort /Mergesort_tailrec.merge_sort_rec
        /leq eqxx -/leq.
rewrite (lock Mergesort_tailrec.merge_sort_push); set push := locked _.
rewrite {12}/push -lock /=.
rewrite {11}/push -lock /=.
rewrite {10}/push -lock /=.
rewrite {9}/push -lock /=.
rewrite {8}/push -lock /=.
rewrite {7}/push -lock /=.
rewrite {6}/push -lock /=.
rewrite {5}/push -lock /=.
rewrite {4}/push -lock /=.
rewrite {3}/push -lock /=.
rewrite {2}/push -lock /=.
rewrite /push -lock /=.
Abort.

Eval compute in
  Mergesort_tailrec.sort (fun _ _ => true) [seq (0, i) | i <- iota 0 100].
Time Eval vm_compute in sort leq (iota 0 1024).
Time Eval vm_compute in Mergesort_tailrec.sort leq (iota 0 1024).
Time Eval vm_compute in Mergesort_tailrec2.sort leq (iota 0 1024).

Require Import extraction_ocaml.
Unset Extraction SafeImplicits.
Set Extraction Flag 8175.

Extraction Implicit merge [T].
Extraction Implicit merge_sort_push [T].
Extraction Implicit merge_sort_pop [T].
Extraction Implicit merge_sort_rec [T].
Extraction Implicit sort [T].

Extraction Implicit Mergesort.merge [A].
Extraction Implicit Mergesort.merge_pair [A].
Extraction Implicit Mergesort.sort [A].

Extraction Implicit Mergesort_tailrec.catrev' [A].
Extraction Implicit Mergesort_tailrec.merge [A].
Extraction Implicit Mergesort_tailrec.merge_sort_push [A].
Extraction Implicit Mergesort_tailrec.merge_sort_pop' [A].
Extraction Implicit Mergesort_tailrec.merge_sort_pop [A].
Extraction Implicit Mergesort_tailrec.merge_sort_rec [A].
Extraction Implicit Mergesort_tailrec.sort [A].

Extraction Implicit Mergesort_tailrec2.merge [A].
Extraction Implicit Mergesort_tailrec2.merge_sort_push [A].
Extraction Implicit Mergesort_tailrec2.merge_sort_pop [A].
Extraction Implicit Mergesort_tailrec2.merge_sort_rec [A].
Extraction Implicit Mergesort_tailrec2.sort [A].

Extraction
  "mergesort.ml"
  iota sort Mergesort.sort Mergesort_tailrec.sort Mergesort_tailrec2.sort.