-
Notifications
You must be signed in to change notification settings - Fork 0
/
merge.v
232 lines (207 loc) · 8.03 KB
/
merge.v
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
Require Import List Permutation Arith Lia Extraction.
Require Import measure_ind list_utils perm_utils sorted.
Set Implicit Arguments.
Section merge.
Variable (X : Type) (R : X -> X -> Prop)
(cmp : forall x y, { R x y } + { R y x })
(Rtran : forall x y z, R x y -> R y z -> R x z).
Definition merge l m : sorted R l -> sorted R m -> { k | k ~p l++m /\ sorted R k }.
Proof.
induction on l m as merge with measure (length l+length m); intros Hl Hm.
refine (match l as l' return l = l' -> _ with
| nil => fun El => exist _ m _
| x::l' => fun El =>
match m as m' return m = m' -> _ with
| nil => fun Em => exist _ l _
| y::m' => fun Em =>
match cmp x y with
| left H => let (k,G) := merge l' m _ _ _ in exist _ (x::k) _
| right H => let (k,G) := merge l m' _ _ _ in exist _ (y::k) _
end
end eq_refl
end eq_refl); auto.
1-3,5-6: cycle 1.
1-3: cycle 2.
1-2: subst; simpl; lia.
+ revert Hl; subst; apply sorted_inv_sorted; auto.
+ subst; rewrite sorted_cons in Hm; tauto.
+ rewrite <- app_nil_end; subst; simpl; auto.
+ destruct G as [ G1 G2 ]; split.
* simpl; apply perm_cons; subst; auto.
* apply sorted_cons; auto; split; auto.
apply perm_incl in G1.
apply lb_incl with (1 := G1), lb_app.
subst.
rewrite sorted_cons in Hl; auto.
rewrite sorted_cons in Hm; auto.
rewrite lb_cons.
repeat split; try tauto.
apply proj2 in Hm.
revert Hm; apply lb_mono; auto.
+ destruct G as [ G1 G2 ]; split.
* simpl.
apply perm_trans with (1 := perm_cons _ G1); subst; simpl.
apply perm_trans with (1 := perm_swap _ _ _), perm_cons.
apply Permutation_middle.
* apply sorted_cons; auto; split; auto.
apply perm_incl in G1.
apply lb_incl with (1 := G1), lb_app.
subst.
rewrite sorted_cons in Hl; auto.
rewrite sorted_cons in Hm; auto.
rewrite lb_cons.
repeat split; try tauto.
apply proj2 in Hl.
revert Hl; apply lb_mono; auto.
Defined.
End merge.
Extract Inductive prod => "(*)" [ "(,)" ].
Extract Inductive list => "list" [ "[]" "(::)" ].
Extraction merge.
Section rev_tail.
Variable (X : Type).
Fixpoint rev_tail (a l : list X) : { m | m = rev l ++ a }.
Proof.
refine (match l with
| nil => exist _ a _
| x::l' => let (r,Hr) := rev_tail (x::a) l' in exist _ r _
end); auto.
simpl; rewrite app_ass; auto.
Defined.
End rev_tail.
Section merge_tail.
Variable (X : Type) (R : X -> X -> Prop)
(cmp : forall x y, { R x y } + { R y x })
(Rtran : forall x y z, R x y -> R y z -> R x z).
(* let merge_tail cmp l m :=
let rec loop a l m :=
match l,m with
| nil, _ => rev_tail a m
| _::_, nil => rev_tail a l
| x::l', y::m' => let (z,l1,m1) = if cmp x y then (x,l',m) else (y,l,m')
in loop (z::a) l1 m1
in rev_tail nil (loop nil l m) *)
Local Definition mt_loop l m : forall a,
sorted R (rev a)
-> lu R a (l++m)
-> sorted R l
-> sorted R m
-> { k | k ~p l++m++a /\ sorted R (rev k) }.
Proof.
induction on l m as loop with measure (length l+length m); intros a Ha1 Ha2 Hl Hm.
refine (match l as l' return l = l' -> _ with
| nil => fun El => let (k,Hk) := rev_tail a m in exist _ k _
| x::l' => fun El =>
match m as m' return m = m' -> _ with
| nil => fun Em => let (k,Hk) := rev_tail a l in exist _ k _
| y::m' => fun Em =>
let c := match cmp x y with
| left H => (x,l',m)
| right H => (y,l,m')
end in match c as c' return c = c' -> _ with (z,l1,m1) => fun Ec =>
let (k,G) := loop l1 m1 _ (z::a) _ _ _ _
in exist _ k _
end eq_refl
end eq_refl
end eq_refl); auto.
1-3 : cycle 2.
+ unfold c in Ec.
destruct (cmp x y); inversion Ec; subst; simpl; lia.
+ split; subst k; simpl.
* apply Permutation_app; auto.
apply Permutation_sym, Permutation_rev.
* rewrite rev_app_distr, rev_involutive.
apply sorted_app; auto.
repeat split; auto.
apply Forall_rev; subst; auto.
+ split.
* rewrite Hk, <- El; simpl.
apply Permutation_app; auto.
apply Permutation_sym, Permutation_rev.
* rewrite Hk, rev_app_distr, rev_involutive.
apply sorted_app; auto.
repeat split; auto.
subst m; rewrite <- app_nil_end in Ha2.
apply Forall_rev; auto.
+ unfold c in Ec.
destruct (cmp x y); inversion Ec; subst z l1 m1; simpl;
apply sorted_app; auto; repeat split; auto.
* apply Forall_rev, lu_spec.
rewrite lu_spec, El in Ha2.
intros u v Hu [ Hv | [] ]; subst v.
apply Ha2; simpl; auto.
* apply Forall_rev, lu_spec.
rewrite lu_spec, Em in Ha2.
intros u v Hu [ Hv | [] ]; subst v.
apply Ha2; simpl; auto.
apply in_or_app; right; simpl; auto.
+ unfold c in Ec.
destruct (cmp x y); inversion Ec; subst z l1 m1; simpl; auto.
* apply lu_cons_l.
- revert Ha2; apply lu_incl; auto.
++ apply incl_refl.
++ rewrite El; simpl; apply incl_tl, incl_refl.
- rewrite Em, sorted_cons in Hm; auto.
destruct Hm as [ Hm1 Hm2 ].
rewrite El, sorted_cons in Hl; auto.
destruct Hl as [ Hl1 Hl2 ].
apply lb_app; split; auto.
rewrite Em; apply lb_cons; split; auto.
revert Hm2; apply lb_mono; auto.
* apply lu_cons_l.
- revert Ha2; apply lu_incl; auto.
++ apply incl_refl.
++ rewrite Em; simpl.
apply incl_app.
** apply incl_appl, incl_refl.
** apply incl_appr, incl_tl, incl_refl.
- rewrite Em, sorted_cons in Hm; auto.
destruct Hm as [ Hm1 Hm2 ].
rewrite El, sorted_cons in Hl; auto.
destruct Hl as [ Hl1 Hl2 ].
apply lb_app; split; auto.
rewrite El; apply lb_cons; split; auto.
revert Hl2; apply lb_mono; auto.
+ unfold c in Ec.
destruct (cmp x y); inversion Ec; subst z l1 m1; simpl; auto.
subst l; apply sorted_cons in Hl; tauto.
+ unfold c in Ec.
destruct (cmp x y); inversion Ec; subst z l1 m1; simpl; auto.
subst m; apply sorted_cons in Hm; tauto.
+ destruct G as [ G1 G2 ]; split; auto.
unfold c in Ec.
destruct (cmp x y); inversion Ec; subst z l1 m1; simpl.
* apply perm_trans with (1 := G1), Permutation_sym.
rewrite (app_assoc l' m), Em.
apply perm_trans with (2 := perm_middle _ _ _).
repeat rewrite app_ass; auto.
* apply perm_trans with (1 := G1), Permutation_sym.
rewrite El; simpl.
apply perm_cons, Permutation_app; auto.
Qed.
Extraction Inline mt_loop.
Definition merge_tail l m : sorted R l -> sorted R m -> { k | k ~p l++m /\ sorted R k }.
Proof.
intros Hl Hm.
refine (let (k,Hk) := @mt_loop _ _ nil _ _ Hl Hm in
let (r,Hr) := rev_tail nil k
in exist _ r _).
+ simpl; auto.
+ apply lu_nil_l.
+ rewrite <- app_nil_end in *.
subst.
destruct Hk as [ Hk ? ]; split; auto.
apply perm_trans with (2 := Hk), perm_sym.
apply Permutation_rev.
Defined.
End merge_tail.
Extract Inductive sumbool => "bool" [ "true" "false" ].
Recursive Extraction merge_tail.