1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
(************************************************************************)
(* 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: Sorting.v 9245 2006-10-17 12:53:34Z notin $ i*)
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.
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.
Hint Resolve leA_refl.
Hint Immediate eqA_dec leA_dec leA_antisym.
Let emptyBag := EmptyBag A.
Let singletonBag := SingletonBag _ eqA_dec.
(** [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).
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 *)
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).
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 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.
|
