Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import Extraction.


(* 練習問題5.1 *)

Section sort.
Variable A : eqType.
Variable le : A -> A -> bool.
Variable le_trans: forall x y z, le x y -> le y z -> le x z.
Variable le_total: forall x y, ~~ le x y -> le y x.
Fixpoint insert a l := match l with
  | nil => (a :: nil)
  | b :: l' => if le a b
      then a :: l
      else b :: insert a l'
  end.
Fixpoint isort l := if l is a :: l' then insert a (isort l') else nil.

Fixpoint sorted l := (* allを使ってbool上の述語を定義する *) if l is a :: l'
  then all (le a) l' && sorted l'
  else true.

Lemma le_seq_insert a b l : le a b -> all (le a) l -> all (le a) (insert b l).
Proof. elim: l => /= [-> // | c l IH].
move=> leab. move => /andP [leac leal].
case: ifPn => lebc /=.
- rewrite leab leac. done.
- by rewrite leac IH.
Qed.
Lemma le_seq_trans a b l : le a b -> all (le b) l -> all (le a) l.
Proof.
move=> leab /allP lebl. apply/allP => x Hx. by apply/le_trans/lebl.
Qed.
Theorem insert_ok a l : sorted l -> sorted (insert a l).
Proof.
  elim: l.
  + done.
  + move => b l'.
    move => IH.
    simpl.
    case: ifPn.
    move => leab.
    simpl.
    rewrite leab andTb.
    move => /andP  [allbl' sortedl'].
    rewrite allbl' sortedl' !andbT.
    apply (le_seq_trans a b l').
    - assumption.
    - assumption.
  + move => leba /andP [lebl' sortedl'].
    rewrite /=.
    rewrite le_seq_insert.
    rewrite andTb.
    by apply IH.
    by apply le_total.
    assumption.
Qed.
Theorem isort_ok l : sorted (isort l).
Proof.
  elim: l.
  + done.
  + move => a l' IH.
    simpl.
    apply insert_ok.
    assumption.
Qed.


(* perm_eq が seq で定義されているが補題だけを使う *)
Theorem insert_perm l a : perm_eq (a :: l) (insert a l).
Proof.
elim: l => //= b l pal.
case: ifPn => //= leab. by rewrite (perm_catCA [:: a] [:: b]) perm_cons.
Qed.
Check perm_catCA.

(*
perm_catCA
     : forall (T : eqType) (s1 s2 s3 : seq T), perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3)
   *)
(* perm_eq_trans : forall (T : eqType), transitive (seq T) perm_eq *)
Search "perm_eq".
Check perm_eq_sym.
Check perm_cons.
Theorem isort_perm l : perm_eq l (isort l).
Proof.
  elim: l.
  + done.
  + move => a l' IH.
    simpl.
    rewrite perm_eq_sym.
    apply: perm_eq_trans.
    rewrite perm_eq_sym.
    apply insert_perm.
    rewrite perm_cons.
    by rewrite perm_eq_sym.

Qed.

End sort.

Check isort.

Definition isortn : seq nat -> seq nat := isort _ leq.
Definition sortedn := sorted _ leq.
Lemma leq_total a b : ~~ (a <= b) -> b <= a.
  rewrite leqNgt.
  Search (reflect _ (~~ _)).
  move => /negPn a_nleq_b .
  rewrite <- ltnS.
  apply: leq_trans.
  apply a_nleq_b.
  rewrite <- addn1.
  apply leq_addr.
Qed.
Theorem isortn_ok l : sortedn (isortn l) && perm_eq l (isortn l).
Proof.
  rewrite isort_perm andbT.
  rewrite /sortedn.
  rewrite isort_ok.
  reflexivity.
  move => x y z.
  apply: leq_trans.
  move => x y.
  apply leq_total.
Qed.
Require Import Extraction. Extraction "isort.ml" isortn.
Extraction leq.