-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathReachableThreshold.v
181 lines (167 loc) · 6.34 KB
/
ReachableThreshold.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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
From stdpp Require Import prelude.
From Coq Require Import Reals Lra.
From VLSM.Lib Require Import RealsExtras Measurable ListExtras StdppListSet.
(** * Core: Reachable Threshold
Given a set of validators and a [threshold] (a positive real number), we say
that the threshold is reachable ([rt_reachable]) when there exists a
set of validators whose combined weight passes the threshold.
In this module we prove that there exist a [potentially_pivotal] validator,
i.e., a validator which added to a set of validators tips over the threshold.
*)
Class ReachableThreshold V Cv (threshold : R) `{Hm : Measurable V} `{FinSet V Cv} : Prop :=
{
rt_positive : (0 <= threshold)%R;
rt_reachable : exists (vs : Cv), (sum_weights vs > threshold)%R;
}.
#[global] Hint Mode ReachableThreshold - - - ! ! ! ! ! ! ! ! ! ! : typeclass_instances.
Section sec_reachable_threshold_props.
Context
(threshold : R)
`{Hrt : ReachableThreshold V Cv threshold}
.
(**
Given a list with no duplicates and whose added weight does not pass the
threshold, we can iteratively add elements into it until it passes the
threshold. Hence, the last element added will tip over the threshold.
*)
Lemma pivotal_validator_extension_list
: forall vsfix vss,
NoDup vsfix ->
(sum_weights_list vsfix <= threshold)%R ->
NoDup (vss ++ vsfix) ->
(sum_weights_list (vss ++ vsfix) > threshold)%R ->
exists (vs : list V),
NoDup vs /\
vs ⊆ vss /\
(sum_weights_list (vs ++ vsfix) > threshold)%R /\
exists v,
v ∈ vs /\
(sum_weights_list (set_remove v vs ++ vsfix) <= threshold)%R.
Proof.
induction vss; intros Hnd_vsfix Hvsfix Hnd_all Hall; simpl in Hall; [by lra |].
destruct (Rle_or_lt (sum_weights_list (vss ++ vsfix)) threshold) as [| Hgt].
- exists (a :: vss).
repeat split; [| done | done |].
+ by apply nodup_append_left in Hnd_all.
+ exists a.
split; [by left |].
by cbn; rewrite decide_True.
- apply NoDup_cons in Hnd_all as [Hnin Hvss].
apply IHvss in Hgt as (vs & Hvs & Hincl & Hex); [| done..].
exists vs.
repeat (split; try done).
by right; apply Hincl.
Qed.
(**
The [FinSet] version of the [pivotal_validator_extension_list] result.
*)
Lemma pivotal_validator_extension
: forall (vsfix vss : Cv),
(sum_weights vsfix <= threshold)%R ->
vss ## vsfix ->
(sum_weights (vss ∪ vsfix) > threshold)%R ->
exists (vs : Cv),
vs ⊆ vss /\
(sum_weights (vs ∪ vsfix) > threshold)%R /\
exists v,
v ∈ vs /\
(sum_weights (vs ∖ {[ v ]} ∪ vsfix) <= threshold)%R.
Proof.
intros vsfix vss Hvsfix Hdisj Hall.
destruct (pivotal_validator_extension_list (elements vsfix) (elements vss))
as (vs & Hnd_vs & Hincl & Hvs & v & Hv & Hvs_v);
[by apply NoDup_elements | done | ..].
- apply NoDup_app; split_and!; [by apply NoDup_elements | | by apply NoDup_elements].
by intro; rewrite !elem_of_elements; intros ? ?; eapply Hdisj.
- rewrite sum_weights_app_list.
by rewrite sum_weights_disj_union in Hall.
- exists (list_to_set vs); split_and!.
+ by intros a Ha; apply elem_of_list_to_set, Hincl, elem_of_elements in Ha.
+ rewrite sum_weights_app_list in Hvs.
rewrite sum_weights_disj_union.
* replace (sum_weights (list_to_set vs)) with (sum_weights_list vs); [done |].
apply sum_weights_list_permutation_proper.
by rewrite elements_list_to_set.
* intros x; rewrite elem_of_list_to_set.
intros Hx_vs Hx_vsfix; eapply Hdisj; [| done].
by eapply elem_of_elements, Hincl.
+ exists v; split; [by apply elem_of_list_to_set |].
replace (sum_weights _)
with (sum_weights_list (StdppListSet.set_remove v vs ++ elements vsfix)); [done |].
apply sum_weights_list_permutation_proper.
rewrite elements_disj_union.
* apply Permutation_app_tail.
etransitivity; [by symmetry; apply (elements_list_to_set (H6 := H6)), set_remove_nodup |].
apply elements_proper.
intro x.
rewrite elem_of_difference, !elem_of_list_to_set.
by rewrite set_remove_iff, elem_of_singleton.
* intros x; rewrite elem_of_difference, elem_of_list_to_set, elem_of_singleton.
by intros [] ?; eapply Hdisj; [apply elem_of_elements, Hincl |].
Qed.
(**
Given a set of validators whose combined weight passes the threshold, we can
iteratively remove elements until the combined weight decreases below the
threshold. The last element removed tips over the threshold.
*)
Lemma validators_pivotal_ind
: forall (vss : Cv),
(sum_weights vss > threshold)%R ->
exists vs,
vs ⊆ vss /\
(sum_weights vs > threshold)%R /\
exists v,
v ∈ vs /\
(sum_weights (vs ∖ {[ v ]}) <= threshold)%R.
Proof.
intros vss Hvss.
destruct (pivotal_validator_extension ∅ vss)
as (vs & Hincl & Hvs & v & Hv & Hvs').
- rewrite sum_weights_empty; [| done].
by apply (rt_positive (H6 := H6)).
- by apply disjoint_empty_r.
- by rewrite sum_weights_union_empty.
- rewrite sum_weights_union_empty in Hvs, Hvs'.
by repeat esplit.
Qed.
(**
There exists a set whose combined weight passes the threshold and containing
an element such that, if the element is removed, the combined weight decreases
below the threshold.
*)
Lemma sufficient_validators_pivotal
: exists (vs : Cv),
(sum_weights vs > threshold)%R /\
exists v,
v ∈ vs /\
(sum_weights (vs ∖ {[ v ]}) <= threshold)%R.
Proof.
destruct (rt_reachable (1 := Hrt)) as [vs Hweight].
apply (validators_pivotal_ind vs) in Hweight as (vs' & Hincl & Hvs').
by exists vs'.
Qed.
(**
A validator <<v>> is called potentially pivotal if there exists a set of
validators whose combined weight is below the threshold such that, if
adding <<v>> to the set, the combine weight would pass over the threshold.
*)
Definition potentially_pivotal (v : V) : Prop :=
exists (vs : Cv),
v ∉ vs /\
(sum_weights vs <= threshold)%R /\
(sum_weights vs > threshold - weight v)%R.
(**
The main result of this section proves the existence of a [potentially_pivotal]
validator.
*)
Lemma exists_pivotal_validator :
exists v, potentially_pivotal v.
Proof.
destruct sufficient_validators_pivotal as (vs & Hgt & v & Hin & Hlte).
exists v, (vs ∖ {[ v ]}); split_and!.
- by rewrite elem_of_difference, elem_of_singleton; intros [].
- done.
- rewrite (sum_weights_in v) in Hgt by done.
by clear Hlte; cbv in *; lra.
Qed.
End sec_reachable_threshold_props.