summaryrefslogtreecommitdiff
path: root/theories/Sorting/Sorting.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sorting/Sorting.v')
-rw-r--r--theories/Sorting/Sorting.v180
1 files changed, 90 insertions, 90 deletions
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 0e0bfe8f..f895d79e 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Sorting.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Sorting.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Import List.
Require Import Multiset.
@@ -17,107 +17,107 @@ Set Implicit Arguments.
Section defs.
-Variable A : Set.
-Variable leA : relation A.
-Variable eqA : relation A.
+ Variable A : Set.
+ Variable leA : relation A.
+ Variable eqA : relation A.
-Let gtA (x y:A) := ~ leA x y.
+ Let gtA (x y:A) := ~ leA x y.
+
+ Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
+ Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+ Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
+ Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
+ Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
-Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
-Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
-Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
-Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
+ Hint Resolve leA_refl.
+ Hint Immediate eqA_dec leA_dec leA_antisym.
-Hint Resolve leA_refl.
-Hint Immediate eqA_dec leA_dec leA_antisym.
+ Let emptyBag := EmptyBag A.
+ Let singletonBag := SingletonBag _ eqA_dec.
-Let emptyBag := EmptyBag A.
-Let singletonBag := SingletonBag _ eqA_dec.
+ (** [lelistA] *)
-(** [lelistA] *)
+ Inductive lelistA (a:A) : list A -> Prop :=
+ | nil_leA : lelistA a nil
+ | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l).
-Inductive lelistA (a:A) : list A -> Prop :=
- | nil_leA : lelistA a nil
- | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l).
-Hint Constructors lelistA.
+ Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b.
+ Proof.
+ intros; inversion H; trivial with datatypes.
+ Qed.
-Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b.
-Proof.
- intros; inversion H; trivial with datatypes.
-Qed.
+ (** * Definition for a list to be sorted *)
-(** definition for a list to be sorted *)
-
-Inductive sort : list A -> Prop :=
- | nil_sort : sort nil
- | cons_sort :
+ Inductive sort : list A -> Prop :=
+ | nil_sort : sort nil
+ | cons_sort :
forall (a:A) (l:list A), sort l -> lelistA a l -> sort (a :: l).
-Hint Constructors sort.
-
-Lemma sort_inv :
- forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l.
-Proof.
-intros; inversion H; auto with datatypes.
-Qed.
-
-Lemma sort_rec :
- forall P:list A -> Set,
- P nil ->
- (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->
- forall y:list A, sort y -> P y.
-Proof.
-simple induction y; auto with datatypes.
-intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes.
-Qed.
-
-(** merging two sorted lists *)
-
-Inductive merge_lem (l1 l2:list A) : Set :=
+
+ Lemma sort_inv :
+ forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l.
+ Proof.
+ intros; inversion H; auto with datatypes.
+ Qed.
+
+ Lemma sort_rec :
+ forall P:list A -> Set,
+ P nil ->
+ (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->
+ forall y:list A, sort y -> P y.
+ Proof.
+ simple induction y; auto with datatypes.
+ intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes.
+ Qed.
+
+ (** * Merging two sorted lists *)
+
+ Inductive merge_lem (l1 l2:list A) : Set :=
merge_exist :
- forall l:list A,
- sort l ->
- meq (list_contents _ eqA_dec l)
- (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
- (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) ->
- merge_lem l1 l2.
-
-Lemma merge :
- forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2.
-Proof.
- simple induction 1; intros.
- apply merge_exist with l2; auto with datatypes.
- elim H3; intros.
- apply merge_exist with (a :: l); simpl in |- *; auto with datatypes.
- elim (leA_dec a a0); intros.
-
-(* 1 (leA a a0) *)
- cut (merge_lem l (a0 :: l0)); auto with datatypes.
- intros [l3 l3sorted l3contents Hrec].
- apply merge_exist with (a :: l3); simpl in |- *; auto with datatypes.
- apply meq_trans with
- (munion (singletonBag a)
- (munion (list_contents _ eqA_dec l)
- (list_contents _ eqA_dec (a0 :: l0)))).
- apply meq_right; trivial with datatypes.
- apply meq_sym; apply munion_ass.
- intros; apply cons_leA.
- apply lelistA_inv with l; trivial with datatypes.
-
-(* 2 (leA a0 a) *)
- elim H5; simpl in |- *; intros.
- apply merge_exist with (a0 :: l3); simpl in |- *; auto with datatypes.
- apply meq_trans with
- (munion (singletonBag a0)
- (munion (munion (singletonBag a) (list_contents _ eqA_dec l))
- (list_contents _ eqA_dec l0))).
- apply meq_right; trivial with datatypes.
- apply munion_perm_left.
- intros; apply cons_leA; apply lelistA_inv with l0; trivial with datatypes.
-Qed.
+ forall l:list A,
+ sort l ->
+ meq (list_contents _ eqA_dec l)
+ (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
+ (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) ->
+ merge_lem l1 l2.
+
+ Lemma merge :
+ forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2.
+ Proof.
+ simple induction 1; intros.
+ apply merge_exist with l2; auto with datatypes.
+ elim H3; intros.
+ apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes.
+ elim (leA_dec a a0); intros.
+
+ (* 1 (leA a a0) *)
+ cut (merge_lem l (a0 :: l0)); auto using cons_sort with datatypes.
+ intros [l3 l3sorted l3contents Hrec].
+ apply merge_exist with (a :: l3); simpl in |- *;
+ auto using cons_sort, cons_leA with datatypes.
+ apply meq_trans with
+ (munion (singletonBag a)
+ (munion (list_contents _ eqA_dec l)
+ (list_contents _ eqA_dec (a0 :: l0)))).
+ apply meq_right; trivial with datatypes.
+ apply meq_sym; apply munion_ass.
+ intros; apply cons_leA.
+ apply lelistA_inv with l; trivial with datatypes.
+
+ (* 2 (leA a0 a) *)
+ elim H5; simpl in |- *; intros.
+ apply merge_exist with (a0 :: l3); simpl in |- *;
+ auto using cons_sort, cons_leA with datatypes.
+ apply meq_trans with
+ (munion (singletonBag a0)
+ (munion (munion (singletonBag a) (list_contents _ eqA_dec l))
+ (list_contents _ eqA_dec l0))).
+ apply meq_right; trivial with datatypes.
+ apply munion_perm_left.
+ intros; apply cons_leA; apply lelistA_inv with l0; trivial with datatypes.
+ Qed.
End defs.
Unset Implicit Arguments.
Hint Constructors sort: datatypes v62.
-Hint Constructors lelistA: datatypes v62. \ No newline at end of file
+Hint Constructors lelistA: datatypes v62.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 06:40:18 +0000