diff options
Diffstat (limited to 'theories/Sorting/Sorted.v')
-rw-r--r-- | theories/Sorting/Sorted.v | 154 |
1 files changed, 154 insertions, 0 deletions
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v new file mode 100644 index 00000000..2b9f59f0 --- /dev/null +++ b/theories/Sorting/Sorted.v @@ -0,0 +1,154 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(* Made by Hugo Herbelin *) + +(** This file defines two notions of sorted list: + + - a list is locally sorted if any element is smaller or equal than + its successor in the list + - a list is sorted if any element coming before another one is + smaller or equal than this other element + + The two notions are equivalent if the order is transitive. +*) + +Require Import List Relations Relations_1. + +(** Preambule *) + +Set Implicit Arguments. +Local Notation "[ ]" := nil (at level 0). +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0). +Implicit Arguments Transitive [U]. + +Section defs. + + Variable A : Type. + Variable R : A -> A -> Prop. + + (** Locally sorted: consecutive elements of the list are ordered *) + + Inductive LocallySorted : list A -> Prop := + | LSorted_nil : LocallySorted [] + | LSorted_cons1 a : LocallySorted [a] + | LSorted_consn a b l : + LocallySorted (b :: l) -> R a b -> LocallySorted (a :: b :: l). + + (** Alternative two-step definition of being locally sorted *) + + Inductive HdRel a : list A -> Prop := + | HdRel_nil : HdRel a [] + | HdRel_cons b l : R a b -> HdRel a (b :: l). + + Inductive Sorted : list A -> Prop := + | Sorted_nil : Sorted [] + | Sorted_cons a l : Sorted l -> HdRel a l -> Sorted (a :: l). + + Lemma HdRel_inv : forall a b l, HdRel a (b :: l) -> R a b. + Proof. + inversion 1; auto. + Qed. + + Lemma Sorted_inv : + forall a l, Sorted (a :: l) -> Sorted l /\ HdRel a l. + Proof. + intros a l H; inversion H; auto. + Qed. + + Lemma Sorted_rect : + forall P:list A -> Type, + P [] -> + (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> + forall l:list A, Sorted l -> P l. + Proof. + induction l; firstorder using Sorted_inv. + Qed. + + Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l. + Proof. + split; [induction 1 as [|a l [|]]| induction 1]; + auto using Sorted, LocallySorted, HdRel. + inversion H1; subst; auto using LocallySorted. + Qed. + + (** Strongly sorted: elements of the list are pairwise ordered *) + + Inductive StronglySorted : list A -> Prop := + | SSorted_nil : StronglySorted [] + | SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l). + + Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) -> + StronglySorted l /\ Forall (R a) l. + Proof. + intros; inversion H; auto. + Defined. + + Lemma StronglySorted_rect : + forall P:list A -> Type, + P [] -> + (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> + forall l, StronglySorted l -> P l. + Proof. + induction l; firstorder using StronglySorted_inv. + Defined. + + Lemma StronglySorted_rec : + forall P:list A -> Type, + P [] -> + (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> + forall l, StronglySorted l -> P l. + Proof. + firstorder using StronglySorted_rect. + Qed. + + Lemma StronglySorted_Sorted : forall l, StronglySorted l -> Sorted l. + Proof. + induction 1 as [|? ? ? ? HForall]; constructor; trivial. + destruct HForall; constructor; trivial. + Qed. + + Lemma Sorted_extends : + Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l. + Proof. + intros. change match a :: l with [] => True | a :: l => Forall (R a) l end. + induction H0 as [|? ? ? ? H1]; [trivial|]. + destruct H1; constructor; trivial. + eapply Forall_impl; [|eassumption]. + firstorder. + Qed. + + Lemma Sorted_StronglySorted : + Transitive R -> forall l, Sorted l -> StronglySorted l. + Proof. + induction 2; constructor; trivial. + apply Sorted_extends; trivial. + constructor; trivial. + Qed. + +End defs. + +Hint Constructors HdRel. +Hint Constructors Sorted. + +(* begin hide *) +(* Compatibility with deprecated file Sorting.v *) +Notation lelistA := HdRel (only parsing). +Notation nil_leA := HdRel_nil (only parsing). +Notation cons_leA := HdRel_cons (only parsing). + +Notation sort := Sorted (only parsing). +Notation nil_sort := Sorted_nil (only parsing). +Notation cons_sort := Sorted_cons (only parsing). + +Notation lelistA_inv := HdRel_inv (only parsing). +Notation sort_inv := Sorted_inv (only parsing). +Notation sort_rect := Sorted_rect (only parsing). +(* end hide *) |