(* We load a small arithmetic library *)
(* essentially for properties of the order on nat *)
Require Import Arith.

(* look how natural numbers are defined *)
Print nat.

Search (0 <= _).
Search (0 < _).

(* we want to compare natural numbers *)
Fixpoint comp x y :=
match x, y with
  | 0,_ => true
  | S _, 0 => false
  | S x, S y => comp x y

(* This formulation will be handy when using comp *)
Lemma comp_corr : forall x y,
                    (comp x y = true /\ x<=y)
                    \/(comp x y = false /\ y<x).
induction x as [|x]; destruct y as [|y].
- left; auto.
- left; split; trivial.
  apply le_0_n.
- right; split; trivial.
  apply lt_0_Sn.
- destruct (IHx y) as [[e h]|[e h]]; simpl; rewrite e.
  left; split; trivial; apply le_n_S; trivial.
right; split; trivial; apply lt_n_S; trivial.

Inductive list :=
  nil | cons : nat -> list -> list.

(* Check the induction principle *)
Check list_ind.

Fixpoint app (l m : list) :=
  match l with
    | nil => m
    | cons x l' => cons x (app l' m)

(* easy *)
Lemma app_ass : forall l m n,
                  app l (app m n) = app (app l m) n.
induction l as [| x l]; intros m n; simpl; trivial.
rewrite IHl; trivial.

Fixpoint length (l : list) : nat :=
  match l with
    | nil => 0
    | cons _ l' => S(length l')

Lemma app_length : forall l m, length (app l m) = length l + length m.
induction l as [|x l]; intros m; trivial.
simpl; rewrite IHl; trivial.

(* permut states that two lists are a permutation *)
(* of one another *)
(* Currently we just axiomatise it *)
Parameter permut : list -> list -> Prop.

Axiom permut_refl : forall l, permut l l.
Axiom permut_trans :
  forall l1 l2 l3,
    permut l1 l2 -> permut l2 l3 ->
       permut l1 l3.
Axiom permut_step : forall l1 l2 x,
      permut (cons x (app l1 l2))(app l1 (cons x l2)).
Axiom permut_congr : forall x l1 l2,
                       permut l1 l2 -> permut (cons x l1)(cons x l2).

(* The apply ... with tactic *)
Lemma ex : permut (cons 3 (cons 2 (cons 1 nil)))
                  (cons 1 (cons 2 (cons 3 nil))).
apply permut_trans with (cons 3 (cons 1 (cons 2 nil))).
  apply permut_congr.
  apply (permut_step (cons 1 nil) nil).
apply (permut_step (cons 1 (cons 2 nil))).

(* What it means for a list to be sorted *)
Definition lower x l :=
  match l with
    | nil => True
    | cons y _ => x <= y

Fixpoint sorted (l : list) :=
  match l with
    | nil => True
    | cons x l => lower x l /\ sorted l

Lemma lower_trans : forall l x y,
                      lower x l -> y <= x -> lower y l.
intros [|z l] x y; simpl; trivial.
intros; apply le_trans with x; trivial.

(* Define the function which inserts x in a list l *)
(* preserving the sorted property *)
(* (for now we do not prove anything) *)
(* you should use comp *)
Fixpoint ins (l : list)(x : nat) :=
  match l with
    | nil => cons x nil
    | cons y l' as l =>
      if (comp x y)
      then (cons x l)
      else (cons y (ins l' x))

(* use ins to define insertion sort *)
Fixpoint tri (l : list) : list :=
  match l with
    | nil => nil
    | cons x l => ins (tri l) x

Eval compute in (tri (cons 4 (cons 2 (cons 1 (cons 5 nil))))).

(* Let us prove properties wrt permutation *)

Lemma ins_ex : forall l x, exists l1 l2,
                 ins l x = app l1 (cons x l2)
                               /\ l = (app l1 l2).
induction l as [|y l]; intros x; simpl.
  exists nil; exists nil; split; trivial.
destruct (comp x y); simpl.
  exists nil; exists (cons y l); simpl; split; trivial.
destruct (IHl x) as [l1 [l2 [e1 e2]]].
exists (cons y l1); exists l2; rewrite e1, e2.
split; simpl; trivial.

Lemma ins_permut : forall x l, permut (cons x l)(ins l x).
intros x l; destruct (ins_ex l x) as [l1 [l2 [e1 e2]]].
rewrite e1, e2.
apply permut_step.

Lemma tri_permut : forall l, permut l (tri l).
induction l as [|x l].
  apply permut_refl.
apply permut_trans with (cons x (tri l)).
  apply permut_congr; trivial.
apply ins_permut.

(* Now we want to prove that the sort function *)
(* preserves sorted *)

(* We want to prove the following property *)
(* But may need to provide a stronger induction hypothesis *)
(* Can you see which one ?? *)
Lemma ins_sorted_aux : forall x l, sorted l ->
                sorted (ins l x)/\(forall z, z<= x -> lower z l -> lower z (ins l x)).
intros x; induction l as [|y l]; simpl.
  intros; split; try split; trivial.
intros [h sl].
destruct (IHl sl) as [h1 h2].
destruct (comp_corr x y) as [[e h']|[e h']];
   rewrite e; split; try split; simpl; trivial.
  split; trivial.
apply h2; trivial.
apply lt_le_weak; trivial.

Lemma tri_sorted : forall l, sorted (tri l).
induction l as [|x l]; simpl.
destruct (ins_sorted_aux x _ IHl).

(* Functional heapsort *)

  (* insertion sort is of complexity n^2  *)
  (* You can try to define and prove correct a similar but
efficient sorting algorithm using binary trees *)

Inductive tree :=
| Leaf : tree
| Node : nat -> tree -> tree -> tree.

Fixpoint tinsert t x :=
  match t with
    | Leaf => (Node x Leaf Leaf)
    | Node y t1 t2 =>
      if comp x y
      then Node x (tinsert t2 y) t1
      else Node y (tinsert t2 x) t2

(* The rest of the construction is similar to what you have done above *)

Fixpoint permutt (t : tree)(l : list) :=
  match t, l with
    | Leaf, nil => True
    | Leaf, _ => False
    |Node x t1 t2, l =>
     exists l1 l2, permutt t1 l1 /\ permutt t2 l2 /\ permut (cons x (app l1 l2)) l

Axiom perm_nil : forall x l, ~permut nil (cons x l).
Axiom perm_nil' : forall x l, ~permut (cons x l) nil.
Axiom perm_trans : forall l1 l2 l3, permut l1 l2 -> permut l2 l3 -> permut l1 l3.

Lemma permt : forall t l1 l2,
              permutt t l1 -> permut l1 l2 -> permutt t l2.
intros [|x t1 t2]; simpl.
 intros [|y1 l1][|y2 l2]; trivial.
   intros; elim (perm_nil y2 l2); auto.
intros l1 l2 [l3 [l4 [h1 [h2 h3]]]] p.
exists l3; exists l4.
split; auto.
split; auto.
apply perm_trans with l1; auto.

Lemma ins_permutt : forall t x l,
  permutt t l -> permutt (tinsert t x) (cons x l).
induction t as [|y t1 t2]; simpl; intros x [| z l].
  intros _; exists nil; exists nil; simpl.
  split; trivial; split; trivial; apply permut_refl.
  destruct 1.
  intros [l1 [l2 [_ [_ h]]]].
  elim (perm_nil' _ _ h).