1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: Lexicographic_Exponentiation.v 9609 2007-02-07 14:42:26Z herbelin $ i*)
11
(** Author: Cristina Cornes
13
From : Constructing Recursion Operators in Type Theory
14
L. Paulson JSC (1986) 2, 325-355 *)
17
Require Import Relation_Operators.
18
Require Import Transitive_Closure.
20
Section Wf_Lexicographic_Exponentiation.
22
Variable leA : A -> A -> Prop.
24
Notation Power := (Pow A leA).
25
Notation Lex_Exp := (lex_exp A leA).
26
Notation ltl := (Ltl A leA).
27
Notation Descl := (Desc A leA).
29
Notation List := (list A).
30
Notation Nil := (nil (A:=A)).
31
(* useless but symmetric *)
32
Notation Cons := (cons (A:=A)).
33
Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
35
(* Hint Resolve d_one d_nil t_step. *)
37
Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z.
41
simpl in |- *; intros H.
43
simpl in |- *; intros; apply (Lt_nil A leA).
48
apply (Lt_hd A leA); auto with sets.
50
apply (HInd y y0); auto with sets.
56
ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z).
58
intros x y; generalize x.
59
elim y; simpl in |- *.
61
exists x0; auto with sets.
64
left; apply (Lt_nil A leA).
65
left; apply (Lt_hd A leA); auto with sets.
66
generalize (H x1 z H3).
68
left; apply (Lt_tl A leA); auto with sets.
70
simple induction 1; intros.
72
right; exists x2; auto with sets.
75
Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
79
generalize (app_cons_not_nil _ _ _ H1); simple induction 1.
80
cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets.
82
generalize (app_eq_unit _ _ H0).
83
simple induction 1; simple induction 1; intros.
84
rewrite H4; auto using d_nil with sets.
86
generalize (app_inj_tail _ _ _ _ H0).
87
simple induction 1; intros.
88
rewrite <- H4; auto with sets.
92
forall (x:List) (a b:A),
93
Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.
100
Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b).
104
cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil);
105
auto with sets; intro.
108
generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4);
112
generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
114
rewrite <- H10; rewrite <- H7; intro.
115
apply (t_step A leA); auto with sets.
119
generalize (app_cons_not_nil _ _ _ H3); intro.
123
generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b);
126
generalize (desc_prefix (Cons b (l ++ Cons x0 Nil)) a H5); intro.
127
generalize (H x0 b H6).
129
apply t_trans with (A := A) (y := x0); auto with sets.
135
generalize (app_inj_tail _ _ _ _ H8); simple induction 1.
137
generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b).
141
generalize (app_inj_tail _ _ _ _ H13); simple induction 1.
143
rewrite <- H11; rewrite <- H16; auto with sets.
148
forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y.
153
cut (x ++ y = Nil); auto with sets; intro.
154
generalize (app_eq_nil _ _ H0); simple induction 1.
156
rewrite H2; rewrite H3; split; apply d_nil.
159
cut (x0 ++ y = Cons x Nil); auto with sets.
161
generalize (app_eq_unit _ _ E); simple induction 1.
162
simple induction 1; intros.
163
rewrite H2; rewrite H3; split.
168
simple induction 1; intros.
169
rewrite H2; rewrite H3; split.
182
(l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 ->
183
Descl x0 /\ Descl y0).
186
generalize (app_nil_end x1); simple induction 1; simple induction 1.
187
split. apply d_conc; auto with sets.
196
forall (x1:A) (x0:List),
197
(l ++ Cons y Nil) ++ Cons x Nil = x0 ++ l0 ++ Cons x1 Nil ->
198
Descl x0 /\ Descl (l0 ++ Cons x1 Nil)).
203
generalize (app_inj_tail _ _ _ _ H2); simple induction 1.
204
simple induction 1; auto with sets.
208
generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)).
210
generalize (app_ass x4 l1 (Cons x2 Nil)); simple induction 1.
212
generalize (app_inj_tail _ _ _ _ E).
213
simple induction 1; intros.
214
generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
215
rewrite <- H7; rewrite <- H10; generalize H6.
216
generalize (app_ass x4 l1 (Cons x2 Nil)); intro E1.
219
generalize (Hind x4 (l1 ++ Cons x2 Nil) H11).
220
simple induction 1; split.
224
rewrite <- H10; intro.
225
apply d_conc; auto with sets.
230
Lemma dist_Desc_concat :
231
forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y.
234
apply (dist_aux (x ++ y) H x y); auto with sets.
238
forall (a b:A) (x:List),
239
Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) ->
240
clos_trans A leA a b.
247
inversion H1; auto with sets.
251
generalize (app_comm_cons l (Cons a Nil) a0).
252
intros E; rewrite <- E; intros.
253
generalize (desc_tail l a a0 H0); intro.
255
apply t_trans with (y := a0); auto with sets.
264
forall (x:List) (a b:A),
265
Descl (x ++ Cons a Nil) ->
266
ltl (x ++ Cons a Nil) (Cons b Nil) -> ltl x (Cons b Nil).
270
intros; apply (Lt_nil A leA).
272
simpl in |- *; intros.
274
apply (Lt_hd A leA a b); auto with sets.
281
forall (x1 x2:List) (y1:Descl (x1 ++ x2)),
282
Acc Lex_Exp << x1 ++ x2, y1 >> ->
283
forall (x:List) (y:Descl x), ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>.
286
apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).
289
unfold lex_exp in |- *; simpl in |- *; auto with sets.
293
Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
295
unfold well_founded at 2 in |- *.
296
simple induction a; intros x y.
299
unfold lex_exp at 1 in |- *; simpl in |- *.
303
forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>).
308
generalize (well_founded_ind (wf_clos_trans A leA H)).
313
(forall (x1:List) (y:Descl x1),
314
ltl x1 l -> Acc Lex_Exp << x1, y >>) ->
315
forall (x1:List) (y:Descl x1),
316
ltl x1 (l ++ Cons x0 Nil) -> Acc Lex_Exp << x1, y >>).
317
intro; intros HInd; intros.
318
generalize (right_prefix x2 l (Cons x1 Nil) H1).
320
intro; apply (H0 x2 y1 H3).
323
intro; simple induction 1.
325
intro; generalize y1; clear y1.
330
forall y1:Descl (l ++ x3),
331
ltl x3 (Cons x1 Nil) -> Acc Lex_Exp << l ++ x3, y1 >>).
333
generalize (app_nil_end l); intros Heq.
340
unfold lex_exp at 1 in |- *.
341
simpl in |- *; intros x4 y3. intros.
342
apply (H0 x4 y3); auto with sets.
345
generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1).
348
generalize (desc_end x4 x1 l0 (conj H8 H5)); intros.
350
rewrite <- (app_ass l l0 (Cons x4 Nil)); intro.
351
generalize (HInd x4 H9 (l ++ l0)); intros HInd2.
352
generalize (ltl_unit l0 x4 x1 H8 H5); intro.
353
generalize (dist_Desc_concat (l ++ l0) (Cons x4 Nil) y2).
354
simple induction 1; intros.
355
generalize (H4 H12 H10); intro.
356
generalize (Acc_inv H14).
357
generalize (acc_app l l0 H12 H14).
359
generalize (HInd2 f); intro.
362
unfold lex_exp at 1 in |- *; simpl in |- *; intros.
363
apply H15; auto with sets.
367
End Wf_Lexicographic_Exponentiation.