aboutsummaryrefslogtreecommitdiff
path: root/theories/Sorting/Sorting.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sorting/Sorting.v')
-rw-r--r--theories/Sorting/Sorting.v144
1 files changed, 75 insertions, 69 deletions
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index cad4e20198..b1986d4e74 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -8,110 +8,116 @@
(*i $Id$ i*)
-Require PolyList.
-Require Multiset.
-Require Permutation.
-Require Relations.
+Require Import List.
+Require Import Multiset.
+Require Import Permutation.
+Require Import Relations.
Set Implicit Arguments.
Section defs.
Variable A : Set.
-Variable leA : (relation A).
-Variable eqA : (relation A).
+Variable leA : relation A.
+Variable eqA : relation A.
-Local gtA := [x,y:A]~(leA x y).
+Let gtA (x y:A) := ~ leA x y.
-Hypothesis leA_dec : (x,y:A){(leA x y)}+{(leA y x)}.
-Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y).
-Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z).
-Hypothesis leA_antisym : (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.
-Hints Resolve leA_refl.
-Hints Immediate eqA_dec leA_dec leA_antisym.
+Hint Resolve leA_refl.
+Hint Immediate eqA_dec leA_dec leA_antisym.
-Local emptyBag := (EmptyBag A).
-Local singletonBag := (SingletonBag eqA_dec).
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
(** [lelistA] *)
-Inductive lelistA [a:A] : (list A) -> Prop :=
- nil_leA : (lelistA a (nil A))
- | cons_leA : (b:A)(l:(list A))(leA a b)->(lelistA a (cons b l)).
-Hint constr_lelistA := Constructors 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).
+Hint Constructors lelistA.
-Lemma lelistA_inv : (a,b:A)(l:(list A))
- (lelistA a (cons b l)) -> (leA a b).
+Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b.
Proof.
- Intros; Inversion H; Trivial with datatypes.
+ intros; inversion H; trivial with datatypes.
Qed.
(** definition for a list to be sorted *)
-Inductive sort : (list A) -> Prop :=
- nil_sort : (sort (nil A))
- | cons_sort : (a:A)(l:(list A))(sort l) -> (lelistA a l) -> (sort (cons a l)).
-Hint constr_sort := Constructors 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 : (a:A)(l:(list A))(sort (cons a l))->(sort l) /\ (lelistA a l).
+Lemma sort_inv :
+ forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l.
Proof.
-Intros; Inversion H; Auto with datatypes.
+intros; inversion H; auto with datatypes.
Qed.
-Lemma sort_rec : (P:(list A)->Set)
- (P (nil A)) ->
- ((a:A)(l:(list A))(sort l)->(P l)->(lelistA a l)->(P (cons a l))) ->
- (y:(list A))(sort y) -> (P y).
+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.
-Induction y; Auto with datatypes.
-Intros; Elim (!sort_inv a l); Auto with datatypes.
+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:(list A);l2:(list A)] : Set :=
- merge_exist : (l:(list A))(sort l) ->
- (meq (list_contents eqA_dec l)
- (munion (list_contents eqA_dec l1) (list_contents eqA_dec l2))) ->
- ((a:A)(lelistA a l1)->(lelistA a l2)->(lelistA a l)) ->
- (merge_lem l1 l2).
-
-Lemma merge : (l1:(list A))(sort l1)->(l2:(list A))(sort l2)->(merge_lem l1 l2).
+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.
- Induction 1; Intros.
- Apply merge_exist with l2; Auto with datatypes.
- Elim H3; Intros.
- Apply merge_exist with (cons a l); Simpl; Auto with datatypes.
- Elim (leA_dec a a0); Intros.
+ 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 (cons a0 l0)); Auto with datatypes.
- Intros (l3, l3sorted, l3contents, Hrec).
- Apply merge_exist with (cons a l3); Simpl; Auto with datatypes.
- Apply meq_trans with (munion (singletonBag a)
- (munion (list_contents eqA_dec l)
- (list_contents eqA_dec (cons 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.
+ 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; Intros.
- Apply merge_exist with (cons a0 l3); Simpl; 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.
+ 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.
End defs.
Unset Implicit Arguments.
-Hint constr_sort : datatypes v62 := Constructors sort.
-Hint constr_lelistA : datatypes v62 := Constructors lelistA.
+Hint Constructors sort: datatypes v62.
+Hint Constructors lelistA: datatypes v62. \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:17:26 +0000