From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From Coq Require Import Reals Lra.
From VLSM.Lib Require Import RealsExtras Measurable ListExtras StdppListSet.[Loading ML file coq-itauto.plugin ... done]

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.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∀ vsfix vss : list V,
  NoDup vsfix
  → (sum_weights_list vsfix <= threshold)%R
    → NoDup (vss ++ vsfix)
      → (sum_weights_list (vss ++ vsfix) > threshold)%R
        → ∃ vs : list V,
            NoDup vs
            ∧ vs ⊆ vss
              ∧ (sum_weights_list (vs ++ vsfix) >
                 threshold)%R
                ∧ (∃ v : V,
                     v ∈ vs
                     ∧ (sum_weights_list
                          (set_remove v vs ++ vsfix) <=
                        threshold)%R)
Proof.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∀ vsfix vss : list V,
  NoDup vsfix
  → (sum_weights_list vsfix <= threshold)%R
    → NoDup (vss ++ vsfix)
      → (sum_weights_list (vss ++ vsfix) > threshold)%R
        → ∃ vs : list V,
            NoDup vs
            ∧ vs ⊆ vss
              ∧ (sum_weights_list (vs ++ vsfix) >
                 threshold)%R
                ∧ (∃ v : V,
                     v ∈ vs
                     ∧ (sum_weights_list
                          (set_remove v vs ++ vsfix) <=
                        threshold)%R)
  induction vss; intros Hnd_vsfix Hvsfix Hnd_all Hall; simpl in Hall; [by lra |].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
∃ vs : list V,
  NoDup vs
  ∧ vs ⊆ a :: vss
    ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
      ∧ (∃ v : V,
           v ∈ vs
           ∧ (sum_weights_list
                (set_remove v vs ++ vsfix) <=
              threshold)%R)
  destruct (Rle_or_lt (sum_weights_list (vss ++ vsfix)) threshold) as [| Hgt].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
∃ vs : list V,
  NoDup vs
  ∧ vs ⊆ a :: vss
    ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
      ∧ (∃ v : V,
           v ∈ vs
           ∧ (sum_weights_list
                (set_remove v vs ++ vsfix) <=
              threshold)%R)
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
Hgt: (threshold < sum_weights_list (vss ++ vsfix))%R
∃ vs : list V,
  NoDup vs
  ∧ vs ⊆ a :: vss
    ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
      ∧ (∃ v : V,
           v ∈ vs
           ∧ (sum_weights_list
                (set_remove v vs ++ vsfix) <=
              threshold)%R)
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
∃ vs : list V,
  NoDup vs
  ∧ vs ⊆ a :: vss
    ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
      ∧ (∃ v : V,
           v ∈ vs
           ∧ (sum_weights_list
                (set_remove v vs ++ vsfix) <=
              threshold)%R) exists (a :: vss).threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
NoDup (a :: vss)
∧ a :: vss ⊆ a :: vss
  ∧ (sum_weights_list ((a :: vss) ++ vsfix) >
     threshold)%R
    ∧ (∃ v : V,
         v ∈ a :: vss
         ∧ (sum_weights_list
              (set_remove v (a :: vss) ++ vsfix) <=
            threshold)%R)
    repeat split; [| done | done |].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
NoDup (a :: vss)
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
∃ v : V,
  v ∈ a :: vss
  ∧ (sum_weights_list
       (set_remove v (a :: vss) ++ vsfix) <= threshold)%R
    +threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
NoDup (a :: vss) by apply nodup_append_left in Hnd_all.
    +threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
∃ v : V,
  v ∈ a :: vss
  ∧ (sum_weights_list
       (set_remove v (a :: vss) ++ vsfix) <= threshold)%R exists a.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
a ∈ a :: vss
∧ (sum_weights_list (set_remove a (a :: vss) ++ vsfix) <=
   threshold)%R
      split; [by left |].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
