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