From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 theories/Sorting/Sorting.v | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

(limited to 'theories/Sorting/Sorting.v')

diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index f895d79e..aed8cd15 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -6,18 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sorting.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Sorting.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
 
-Require Import List.
-Require Import Multiset.
-Require Import Permutation.
-Require Import Relations.
+Require Import List Multiset Permutation Relations.
 
 Set Implicit Arguments.
 
 Section defs.
 
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : relation A.
   Variable eqA : relation A.
 
@@ -59,6 +56,16 @@ Section defs.
     intros; inversion H; auto with datatypes.
   Qed.
 
+  Lemma sort_rect :
+    forall P:list A -> Type,
+      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.
+
   Lemma sort_rec :
     forall P:list A -> Set,
       P nil ->
@@ -71,7 +78,7 @@ Section defs.
 
   (** * Merging two sorted lists *)
 
-  Inductive merge_lem (l1 l2:list A) : Set :=
+  Inductive merge_lem (l1 l2:list A) : Type :=
     merge_exist :
     forall l:list A,
       sort l ->
@@ -85,7 +92,7 @@ Section defs.
   Proof.
     simple induction 1; intros.
     apply merge_exist with l2; auto with datatypes.
-    elim H3; intros.
+    elim H2; intros.
     apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes.
     elim (leA_dec a a0); intros.
 
@@ -104,7 +111,7 @@ Section defs.
     apply lelistA_inv with l; trivial with datatypes.
 
     (* 2 (leA a0 a) *)
-    elim H5; simpl in |- *; intros.
+    elim X0; simpl in |- *; intros.
     apply merge_exist with (a0 :: l3); simpl in |- *; 
       auto using cons_sort, cons_leA with datatypes.
     apply meq_trans with
-- 
cgit v1.2.3