H7: (sum_weights_list (vss ++ vsfix) <= threshold)%R
(sum_weights_list (set_remove a (a :: vss) ++ vsfix) <=
 threshold)%R
      by cbn; rewrite decide_True.
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnd_all: NoDup ((a :: vss) ++ vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
Hgt: (threshold < sum_weights_list (vss ++ vsfix))%R
∃ vs : list V,
  NoDup vs
  ∧ vs ⊆ a :: vss
    ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
      ∧ (∃ v : V,
           v ∈ vs
           ∧ (sum_weights_list
                (set_remove v vs ++ vsfix) <=
              threshold)%R) apply NoDup_cons in Hnd_all as [Hnin Hvss].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnin: a
∉ (fix app (l m : list V) {struct l} :
       list V :=
     match l with
     | [] => m
     | a :: l1 => a :: app l1 m
     end) vss vsfix
Hvss: NoDup
  ((fix app (l m : list V) {struct l} :
        list V :=
      match l with
      | [] => m
      | a :: l1 => a :: app l1 m
      end) vss vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
Hgt: (threshold < sum_weights_list (vss ++ vsfix))%R
∃ vs : list V,
  NoDup vs
  ∧ vs ⊆ a :: vss
    ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
      ∧ (∃ v : V,
           v ∈ vs
           ∧ (sum_weights_list
                (set_remove v vs ++ vsfix) <=
              threshold)%R)
    apply IHvss in Hgt as (vs & Hvs & Hincl & Hex); [| done..].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnin: a
∉ (fix app (l m : list V) {struct l} :
       list V :=
     match l with
     | [] => m
     | a :: l1 => a :: app l1 m
     end) vss vsfix
Hvss: NoDup
  ((fix app (l m : list V) {struct l} :
        list V :=
      match l with
      | [] => m
      | a :: l1 => a :: app l1 m
      end) vss vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
vs: list V
Hvs: NoDup vs
Hincl: vs ⊆ vss
Hex: (sum_weights_list (vs ++ vsfix) > threshold)%R
∧ (∃ v : V,
     v ∈ vs
     ∧ (sum_weights_list
          (set_remove v vs ++ vsfix) <=
        threshold)%R)
∃ vs : list V,
  NoDup vs
  ∧ vs ⊆ a :: vss
    ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
      ∧ (∃ v : V,
           v ∈ vs
           ∧ (sum_weights_list
                (set_remove v vs ++ vsfix) <=
              threshold)%R)
    exists vs.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnin: a
∉ (fix app (l m : list V) {struct l} :
       list V :=
     match l with
     | [] => m
     | a :: l1 => a :: app l1 m
     end) vss vsfix
Hvss: NoDup
  ((fix app (l m : list V) {struct l} :
        list V :=
      match l with
      | [] => m
      | a :: l1 => a :: app l1 m
      end) vss vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
vs: list V
Hvs: NoDup vs
Hincl: vs ⊆ vss
Hex: (sum_weights_list (vs ++ vsfix) > threshold)%R
∧ (∃ v : V,
     v ∈ vs
     ∧ (sum_weights_list
          (set_remove v vs ++ vsfix) <=
        threshold)%R)
NoDup vs
∧ vs ⊆ a :: vss
  ∧ (sum_weights_list (vs ++ vsfix) > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights_list
              (set_remove v vs ++ vsfix) <= threshold)%R)
    repeat (split; try done).threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix: list V
a: V
vss: list V
IHvss: NoDup vsfix
→ (sum_weights_list vsfix <= threshold)%R
  → NoDup (vss ++ vsfix)
    → (sum_weights_list (vss ++ vsfix) >
       threshold)%R
      → ∃ vs : list V,
          NoDup vs
          ∧ vs ⊆ vss
            ∧ (sum_weights_list (vs ++ vsfix) >
               threshold)%R
              ∧ (∃ v : V,
                   v ∈ vs
                   ∧ (sum_weights_list
                     (set_remove v vs ++ vsfix) <=
                     threshold)%R)
Hnd_vsfix: NoDup vsfix
Hvsfix: (sum_weights_list vsfix <= threshold)%R
Hnin: a
∉ (fix app (l m : list V) {struct l} :
       list V :=
     match l with
     | [] => m
     | a :: l1 => a :: app l1 m
     end) vss vsfix
Hvss: NoDup
  ((fix app (l m : list V) {struct l} :
        list V :=
      match l with
      | [] => m
      | a :: l1 => a :: app l1 m
      end) vss vsfix)
Hall: (`(weight a) + sum_weights_list (vss ++ vsfix) >
 threshold)%R
vs: list V
Hvs: NoDup vs
Hincl: vs ⊆ vss
Hex: (sum_weights_list (vs ++ vsfix) > threshold)%R
∧ (∃ v : V,
     v ∈ vs
     ∧ (sum_weights_list
          (set_remove v vs ++ vsfix) <=
        threshold)%R)
vs ⊆ a :: vss
    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.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∀ vsfix vss : Cv,
  (sum_weights vsfix <= threshold)%R
  → vss ## vsfix
    → (sum_weights (vss ∪ vsfix) > threshold)%R
      → ∃ vs : Cv,
          vs ⊆ vss
          ∧ (sum_weights (vs ∪ vsfix) > threshold)%R
            ∧ (∃ v : V,
                 v ∈ vs
                 ∧ (sum_weights (vs ∖ {[v]} ∪ vsfix) <=
                    threshold)%R)
Proof.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∀ vsfix vss : Cv,
  (sum_weights vsfix <= threshold)%R
  → vss ## vsfix
    → (sum_weights (vss ∪ vsfix) > threshold)%R
      → ∃ vs : Cv,
          vs ⊆ vss
          ∧ (sum_weights (vs ∪ vsfix) > threshold)%R
            ∧ (∃ v : V,
                 v ∈ vs
                 ∧ (sum_weights (vs ∖ {[v]} ∪ vsfix) <=
                    threshold)%R)
  intros vsfix vss Hvsfix Hdisj Hall.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
∃ vs : Cv,
  vs ⊆ vss
  ∧ (sum_weights (vs ∪ vsfix) > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights (vs ∖ {[v]} ∪ vsfix) <=
            threshold)%R)
  destruct (pivotal_validator_extension_list (elements vsfix) (elements vss))
    as (vs & Hnd_vs & Hincl & Hvs & v & Hv & Hvs_v);
      [by apply NoDup_elements | done | ..].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
NoDup (elements vss ++ elements vsfix)
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
(sum_weights_list (elements vss ++ elements vsfix) >
 threshold)%R
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
∃ vs : Cv,
  vs ⊆ vss
  ∧ (sum_weights (vs ∪ vsfix) > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights (vs ∖ {[v]} ∪ vsfix) <=
            threshold)%R)
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
NoDup (elements vss ++ elements vsfix) apply NoDup_app; split_and!; [by apply NoDup_elements | | by apply NoDup_elements].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
∀ x : V, x ∈ elements vss → x ∉ elements vsfix
    by intro; rewrite !elem_of_elements; intros ? ?; eapply Hdisj.
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
(sum_weights_list (elements vss ++ elements vsfix) >
 threshold)%R rewrite sum_weights_app_list.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
(sum_weights_list (elements vss) +
 sum_weights_list (elements vsfix) > threshold)%R
    by rewrite sum_weights_disj_union in Hall.
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
∃ vs : Cv,
  vs ⊆ vss
  ∧ (sum_weights (vs ∪ vsfix) > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights (vs ∖ {[v]} ∪ vsfix) <=
            threshold)%R) exists (list_to_set vs); split_and!.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
list_to_set vs ⊆ vss
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
(sum_weights (list_to_set vs ∪ vsfix) > threshold)%R
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
∃ v : V,
  v ∈ list_to_set vs
  ∧ (sum_weights (list_to_set vs ∖ {[v]} ∪ vsfix) <=
     threshold)%R
    +threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
list_to_set vs ⊆ vss by intros a Ha; apply elem_of_list_to_set, Hincl, elem_of_elements in Ha.
    +threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
(sum_weights (list_to_set vs ∪ vsfix) > threshold)%R rewrite sum_weights_app_list in Hvs.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
(sum_weights (list_to_set vs ∪ vsfix) > threshold)%R
      rewrite sum_weights_disj_union.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
(sum_weights (list_to_set vs) + sum_weights vsfix >
 threshold)%R
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
list_to_set vs ## vsfix
      *threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
(sum_weights (list_to_set vs) + sum_weights vsfix >
 threshold)%R replace (sum_weights (list_to_set vs)) with (sum_weights_list vs); [done |].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
sum_weights_list vs = sum_weights (list_to_set vs)
        apply sum_weights_list_permutation_proper.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
vs ≡ₚ elements (list_to_set vs)
        by rewrite elements_list_to_set.
      *threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
list_to_set vs ## vsfix intros x; rewrite elem_of_list_to_set.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
x: V
x ∈ vs → x ∈ vsfix → False
        intros Hx_vs Hx_vsfix; eapply Hdisj; [| done].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list vs +
 sum_weights_list (elements vsfix) > threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
x: V
Hx_vs: x ∈ vs
Hx_vsfix: x ∈ vsfix
x ∈ vss
        by eapply elem_of_elements, Hincl.
    +threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
∃ v : V,
  v ∈ list_to_set vs
  ∧ (sum_weights (list_to_set vs ∖ {[v]} ∪ vsfix) <=
     threshold)%R exists v; split; [by apply elem_of_list_to_set |].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
(sum_weights (list_to_set vs ∖ {[v]} ∪ vsfix) <=
 threshold)%R
      replace (sum_weights _)
        with (sum_weights_list (StdppListSet.set_remove v vs ++ elements vsfix)); [done |].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
sum_weights_list (set_remove v vs ++ elements vsfix) =
sum_weights (list_to_set vs ∖ {[v]} ∪ vsfix)
      apply sum_weights_list_permutation_proper.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
set_remove v vs ++ elements vsfix
≡ₚ elements (list_to_set vs ∖ {[v]} ∪ vsfix)
      rewrite elements_disj_union.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
set_remove v vs ++ elements vsfix
≡ₚ elements (list_to_set vs ∖ {[v]}) ++ elements vsfix
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
list_to_set vs ∖ {[v]} ## vsfix
      *threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
set_remove v vs ++ elements vsfix
≡ₚ elements (list_to_set vs ∖ {[v]}) ++ elements vsfix apply Permutation_app_tail.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
set_remove v vs ≡ₚ elements (list_to_set vs ∖ {[v]})
        etransitivity; [by symmetry; apply (elements_list_to_set (H6 := H6)), set_remove_nodup |].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
elements (list_to_set (set_remove v vs))
≡ₚ elements (list_to_set vs ∖ {[v]})
        apply elements_proper.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
list_to_set (set_remove v vs) ≡ list_to_set vs ∖ {[v]}
        intro x.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
x: V
x ∈ list_to_set (set_remove v vs)
↔ x ∈ list_to_set vs ∖ {[v]}
        rewrite elem_of_difference, !elem_of_list_to_set.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
x: V
x ∈ set_remove v vs ↔ x ∈ vs ∧ x ∉ {[v]}
        by rewrite set_remove_iff, elem_of_singleton.
      *threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
list_to_set vs ∖ {[v]} ## vsfix intros x; rewrite elem_of_difference, elem_of_list_to_set, elem_of_singleton.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vsfix, vss: Cv
Hvsfix: (sum_weights vsfix <= threshold)%R
Hdisj: vss ## vsfix
Hall: (sum_weights (vss ∪ vsfix) > threshold)%R
vs: list V
Hnd_vs: NoDup vs
Hincl: vs ⊆ elements vss
Hvs: (sum_weights_list (vs ++ elements vsfix) >
 threshold)%R
v: V
Hv: v ∈ vs
Hvs_v: (sum_weights_list
   (set_remove v vs ++ elements vsfix) <=
 threshold)%R
x: V
x ∈ vs ∧ x ≠ v → x ∈ vsfix → False
        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.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∀ vss : Cv,
  (sum_weights vss > threshold)%R
  → ∃ vs : Cv,
      vs ⊆ vss
      ∧ (sum_weights vs > threshold)%R
        ∧ (∃ v : V,
             v ∈ vs
             ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
Proof.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∀ vss : Cv,
  (sum_weights vss > threshold)%R
  → ∃ vs : Cv,
      vs ⊆ vss
      ∧ (sum_weights vs > threshold)%R
        ∧ (∃ v : V,
             v ∈ vs
             ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
  intros vss Hvss.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
∃ vs : Cv,
  vs ⊆ vss
  ∧ (sum_weights vs > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
  destruct (pivotal_validator_extension ∅ vss)
    as (vs & Hincl & Hvs & v & Hv & Hvs').threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
(sum_weights ∅ <= threshold)%R
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
vss ## ∅
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
(sum_weights (vss ∪ ∅) > threshold)%R
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
vs: Cv
Hincl: vs ⊆ vss
Hvs: (sum_weights (vs ∪ ∅) > threshold)%R
v: V
Hv: v ∈ vs
Hvs': (sum_weights (vs ∖ {[v]} ∪ ∅) <= threshold)%R
∃ vs : Cv,
  vs ⊆ vss
  ∧ (sum_weights vs > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
(sum_weights ∅ <= threshold)%R rewrite sum_weights_empty; [| done].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
(0 <= threshold)%R
    by apply (rt_positive (H6 := H6)).
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
vss ## ∅ by apply disjoint_empty_r.
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
(sum_weights (vss ∪ ∅) > threshold)%R by rewrite sum_weights_union_empty.
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
vs: Cv
Hincl: vs ⊆ vss
Hvs: (sum_weights (vs ∪ ∅) > threshold)%R
v: V
Hv: v ∈ vs
Hvs': (sum_weights (vs ∖ {[v]} ∪ ∅) <= threshold)%R
∃ vs : Cv,
  vs ⊆ vss
  ∧ (sum_weights vs > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R) rewrite sum_weights_union_empty in Hvs, Hvs'.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vss: Cv
Hvss: (sum_weights vss > threshold)%R
vs: Cv
Hincl: vs ⊆ vss
Hvs: (sum_weights vs > threshold)%R
v: V
Hv: v ∈ vs
Hvs': (sum_weights (vs ∖ {[v]}) <= threshold)%R
∃ vs : Cv,
  vs ⊆ vss
  ∧ (sum_weights vs > threshold)%R
    ∧ (∃ v : V,
         v ∈ vs
         ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
    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.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∃ vs : Cv,
  (sum_weights vs > threshold)%R
  ∧ (∃ v : V,
       v ∈ vs
       ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
Proof.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∃ vs : Cv,
  (sum_weights vs > threshold)%R
  ∧ (∃ v : V,
       v ∈ vs
       ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
  destruct (rt_reachable (1 := Hrt)) as [vs Hweight].threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hweight: (sum_weights vs > threshold)%R
∃ vs : Cv,
  (sum_weights vs > threshold)%R
  ∧ (∃ v : V,
       v ∈ vs
       ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
  apply (validators_pivotal_ind vs) in Hweight as (vs' & Hincl & Hvs').threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs, vs': Cv
Hincl: vs' ⊆ vs
Hvs': (sum_weights vs' > threshold)%R
∧ (∃ v : V,
     v ∈ vs'
     ∧ (sum_weights (vs' ∖ {[v]}) <= threshold)%R)
∃ vs : Cv,
  (sum_weights vs > threshold)%R
  ∧ (∃ v : V,
       v ∈ vs
       ∧ (sum_weights (vs ∖ {[v]}) <= threshold)%R)
  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.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∃ v : V, potentially_pivotal v
Proof.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
∃ v : V, potentially_pivotal v
  destruct sufficient_validators_pivotal as (vs & Hgt & v & Hin & Hlte).threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hgt: (sum_weights vs > threshold)%R
v: V
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
∃ v : V, potentially_pivotal v
  exists v, (vs ∖ {[ v ]}); split_and!.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hgt: (sum_weights vs > threshold)%R
v: V
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
v ∉ vs ∖ {[v]}
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hgt: (sum_weights vs > threshold)%R
v: V
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
(sum_weights (vs ∖ {[v]}) <= threshold)%R
threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hgt: (sum_weights vs > threshold)%R
v: V
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
(sum_weights (vs ∖ {[v]}) > threshold - weight v)%R
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hgt: (sum_weights vs > threshold)%R
v: V
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
v ∉ vs ∖ {[v]} by rewrite elem_of_difference, elem_of_singleton; intros [].
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hgt: (sum_weights vs > threshold)%R
v: V
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
(sum_weights (vs ∖ {[v]}) <= threshold)%R done.
  -threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
Hgt: (sum_weights vs > threshold)%R
v: V
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
(sum_weights (vs ∖ {[v]}) > threshold - weight v)%R rewrite (sum_weights_in v) in Hgt by done.threshold: R
V, Cv: Type
Hm: Measurable V
H: ElemOf V Cv
H0: Empty Cv
H1: Singleton V Cv
H2: Union Cv
H3: Intersection Cv
H4: Difference Cv
H5: Elements V Cv
EqDecision0: EqDecision V
H6: FinSet V Cv
Hrt: ReachableThreshold V Cv threshold
vs: Cv
v: V
Hgt: (`(weight v) + sum_weights (vs ∖ {[v]}) >
 threshold)%R
Hin: v ∈ vs
Hlte: (sum_weights (vs ∖ {[v]}) <= threshold)%R
(sum_weights (vs ∖ {[v]}) > threshold - weight v)%R
    by clear Hlte; cbv in *; lra.
Qed.

End sec_reachable_threshold_props.