Library tri_ex

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.

Un exemple typique de fermeture reflexive transitive par definition inductive

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.

Une sÚrie de petits lemmes sur les permutations

Lemma step_permut : forall a b, permut_step a b -> permut a b.
Proof.

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.

Lemma step_sym : forall a b, permut_step a b -> permut_step b a.
Proof.

Lemma permut_sym : forall a b, permut a b -> permut b a.
Proof.

Lemma permut_step_hd : forall a l1 l2,
  permut_step l1 l2 -> permut_step (a::l1) (a::l2).
Proof.

Lemma permut_hd : forall a l1 l2,
  permut l1 l2 -> permut (a::l1) (a::l2).

Lemma permut_swap1 : forall a b l1,
  permut (a::b::l1) (b::a::l1).
Proof.

Lemma permut_swap : forall a b l1 l2,
  permut (a::b::l1) l2 -> permut (b::a::l1) l2.
Proof.

Lemma permut_middle : forall x l1 l2, permut (x::l1++l2)(l1++x::l2).
Proof.

Lemma permut_middle' : forall x l1 l2 l3, permut (x::l1++l2) l3 -> permut (l1++x::l2) l3.
Proof.

Lemma permut_switch : forall x1 l1 x2 l2 l3,
permut (x1 :: l1 ++ x2 :: l2) l3 -> permut (x2 :: l1 ++ x1 :: l2) l3.
Proof.

Lemma permut_app : forall l1 l2, permut (l1++l2) (l2++l1).
Proof.

Lemma permut_app_r : forall l1 l2 l, permut l1 l2 -> permut (l++l1) (l++l2).

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.

La notion de liste triee

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.

Tri par insertion
Fixpoint insert (n:nat)(l:list nat) :=



Lemma insert_perm : forall n l, permut (n::l) (insert n l).

Remarquez l'hypothese renforcee
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.

Fixpoint sort (l:list nat) :=
end.

Lemma sort_sorted : forall l, sorted (sort l).
Qed.

Lemma sort_permut : forall l, permut l (sort l).

mergesort

Plus efficace maintenant

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<x2
     then x1::(merge l1' l2)
     else x2::(aux l2')
end
in aux.

Lemma aux : forall l1 l2 x1, let aux :=
     fix aux (l:list nat) :=
      match l with nil => (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.

Lemma sort_ord : forall a b l, a<=b -> sorted (b::l) -> ord1 a l.
Proof.

Lemma ord1_trans : forall a b l, ord1 a l -> b <= a -> ord1 b l.
Proof.

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

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.

Un algo astucieux

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

Lemma merge_sort_permut : forall l, permut l (merge_sort l).
Proof.

Fixpoint l_sorted (L:stack) : Prop :=
match L with



Hint Resolve merge_sorted.

Lemma add_sorted : forall L l, sorted l -> l_sorted L -> l_sorted (add l L).
Proof.

Lemma flat_sorted : forall L, l_sorted L -> sorted (flat L).

Lemma stack_sorted : forall l, l_sorted (to_stack l).
Proof.

Lemma merge_sorte_sorted : forall l, sorted (merge_sort l).
Proof.