-
Notifications
You must be signed in to change notification settings - Fork 0
/
Labels.v
164 lines (135 loc) · 4.14 KB
/
Labels.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
Require Import ZArith.
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.
Require Import Utils.
Class JoinSemiLattice (Lab : Type) :=
{ bot : Lab
; join : Lab -> Lab -> Lab
; flows : Lab -> Lab -> bool
; meet : Lab -> Lab -> Lab
; bot_flows : forall l, flows bot l = true
; flows_refl : forall l, flows l l = true
; flows_trans : forall l1 l2 l3, flows l1 l2 = true ->
flows l2 l3 = true ->
flows l1 l3 = true
; flows_antisymm : forall l1 l2, flows l1 l2 = true ->
flows l2 l1 = true -> l1 = l2
; flows_join_right : forall l1 l2, flows l1 (join l1 l2) = true
; flows_join_left : forall l1 l2, flows l2 (join l1 l2) = true
; join_minimal : forall l1 l2 l, flows l1 l = true ->
flows l2 l = true ->
flows (join l1 l2) l = true
}.
Notation "l1 \_/ l2" := (join l1 l2) (at level 40) : type_scope.
Notation "l1 <: l2" := (flows l1 l2 = true)
(at level 50, no associativity) : type_scope.
Notation "⊥" := bot.
Hint Resolve
@flows_refl
@flows_trans
@flows_join_left
@flows_join_right
@flows_antisymm
@join_minimal : lat.
Definition flows_to {Lab : Type} `{JoinSemiLattice Lab} (l1 l2 : Lab) : Z :=
if flows l1 l2 then 1%Z else 0%Z.
(** Immediate properties from the semi-lattice structure. *)
Section JoinSemiLattice_properties.
Context {T: Type}.
Lemma flows_join {L : JoinSemiLattice T} : forall l1 l2,
l1 <: l2 <-> l1 \_/ l2 = l2.
Proof.
intros.
split.
- intros H.
apply flows_antisymm.
+ apply join_minimal; auto with lat.
+ apply flows_join_left.
- intros H.
rewrite <- H.
auto with lat.
Qed.
Lemma join_1_rev {L : JoinSemiLattice T} : forall l1 l2 l,
l1 \_/ l2 <: l -> l1 <: l.
Proof. eauto with lat. Qed.
Lemma join_2_rev {L : JoinSemiLattice T} : forall l1 l2 l,
l1 \_/ l2 <: l -> l2 <: l.
Proof. eauto with lat. Qed.
Lemma join_1 {L : JoinSemiLattice T} : forall l l1 l2,
l <: l1 -> l <: l1 \_/ l2.
Proof. eauto with lat. Qed.
Lemma join_2 {L : JoinSemiLattice T} : forall l l1 l2,
l <: l2 -> l <: l1 \_/ l2.
Proof. eauto with lat. Qed.
Lemma join_bot_right {L : JoinSemiLattice T} : forall l,
l \_/ bot = l.
Proof.
eauto using bot_flows with lat.
Qed.
Lemma join_bot_left {L: JoinSemiLattice T} : forall l,
bot \_/ l = l.
Proof. eauto using bot_flows with lat.
Qed.
Lemma not_flows_not_join_flows_left {L : JoinSemiLattice T} : forall l l1 l2,
flows l1 l = false ->
flows (l1 \_/ l2) l = false.
Proof.
intros.
destruct (flows (l1 \_/ l2) l) eqn:E.
exploit join_1_rev; eauto.
auto.
Qed.
Lemma not_flows_not_join_flows_right {L : JoinSemiLattice T} : forall l l1 l2,
flows l2 l = false ->
flows (l1 \_/ l2) l = false.
Proof.
intros.
destruct (flows (l1 \_/ l2) l) eqn:E.
exploit join_2_rev; eauto.
auto.
Qed.
Definition label_eqb {L : JoinSemiLattice T} l1 l2 :=
flows l1 l2 && flows l2 l1.
Lemma label_eqP (L : JoinSemiLattice T) : Equality.axiom label_eqb.
Proof.
move => l1 l2.
rewrite /label_eqb.
apply/(iffP idP).
- move/andP => [H1 H2].
by apply flows_antisymm.
- move => -> .
by rewrite !flows_refl.
Qed.
Definition label_eqMixin (L : JoinSemiLattice T) := EqMixin (@label_eqP L).
End JoinSemiLattice_properties.
Hint Resolve
@join_1
@join_2
@bot_flows
@not_flows_not_join_flows_right
@not_flows_not_join_flows_left : lat.
Definition label_dec {T : Type} {Lat : JoinSemiLattice T}
: forall l1 l2 : T, {l1 = l2} + {l1 <> l2}.
Proof.
intros x y.
destruct (flows x y) eqn:xy;
destruct (flows y x) eqn:yx; try (right; congruence).
- left. eauto with lat.
- generalize (flows_refl x). intros.
right. congruence.
Defined.
Class Lattice (Lab: Type) :=
{ jslat :> JoinSemiLattice Lab
; top : Lab
; flows_top : forall l, l <: top
}.
Module Import LabelEqType.
Canonical label_eqType T {L : JoinSemiLattice T} := Eval hnf in EqType _ (label_eqMixin L).
End LabelEqType.
Class FiniteLattice (Lab : Type) :=
{
lat :> Lattice Lab
; elems : list Lab
; all_elems : forall l : Lab, l \in elems
}.
Definition allThingsBelow {L : Type} `{FiniteLattice L} (l : L) : list L :=
filter (fun l' => flows l' l) elems.