Library Lebesgue.sort_compl
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Used logic axioms
- classic, the weak form of excluded middle;
- classic_dec, an alias for excluded_middle_informative, the strong form of excluded middle.
From Requisite Require Import stdlib.
From Coq Require Import List Sorted Permutation.
From Subsets Require Import Subsets_wDep.
From Lebesgue Require Import list_compl.
Local Open Scope list_scope.
Section Insertion_sort.
Insertion sort.
Context {A : Set}.
Variable ord : A → A → Prop.
Lemma Permutation_ex :
∀ (a : A) l l',
Permutation (a :: l) l' →
∃ l1 l2,
l' = l1 ++ (cons a l2) ∧ Permutation l (l1 ++ l2).
Proof.
intros a l l' Hl.
assert (H:In a l').
apply Permutation_in with (a::l); try easy.
apply in_eq.
destruct (in_split _ _ H) as (l1,(l2, H1)).
∃ l1; ∃ l2; split; try easy.
apply Permutation_cons_inv with a.
rewrite H1 in Hl.
apply Permutation_trans with (1:=Hl).
rewrite Permutation_app_comm.
simpl.
apply perm_skip.
apply Permutation_app_comm.
Qed.
Definition leqb : A → A → bool :=
fun x y ⇒ match classic_dec (ord x y) with
| left _ ⇒ true
| right _ ⇒ false
end.
Lemma leqb_true : ∀ a b, leqb a b = true → ord a b.
Proof.
intros a b H.
unfold leqb in H.
destruct (classic_dec (ord a b));easy.
Qed.
Lemma leqb_false : ∀ a b, leqb a b = false → ¬ord a b.
Proof.
intros a b H.
unfold leqb in H.
destruct (classic_dec (ord a b));easy.
Qed.
Fixpoint insert (x : A) (l : list A) {struct l} : list A :=
match l with
| nil ⇒ x :: nil
| y :: tl ⇒ if leqb x y then x :: l else y :: insert x tl
end.
Fixpoint sort (l : list A) : list A :=
match l with
| nil ⇒ nil
| x :: tl ⇒ insert x (sort tl)
end.
Lemma corr_insert : ∀ (x : A) l, Permutation (x :: l) (insert x l).
Proof.
intros x.
induction l;intros.
simpl;apply perm_skip.
apply perm_nil.
simpl.
case (leqb x a).
apply Permutation_refl.
assert (Permutation (a::x::l) (a:: insert x l)).
now apply perm_skip.
apply perm_trans with (l':=(a::x::l));auto.
apply perm_swap.
Qed.
Lemma corr_sort : ∀ l, Permutation l (sort l).
Proof.
induction l;intros.
simpl;apply perm_nil.
apply perm_trans with (l':=(a::(sort l)));auto.
simpl;apply corr_insert.
Qed.
Lemma LocallySorted_0_1 :
∀ P l (a0 a : A),
l ≠ nil → LocallySorted P l → LocallySorted P (a0 :: l) →
P a0 (nth 0 l a).
Proof.
intros P; induction l;intros.
exfalso;now apply H.
inversion H1.
now simpl.
Qed.
Lemma LocallySorted_cons :
∀ P (a : A) l,
LocallySorted P (a :: l) →
LocallySorted P l.
Proof.
induction l;simpl;intros.
apply LSorted_nil.
now inversion H.
Qed.
Lemma LocallySorted_0_1_alt :
∀ P (a : A) l,
LocallySorted P l → (1 < length l)%nat →
P (nth 0 l a) (nth (S 0) l a).
Proof.
induction l.
simpl;intros.
contradict H0; easy.
intros.
simpl.
case_eq l; try easy.
intros H1; contradict H0; rewrite H1; simpl; auto with arith.
intros a1 l0 H1; rewrite H1 in H.
apply LocallySorted_0_1; try discriminate; auto.
now apply LocallySorted_cons with a0.
Qed.
Lemma LocallySorted_nth :
∀ P (a : A) l,
(∀ i, (i < length l - 1)%nat →
LocallySorted P l →
P (nth i l a) (nth (S i) l a)).
Proof.
intros P; induction l;intros.
inversion H.
destruct (eq_nat_dec i 0).
rewrite e;simpl;apply LocallySorted_0_1;auto.
red;intro;rewrite H1 in H;simpl in H.
inversion H.
now apply LocallySorted_cons with a0.
assert ((i-1<length l - 1)%nat).
rewrite length_cons_1 in H.
assert ((length l + 1 - 1)=length l)%nat.
lia.
rewrite H1 in H;lia.
assert (LocallySorted P l).
now apply LocallySorted_cons with a0.
generalize (IHl (i-1)%nat H1 H2);clear IHl;intro IHl.
rewrite (nth_cons a0 a l (i-1)%nat) in IHl.
assert (S (i - 1)=i)%nat.
lia.
rewrite H3 in IHl;now rewrite <-(nth_cons a0 a l).
Qed.
Lemma insert_hd_dec :
∀ (a r : A) l, {hd a (insert r l) = r} + {hd a (insert r l) = hd a l}.
Proof.
intros n r l;induction l.
left;simpl;reflexivity.
simpl;destruct (leqb r a).
left;simpl;reflexivity.
right;simpl;reflexivity.
Qed.
Lemma LocallySorted_insert :
∀ l a,
(∀ x y, ¬ ord x y → ord y x) →
LocallySorted ord l →
LocallySorted ord (insert a l).
Proof.
intros l a Hord Hl; simpl;induction l;simpl.
apply LSorted_cons1.
case_eq (leqb a a0).
intros;apply LSorted_consn;auto.
now apply leqb_true.
intros;case_eq (insert a l).
intros H0;apply LSorted_cons1;auto.
intros r l0 H0;
destruct (insert_hd_dec a0 a l) as [H1 | H2].
case_eq (leqb a0 r);intro H2.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl.
now apply LocallySorted_cons with a0.
now apply leqb_true.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl;
now apply LocallySorted_cons with a0.
rewrite H0 in H1;simpl in H1;rewrite <- H1 in H;
generalize (leqb_false r a0 H).
intro H3;apply Hord; easy.
case_eq (leqb a0 r);intro H3.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl.
now apply LocallySorted_cons with a0.
now apply leqb_true.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl.
now apply LocallySorted_cons with a0.
rewrite H0 in H2;simpl in H2;rewrite H2; simpl.
inversion Hl; simpl.
destruct (classic (ord a0 a0));auto.
easy.
Qed.
Lemma LocallySorted_sort :
∀ l,
(∀ x y, ¬ ord x y → ord y x) →
LocallySorted ord (sort l).
Proof.
intros l Hord; induction l.
apply LSorted_nil.
simpl; now apply (LocallySorted_insert (sort l) a).
Qed.
Lemma LocallySorted_impl :
∀ (P1 P2 P3 : A → A → Prop) l,
(∀ a b, P1 a b → P2 a b → P3 a b) →
LocallySorted P1 l → LocallySorted P2 l → LocallySorted P3 l.
Proof.
intros P1 P2 P3; intros l; case l.
intros; apply LSorted_nil.
clear l; intros r1 l; generalize r1; clear r1.
induction l.
intros; apply LSorted_cons1.
intros r1 H0 H1 H2.
apply LSorted_consn.
apply IHl; try easy.
now apply LocallySorted_cons with r1.
now apply LocallySorted_cons with r1.
apply H0.
now inversion H1.
now inversion H2.
Qed.
Lemma LocallySorted_impl1 :
∀ {B : Type} (P1 P2 : B → B → Prop) l,
(∀ a b, P1 a b → P2 a b) →
LocallySorted P1 l → LocallySorted P2 l.
Proof.
intros B P1 P2; induction l as [ | a]; intros H H1.
apply LSorted_nil.
induction l as [ | b].
apply LSorted_cons1.
apply LSorted_consn.
apply IHl; try easy.
assert (LocallySorted_cons :
∀ P a (l : list B),
LocallySorted P (a :: l) → LocallySorted P l).
intros P a' l' H'.
induction l'; simpl.
apply LSorted_nil.
now inversion H'.
now apply LocallySorted_cons with (a := a).
apply H.
now inversion H1.
Qed.
Lemma LocallySorted_neq :
∀ l, NoDup l → LocallySorted (fun x y : A ⇒ x ≠ y) l.
Proof.
intros l; case l.
intros; apply LSorted_nil.
clear l; intros a l; generalize a; clear a.
induction l.
intros; apply LSorted_cons1.
intros b H1.
apply LSorted_consn.
apply IHl; try easy.
now apply (NoDup_cons_iff b (a::l)).
assert (~(In b (a::l))).
now apply (NoDup_cons_iff b (a::l)).
intros H2; apply H; rewrite H2.
apply in_eq.
Qed.
Lemma LocallySorted_extends :
∀ l (a x : A),
(∀ x y z, ord x y → ord y z → ord x z) →
LocallySorted ord (a :: l) →
In x l → ord a x.
Proof.
intros l a x Ho Hl.
apply Forall_forall.
apply Sorted_extends; try assumption.
now apply Sorted_LocallySorted_iff.
Qed.
Lemma LocallySorted_cons2 :
∀ (a b : A) l,
(∀ x y z, ord x y → ord y z → ord x z) →
LocallySorted ord (a :: b :: l) → LocallySorted ord (a :: l).
Proof.
intros a b l Ho Hl.
inversion Hl; inversion H1.
apply LSorted_cons1.
apply LSorted_consn; try easy.
now apply Ho with b.
Qed.
Lemma LocallySorted_select :
∀ P l,
(∀ x y z, ord x y → ord y z → ord x z) →
LocallySorted ord l →
LocallySorted ord (select P l).
Proof.
induction l.
intros;apply LSorted_nil.
intros Ho H1.
generalize (LocallySorted_cons ord a l H1);intro H2.
simpl;case (in_dec P a);intro H.
2: now apply IHl.
generalize (IHl Ho H2);intro H0.
case_eq (select P l).
intros _; apply LSorted_cons1.
intros b l' H3.
apply LSorted_consn.
rewrite <- H3; easy.
apply LocallySorted_extends with l; try easy.
apply In_select_In with P.
rewrite H3; apply in_eq.
Qed.
Lemma LocallySorted_map :
∀ (P : A → A → Prop) f l,
(∀ x y, P x y → P (f x) (f y)) →
LocallySorted P l →
LocallySorted P (map f l).
Proof.
intros P f l; case l.
intros H1 H2; simpl.
apply LSorted_nil.
clear l; intros a l; generalize a; clear a.
induction l.
intros a H1 H2; simpl.
apply LSorted_cons1.
intros b H1 H2; simpl.
apply LSorted_consn.
apply IHl; try easy.
inversion H2; easy.
apply H1.
inversion H2; easy.
Qed.
End Insertion_sort.