Library Majority
Copyright (c) 2018 by Swirlds, Inc.
Implemented by Karl Crary.
Require Import Nat.
Require Import List.
Require Import Decide.
Require Import Omega.
Require Import Tact.
Require Import Weight.
Require Import Calculate.
Definition every {T : Type} : T -> Prop := fun _ => True.
Lemma incl_every :
forall T (P : T -> Prop), incl P every.
Hint Resolve incl_every.
Definition majority {T : Type} (f : T -> nat) (P Q : T -> Prop) :=
exists m n,
incl P Q
/\ weight f P m
/\ weight f Q n
/\ m > one_half n.
Definition supermajority {T : Type} (f : T -> nat) (P Q : T -> Prop) :=
exists m n,
incl P Q
/\ weight f P m
/\ weight f Q n
/\ m > two_thirds n.
enough to deny a supermajority
Definition superminority {T : Type} (f : T -> nat) (P Q : T -> Prop) :=
exists m n,
incl P Q
/\ weight f P m
/\ weight f Q n
/\ m >= one_third n.
exists m n,
incl P Q
/\ weight f P m
/\ weight f Q n
/\ m >= one_third n.
enough to deny a majority
Definition atleasthalf {T : Type} (f : T -> nat) (P Q : T -> Prop) :=
exists m n,
incl P Q
/\ weight f P m
/\ weight f Q n
/\ m >= one_half (S n).
exists m n,
incl P Q
/\ weight f P m
/\ weight f Q n
/\ m >= one_half (S n).
Manipulations
Lemma majority_incl :
forall (T : Type) (f : T -> nat) (P Q : T -> Prop),
majority f P Q
-> incl P Q.
Lemma unanimous_supermajority :
forall T (f : T -> nat) (P : T -> Prop) n,
n > 0
-> weight f P n
-> supermajority f P P.
Lemma supermajority_impl_majority :
forall (T : Type) (f : T -> nat) (P U : T -> Prop),
supermajority f P U
-> majority f P U.
Lemma majority_impl_superminority :
forall (T : Type) (f : T -> nat) (P U : T -> Prop),
majority f P U
-> superminority f P U.
Lemma majority_enlarge :
forall (T : Type) (f : T -> nat) (P Q U : T -> Prop),
incl P Q
-> incl Q U
-> (forall x, U x -> decidable (Q x))
-> majority f P U
-> majority f Q U.
Lemma supermajority_enlarge :
forall (T : Type) (f : T -> nat) (P Q U : T -> Prop),
incl P Q
-> incl Q U
-> (forall x, U x -> decidable (Q x))
-> supermajority f P U
-> supermajority f Q U.
Lemma supermajority_iff :
forall (T : Type) (f : T -> nat) (P Q U : T -> Prop),
(forall x, P x <-> Q x)
-> supermajority f P U
-> supermajority f Q U.
Intersections
Lemma majority_intersect :
forall T (f : T -> nat) (P Q U : T -> Prop),
(forall (x y : T), decidable (x = y))
-> majority f P U
-> majority f Q U
-> exists x, P x /\ Q x.
Lemma majority_atleasthalf_intersect :
forall T (f : T -> nat) (P Q U : T -> Prop),
(forall (x y : T), decidable (x = y))
-> majority f P U
-> atleasthalf f Q U
-> exists x, P x /\ Q x.
Lemma supermajority_intersect_2 :
forall T (f : T -> nat) (P Q U : T -> Prop),
(forall (x y : T), decidable (x = y))
-> supermajority f P U
-> supermajority f Q U
-> exists R,
majority f R P
/\ majority f R Q.
Lemma supermajority_intersect_2' :
forall T (f : T -> nat) (P Q U : T -> Prop),
(forall (x y : T), decidable (x = y))
-> supermajority f P U
-> supermajority f Q U
-> majority f (fun x => P x /\ Q x) P
/\ majority f (fun x => P x /\ Q x) Q.
Lemma supermajority_intersect_3 :
forall T (f : T -> nat) (P Q R U : T -> Prop),
(forall (x y : T), decidable (x = y))
-> supermajority f P U
-> supermajority f Q U
-> supermajority f R U
-> exists x, P x /\ Q x /\ R x.
Lemma superminority_supermajority_intersect :
forall T (f : T -> nat) (P Q U : T -> Prop),
(forall (x y : T), decidable (x = y))
-> superminority f P U
-> supermajority f Q U
-> exists x, P x /\ Q x.
Lemma majority_decide :
forall (T : Type) (f : T -> nat) (P U : T -> Prop) n,
(forall x, decidable (P x))
-> incl P U
-> weight f U n
-> decidable (majority f P U).
Lemma supermajority_decide :
forall (T : Type) (f : T -> nat) (P U : T -> Prop) n,
(forall x, decidable (P x))
-> incl P U
-> weight f U n
-> decidable (supermajority f P U).
Lemma not_supermajority :
forall T (f : T -> nat) (P U : T -> Prop) n,
(forall x, decidable (P x))
-> incl P U
-> weight f U n
-> ~ supermajority f P U
-> superminority f (fun x => ~ P x /\ U x) U.
Lemma not_supermajority_every :
forall T (f : T -> nat) (P : T -> Prop) n,
(forall x, decidable (P x))
-> weight f (@every T) n
-> ~ supermajority f P every
-> superminority f (fun x => ~ P x) every.
Lemma majority_inhabitant :
forall T (f : T -> nat) (P U : T -> Prop),
majority f P U
-> exists x, P x.
Lemma supermajority_inhabitant :
forall T (f : T -> nat) (P U : T -> Prop),
supermajority f P U
-> exists x, P x.