blob: 60145cf04783f007f97367fe125eb0356678e47e (
plain)
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
|
Require Import FSets.
Set Implicit Arguments.
(* Useful properties over finite sets and ordered types *)
Module MyOTFacts (M : OrderedType).
Section compat.
Lemma compat_not_compat : forall f : M.t -> bool,
compat_bool M.eq f ->
compat_bool M.eq (fun x => negb (f x)).
Proof.
unfold compat_bool;intros f H.
intros; unfold negb.
rewrite (H x y H0);reflexivity.
Qed.
End compat.
End MyOTFacts.
Module MyFacts (M : S).
Import M.
Module Import Props := Properties M.
Module Import Facts := OrderedTypeFacts E.
Module Import OTFacts := MyOTFacts E.
Lemma set_induction2 : forall s,
Empty s \/ exists x, exists s', Add x s' s.
Proof.
intros. case_eq (choose s);intros.
right. exists e. exists (remove e s).
constructor;intro H0.
destruct (eq_dec e y).
left;assumption.
right;apply (remove_2 n H0).
destruct H0.
rewrite <-H0;apply (choose_1 H).
eapply remove_3;eassumption.
left;apply (choose_2 H).
Qed.
Lemma equal_equivlist : forall s s',
Equal s s' -> equivlistA E.eq (elements s) (elements s').
Proof.
unfold equivlistA.
generalize elements_1;generalize elements_2;intros H0 H1 s s' H x.
split;intro H2.
apply H1;rewrite <-H;apply H0;assumption.
apply H1;rewrite H;apply H0;assumption.
Qed.
Section Fold_Facts.
Variable A : Type.
Lemma fold_left_compat_set : forall (f : t -> A -> t) l e e',
Equal e e' ->
(forall e1 e2 a, Equal e1 e2 -> Equal (f e1 a) (f e2 a)) ->
Equal (fold_left f l e) (fold_left f l e').
Proof.
intros f l.
induction l;simpl.
auto.
intros e e' H H0 H1.
apply (IHl (f e a) (f e' a)).
apply H0;assumption.
assumption.
Qed.
Lemma fold_left_assoc : forall l f x h,
(forall (y z : A) s, Equal (f (f s y) z) (f (f s z) y)) ->
(forall e1 e2 a, Equal e1 e2 -> Equal (f e1 a) (f e2 a)) ->
Equal (fold_left f (h :: l) x) (f (fold_left f l x) h).
Proof.
induction l;simpl;intros f x h H H0.
intuition.
rewrite <-IHl;simpl;try assumption.
apply fold_left_compat_set;[apply H|];auto.
Qed.
Lemma NoDupA_elements : forall s,
NoDupA E.eq (elements s).
Proof.
intro s.
apply SortA_NoDupA with (ltA := E.lt).
apply E.eq_refl.
apply E.eq_sym.
apply E.lt_trans.
apply E.lt_not_eq.
apply Facts.lt_eq.
apply Facts.eq_lt.
apply elements_3.
Qed.
End Fold_Facts.
End MyFacts.
|
