blob: 292b1c0e4d39c6ddbbe20983c55776f1ece41934 (
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
|
Require Import List.
Require Import InterfGraphMapImp.
Section fold_assoc_interf_map.
Variable A : Type.
Inductive eq_set_option : option VertexSet.t -> option VertexSet.t -> Prop :=
|None_eq : eq_set_option None None
|Some_eq : forall s s', VertexSet.Equal s s' -> eq_set_option (Some s) (Some s').
Definition EqualSetMap m1 m2 := forall x, eq_set_option (VertexMap.find x m1) (VertexMap.find x m2).
Lemma EqualSetMap_refl : forall m, EqualSetMap m m.
Proof.
unfold EqualSetMap. intro m. intro x.
destruct (VertexMap.find x m).
constructor. intuition.
constructor.
Qed.
Lemma EqualSetMap_trans : forall m1 m2 m3,
EqualSetMap m1 m2 ->
EqualSetMap m2 m3 ->
EqualSetMap m1 m3.
Proof.
intros m1 m2 m3 H H0.
unfold EqualSetMap in *.
intro x.
generalize (H x). clear H. intro H.
generalize (H0 x). clear H0. intro H0.
destruct (VertexMap.find x m1).
inversion H. subst.
rewrite <-H2 in H0.
destruct (VertexMap.find x m3).
constructor. inversion H0. subst.
rewrite H3. assumption.
inversion H0.
destruct (VertexMap.find x m3).
inversion H0. inversion H. subst. rewrite <-H4 in H1. inversion H1.
constructor.
Qed.
Lemma fold_left_compat_map : forall (f : VertexMap.t VertexSet.t -> A -> VertexMap.t VertexSet.t) l e e',
EqualSetMap e e' ->
(forall e1 e2 a, EqualSetMap e1 e2 -> EqualSetMap (f e1 a) (f e2 a)) ->
EqualSetMap (fold_left f l e) (fold_left f l e').
Proof.
intro f;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_map : forall l (f : VertexMap.t VertexSet.t -> A -> VertexMap.t VertexSet.t) x h,
(forall (y z : A) s, EqualSetMap (f (f s y) z) (f (f s z) y)) ->
(forall e1 e2 a, EqualSetMap e1 e2 -> EqualSetMap (f e1 a) (f e2 a)) ->
EqualSetMap (fold_left f (h :: l) x) (f (fold_left f l x) h).
Proof.
induction l;simpl;intros f x h H H0.
apply EqualSetMap_refl.
apply EqualSetMap_trans with (m2 := fold_left f (h :: l) (f x a)).
simpl. apply fold_left_compat_map. apply H.
assumption.
apply IHl. assumption. assumption.
Qed.
(*
Add Morphism EqualSetMap : equalsetmap_m.
Proof.
unfold EqualSetMap, VertexMap.Equal. split; intros.
rewrite <-(H0 x1). rewrite <-(H x1). apply H1.
rewrite (H0 x1). rewrite (H x1). apply H1.
Qed.
*)
End fold_assoc_interf_map.
|
