1
(***********************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
4
(* \VV/ *************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(***********************************************************************)
9
(* $Id: SetoidList.v 11800 2009-01-18 18:34:15Z msozeau $ *)
12
Require Export Sorting.
13
Require Export Setoid.
14
Set Implicit Arguments.
15
Unset Strict Implicit.
17
(** * Logical relations over lists with respect to a setoid equality
20
(** This can be seen as a complement of predicate [lelistA] and [sort]
21
found in [Sorting]. *)
23
Section Type_with_equality.
25
Variable eqA : A -> A -> Prop.
27
(** Being in a list modulo an equality relation over type [A]. *)
29
Inductive InA (x : A) : list A -> Prop :=
30
| InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
31
| InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
33
Hint Constructors InA.
35
Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
41
Lemma InA_nil : forall x, InA x nil <-> False.
47
(** An alternative definition of [InA]. *)
49
Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
51
induction l; intuition.
54
inversion H1; firstorder.
55
firstorder; subst; auto.
58
(** A list without redundancy modulo the equality over [A]. *)
60
Inductive NoDupA : list A -> Prop :=
61
| NoDupA_nil : NoDupA nil
62
| NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
64
Hint Constructors NoDupA.
66
(** lists with same elements modulo [eqA] *)
68
Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
70
(** lists with same elements modulo [eqA] at the same place *)
72
Inductive eqlistA : list A -> list A -> Prop :=
73
| eqlistA_nil : eqlistA nil nil
74
| eqlistA_cons : forall x x' l l',
75
eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
77
Hint Constructors eqlistA.
79
(** Compatibility of a boolean function with respect to an equality. *)
81
Definition compat_bool (f : A->bool) := forall x y, eqA x y -> f x = f y.
83
(** Compatibility of a function upon natural numbers. *)
85
Definition compat_nat (f : A->nat) := forall x y, eqA x y -> f x = f y.
87
(** Compatibility of a predicate with respect to an equality. *)
89
Definition compat_P (P : A->Prop) := forall x y, eqA x y -> P x -> P y.
91
(** Results concerning lists modulo [eqA] *)
93
Hypothesis eqA_refl : forall x, eqA x x.
94
Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
95
Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
97
Hint Resolve eqA_refl eqA_trans.
98
Hint Immediate eqA_sym.
100
Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
103
do 2 rewrite InA_alt.
105
exists z; split; eauto.
107
Hint Immediate InA_eqA.
109
Lemma In_InA : forall l x, In x l -> InA x l.
111
simple induction l; simpl in |- *; intuition.
116
Lemma InA_split : forall l x, InA x l ->
117
exists l1, exists y, exists l2,
118
eqA x y /\ l = l1++y::l2.
120
induction l; inversion_clear 1.
121
exists (@nil A); exists a; exists l; auto.
122
destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))).
123
exists (a::l1); exists y; exists l2; auto.
124
split; simpl; f_equal; auto.
127
Lemma InA_app : forall l1 l2 x,
128
InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
130
induction l1; simpl in *; intuition.
131
inversion_clear H; auto.
132
elim (IHl1 l2 x H0); auto.
135
Lemma InA_app_iff : forall l1 l2 x,
136
InA x (l1 ++ l2) <-> InA x l1 \/ InA x l2.
140
destruct 1; generalize H; do 2 rewrite InA_alt.
141
destruct 1 as (y,(H1,H2)); exists y; split; auto.
142
apply in_or_app; auto.
143
destruct 1 as (y,(H1,H2)); exists y; split; auto.
144
apply in_or_app; auto.
147
Lemma InA_rev : forall p m,
148
InA p (rev m) <-> InA p m.
150
intros; do 2 rewrite InA_alt.
151
split; intros (y,H); exists y; intuition.
152
rewrite In_rev; auto.
153
rewrite <- In_rev; auto.
156
(** Results concerning lists modulo [eqA] and [ltA] *)
158
Variable ltA : A -> A -> Prop.
160
Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z.
161
Hypothesis ltA_not_eqA : forall x y, ltA x y -> ~ eqA x y.
162
Hypothesis ltA_eqA : forall x y z, ltA x y -> eqA y z -> ltA x z.
163
Hypothesis eqA_ltA : forall x y z, eqA x y -> ltA y z -> ltA x z.
165
Hint Resolve ltA_trans.
166
Hint Immediate ltA_eqA eqA_ltA.
168
Notation InfA:=(lelistA ltA).
169
Notation SortA:=(sort ltA).
171
Hint Constructors lelistA sort.
174
forall l x y, ltA x y -> InfA y l -> InfA x l.
176
destruct l; constructor; inversion_clear H0;
177
eapply ltA_trans; eauto.
181
forall l x y, eqA x y -> InfA y l -> InfA x l.
183
intro s; case s; constructor; inversion_clear H0; eauto.
185
Hint Immediate InfA_ltA InfA_eqA.
187
Lemma SortA_InfA_InA :
188
forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
191
intros; inversion H1.
193
inversion_clear H0; inversion_clear H1; inversion_clear H2.
194
eapply ltA_eqA; eauto.
199
forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
201
simple induction l; simpl in |- *; intros; constructor; auto.
205
forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
207
simple induction l; simpl in |- *; intros; constructor; auto.
210
(* In fact, this may be used as an alternative definition for InfA: *)
213
forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
216
intros; eapply SortA_InfA_InA; eauto.
220
Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
222
induction l1; simpl; auto.
223
inversion_clear 1; auto.
227
forall l1 l2, SortA l1 -> SortA l2 ->
228
(forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
231
induction l1; simpl in *; intuition.
234
apply InfA_app; auto.
240
Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
242
simple induction l; auto.
247
assert (ltA x x) by (eapply SortA_InfA_InA; eauto).
248
elim (ltA_not_eqA H3); auto.
251
Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->
252
(forall x, InA x l -> InA x l' -> False) ->
255
induction l; simpl; auto; intros.
258
rewrite InA_alt; intros (y,(H4,H5)).
259
destruct (in_app_or _ _ _ H5).
272
Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
278
apply NoDupA_app; auto.
280
intro H2; inversion H2.
286
apply InA_eqA with x1; eauto.
288
rewrite In_rev; auto.
292
Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
294
induction l; simpl in *; inversion_clear 1; auto.
297
rewrite InA_app_iff in *; rewrite InA_cons; intuition.
300
Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
302
induction l; simpl in *; inversion_clear 1; auto.
304
assert (H2:=IHl _ _ H1).
309
rewrite InA_app_iff in *; rewrite InA_cons; auto.
313
rewrite InA_app_iff in *; rewrite InA_cons; intuition.
314
eapply NoDupA_split; eauto.
319
(** Some results about [eqlistA] *)
323
Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
325
induction 1; auto; simpl; congruence.
328
Lemma eqlistA_app : forall l1 l1' l2 l2',
329
eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
331
intros l1 l1' l2 l2' H; revert l2 l2'; induction H; simpl; auto.
334
Lemma eqlistA_rev_app : forall l1 l1',
335
eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
336
eqlistA ((rev l1)++l2) ((rev l1')++l2').
340
do 2 rewrite app_ass; simpl; auto.
343
Lemma eqlistA_rev : forall l1 l1',
344
eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
347
rewrite (app_nil_end (rev l1)).
348
rewrite (app_nil_end (rev l1')).
349
apply eqlistA_rev_app; auto.
352
Lemma SortA_equivlistA_eqlistA : forall l l',
353
SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
355
induction l; destruct l'; simpl; intros; auto.
356
destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.
357
destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.
358
inversion_clear H; inversion_clear H0.
359
assert (forall y, InA y l -> ltA a y).
360
intros; eapply SortA_InfA_InA with (l:=l); eauto.
361
assert (forall y, InA y l' -> ltA a0 y).
362
intros; eapply SortA_InfA_InA with (l:=l'); eauto.
367
assert (InA a (a0::l')) by auto.
368
inversion_clear H8; auto.
369
assert (InA a0 (a::l)) by auto.
370
inversion_clear H8; auto.
371
elim (@ltA_not_eqA a a); auto.
372
apply ltA_trans with a0; auto.
377
assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto.
378
elim (@ltA_not_eqA a x); eauto.
380
assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto.
381
elim (@ltA_not_eqA a0 x); eauto.
386
(** A few things about [filter] *)
390
Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
392
induction l; simpl; auto.
393
inversion_clear 1; auto.
394
destruct (f a); auto.
398
rewrite filter_In in H; destruct H.
399
eapply SortA_InfA_InA; eauto.
402
Lemma filter_InA : forall f, (compat_bool f) ->
403
forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
405
intros; do 2 rewrite InA_alt; intuition.
406
destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
407
destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
408
rewrite (H _ _ H0); auto.
409
destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
410
rewrite <- (H _ _ H0); auto.
414
forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
415
forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
417
induction l; simpl; intros; auto.
419
pattern l at 1; rewrite IHl; auto.
420
case_eq (f a); simpl; intros; auto.
421
assert (forall e, In e l -> f e = false).
423
assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
424
case_eq (f e); simpl; intros; auto.
425
elim (@ltA_not_eqA e e); auto.
426
apply ltA_trans with a; eauto.
427
replace (List.filter f l) with (@nil A); auto.
428
generalize H3; clear; induction l; simpl; auto.
429
case_eq (f a); auto; intros.
430
rewrite H3 in H; auto; try discriminate.
438
Variable eqB:B->B->Prop.
440
(** Compatibility of a two-argument function with respect to two equalities. *)
441
Definition compat_op (f : A -> B -> B) :=
442
forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
444
(** Two-argument functions that allow to reorder their arguments. *)
445
Definition transpose (f : A -> B -> B) :=
446
forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
448
(** A version of transpose with restriction on where it should hold *)
449
Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
450
forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
452
Variable st:Equivalence eqB.
455
Variable Comp:compat_op f.
457
Lemma fold_right_eqlistA :
458
forall s s', eqlistA s s' ->
459
eqB (fold_right f i s) (fold_right f i s').
461
induction 1; simpl; auto.
465
Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y ->
466
NoDupA (x::l) -> NoDupA (l1++y::l2) ->
467
equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
471
repeat rewrite InA_app_iff.
472
do 2 rewrite InA_cons.
474
assert (SW:=NoDupA_swap H1).
476
rewrite InA_app_iff in H0.
479
contradict H3; apply InA_eqA with a; auto.
481
contradict H8; eauto.
483
assert (eqA a x \/ InA a l) by intuition.
486
destruct H7; [left|right]; eapply InA_eqA; eauto.
489
(** [ForallList2] : specifies that a certain binary predicate should
490
always hold when inspecting two different elements of the list. *)
492
Inductive ForallList2 (R : A -> A -> Prop) : list A -> Prop :=
493
| ForallNil : ForallList2 R nil
494
| ForallCons : forall a l,
495
(forall b, In b l -> R a b) ->
496
ForallList2 R l -> ForallList2 R (a::l).
497
Hint Constructors ForallList2.
499
(** [NoDupA] can be written in terms of [ForallList2] *)
501
Lemma ForallList2_NoDupA : forall l,
502
ForallList2 (fun a b => ~eqA a b) l <-> NoDupA l.
504
induction l; split; intros; auto.
505
inversion_clear H. constructor; [ | rewrite <- IHl; auto ].
506
rewrite InA_alt; intros (a',(Haa',Ha')).
507
exact (H0 a' Ha' Haa').
508
inversion_clear H. constructor; [ | rewrite IHl; auto ].
511
rewrite InA_alt; exists b; auto.
514
Lemma ForallList2_impl : forall (R R':A->A->Prop),
515
(forall a b, R a b -> R' a b) ->
516
forall l, ForallList2 R l -> ForallList2 R' l.
521
(** The following definition is easier to use than [ForallList2]. *)
523
Definition ForallList2_alt (R:A->A->Prop) l :=
524
forall a b, InA a l -> InA b l -> ~eqA a b -> R a b.
527
Variable R : A -> A -> Prop.
529
(** [ForallList2] and [ForallList2_alt] are related, but no completely
530
equivalent. For proving one implication, we need to know that the
531
list has no duplicated elements... *)
533
Lemma ForallList2_equiv1 : forall l, NoDupA l ->
534
ForallList2_alt R l -> ForallList2 R l.
537
constructor. intros b Hb.
541
apply InA_eqA with b; auto.
543
inversion_clear H; auto.
544
intros b c Hb Hc Hneq.
548
(** ... and for proving the other implication, we need to be able
549
to reverse and adapt relation [R] modulo [eqA]. *)
551
Hypothesis R_sym : forall a b, R a b -> R b a.
552
Hypothesis R_compat : forall a, compat_P (R a).
554
Lemma ForallList2_equiv2 : forall l,
555
ForallList2 R l -> ForallList2_alt R l.
558
intros _. red. intros a b Ha. inversion Ha.
559
inversion_clear 1 as [|? ? H_R Hl].
560
intros b c Hb Hc Hneq.
561
inversion_clear Hb; inversion_clear Hc.
562
(* b,c = a : impossible *)
565
rewrite InA_alt in H0; destruct H0 as (d,(Hcd,Hd)).
566
apply R_compat with d; auto.
567
apply R_sym; apply R_compat with a; auto.
569
rewrite InA_alt in H; destruct H as (d,(Hcd,Hd)).
570
apply R_compat with a; auto.
571
apply R_sym; apply R_compat with d; auto.
573
apply (IHl Hl); auto.
576
Lemma ForallList2_equiv : forall l, NoDupA l ->
577
(ForallList2 R l <-> ForallList2_alt R l).
579
split; [apply ForallList2_equiv2|apply ForallList2_equiv1]; auto.
582
Lemma ForallList2_equivlistA : forall l l', NoDupA l' ->
583
equivlistA l l' -> ForallList2 R l -> ForallList2 R l'.
586
apply ForallList2_equiv1; auto.
587
intros a b Ha Hb Hneq.
588
red in H0; rewrite <- H0 in Ha,Hb.
589
revert a b Ha Hb Hneq.
590
change (ForallList2_alt R l).
591
apply ForallList2_equiv2; auto.
594
Variable TraR :transpose_restr R f.
596
Lemma fold_right_commutes_restr :
597
forall s1 s2 x, ForallList2 R (s1++x::s2) ->
598
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
600
induction s1; simpl; auto; intros.
602
transitivity (f a (f x (fold_right f i (s1++s2)))).
605
inversion_clear H; auto.
609
apply in_or_app; simpl; auto.
612
Lemma fold_right_equivlistA_restr :
613
forall s s', NoDupA s -> NoDupA s' -> ForallList2 R s ->
614
equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
619
unfold equivlistA; intros.
621
assert (X : InA a nil); auto; inversion X.
622
intros x l Hrec s' N N' F E; simpl in *.
624
rewrite <- (E x); auto.
625
destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
627
transitivity (f x (fold_right f i (s1++s2))).
630
inversion_clear N; auto.
631
eapply NoDupA_split; eauto.
632
inversion_clear F; auto.
633
eapply equivlistA_NoDupA_split; eauto.
634
transitivity (f y (fold_right f i (s1++s2))).
635
apply Comp; auto. reflexivity.
636
symmetry; apply fold_right_commutes_restr.
637
apply ForallList2_equivlistA with (x::l); auto.
640
Lemma fold_right_add_restr :
641
forall s' s x, NoDupA s -> NoDupA s' -> ForallList2 R s' -> ~ InA x s ->
642
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
644
intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
649
(** we know state similar results, but without restriction on transpose. *)
651
Variable Tra :transpose f.
653
Lemma fold_right_commutes : forall s1 s2 x,
654
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
656
induction s1; simpl; auto; intros.
658
transitivity (f a (f x (fold_right f i (s1++s2)))); auto.
661
Lemma fold_right_equivlistA :
662
forall s s', NoDupA s -> NoDupA s' ->
663
equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
665
intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True);
667
apply ForallList2_equiv1; try red; auto.
670
Lemma fold_right_add :
671
forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
672
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
674
intros; apply (@fold_right_equivlistA s' (x::s)); auto.
679
Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
681
Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
686
destruct (eqA_dec x a).
690
right; red; inversion_clear 1; contradiction.
693
Fixpoint removeA (x : A) (l : list A){struct l} : list A :=
696
| y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
699
Lemma removeA_filter : forall x l,
700
removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
702
induction l; simpl; auto.
703
destruct (eqA_dec x a); auto.
707
Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
709
induction l; simpl; auto.
712
destruct 1; inversion_clear H.
714
destruct (eqA_dec x a); simpl; auto.
715
rewrite IHl; split; destruct 1; split; auto.
716
inversion_clear H; auto.
717
destruct H0; apply eqA_trans with a; auto.
722
apply eqA_trans with y; auto.
723
rewrite (IHl x y) in H0; destruct H0; auto.
724
destruct 1; inversion_clear H; auto.
725
constructor 2; rewrite IHl; auto.
728
Lemma removeA_NoDupA :
729
forall s x, NoDupA s -> NoDupA (removeA x s).
731
simple induction s; simpl; intros.
734
destruct (eqA_dec x a); simpl; auto.
740
Lemma removeA_equivlistA : forall l l' x,
741
~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
743
unfold equivlistA; intros.
746
rewrite <- H0; split; auto.
748
apply InA_eqA with x0; auto.
749
rewrite <- (H0 x0) in H1.
751
inversion_clear H1; auto.
759
End Type_with_equality.
761
Hint Unfold compat_bool compat_nat compat_P.
762
Hint Constructors InA NoDupA sort lelistA eqlistA.
766
Variable eqA : A -> A -> Prop.
767
Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
768
Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
769
Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
771
Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B :=
774
| (a,b)::l => if f a then Some b else findA f l
779
NoDupA (fun p p' => eqA (fst p) (fst p')) l ->
780
(InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <->
781
findA (fun a' => if eqA_dec a a' then true else false) l = Some b).
783
induction l; simpl; intros.
784
split; intros; try discriminate.
786
destruct a as (a',b'); rename a0 into a.
790
simpl in *; destruct H2; subst b'.
791
destruct (eqA_dec a a'); intuition.
792
destruct (eqA_dec a a'); simpl.
794
generalize e H2 eqA_trans eqA_sym; clear.
797
inversion_clear 2; intros; auto.
799
compute in H; destruct H.
803
apply eqA_trans with a; auto.
804
rewrite <- IHl; auto.
805
destruct (eqA_dec a a'); simpl in *.
806
inversion H; clear H; intros; subst b'; auto.
added
removed
theories/Lists/SetoidList.v
