# lists_sol

(* 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
end.

(* 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.
Qed.

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)
end.

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

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

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

(* permut states that two lists are a permutation *)
(* of one another *)
(* WE WILL SEE NEXT WEEK HOW TO DEFINE IT  *)
(* 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))).
Qed.

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

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

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

(* 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))
end.

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

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).
Proof.
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.
Qed.

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

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

(* 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)).
Proof.
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.
Qed.

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

(* 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
end.

(* 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
end.

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.
Proof.
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.
Qed.

Lemma ins_permutt : forall t x l,
permutt t l -> permutt (tinsert t x) (cons x l).
Proof.
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).
Abort.