Library Calculate
Copyright (c) 2018 by Swirlds, Inc.
Implemented by Karl Crary.
Require Import Nat.
Require Import Omega.
Require Import Tact.
Definition one_half (n : nat) := n / 2.
Definition two_thirds (n : nat) := 2 * n / 3.
Definition one_third (n : nat) := n - two_thirds n.
Lemma majority_intersect_calculation :
forall x y z,
x > z / 2
-> y > z / 2
-> x + y - z > 0.
Lemma majority_atleasthalf_intersect_calculation :
forall x y z,
x > z / 2
-> y >= S z / 2
-> x + y - z > 0.
Lemma mod3_0 : (2 * 0) mod 3 = 0.
Lemma mod3_1 : (2 * 1) mod 3 = 2.
Lemma mod3_2 : (2 * 2) mod 3 = 1.
Hint Rewrite mod3_0 mod3_1 mod3_2 : mod3.
Lemma supermajority_intersect_2_calculation :
forall x y z,
x > 2 * z / 3
-> y > 2 * z / 3
-> x + y - z > x / 2.
Lemma supermajority_intersect_3_calculation :
forall w x y z,
w > 2 * z / 3
-> x > 2 * z / 3
-> y > 2 * z / 3
-> w + x + y - 2 * z > 0.
Lemma superminority_supermajority_intersect_calculation :
forall x y z,
x >= z - 2 * z / 3
-> y > 2 * z / 3
-> x + y - z > 0.
Lemma four_thirds_le :
forall n,
n > 1 -> two_thirds n + two_thirds n >= n.
Lemma two_thirds_lt :
forall n, n > 0 -> n > two_thirds n.
Lemma majority_complement :
forall x y,
one_half (x + y) < x
-> y <= one_half (x + y).
Lemma half_supermajority :
forall x y z,
x + y > two_thirds z
-> x >= y
-> x >= one_third z.
Lemma two_thirds_mono :
forall x y, x <= y -> two_thirds x <= two_thirds y.
Lemma one_third_mono :
forall x y, x <= y -> one_third x <= one_third y.
Lemma div3_one_third :
forall x,
one_third x <= S (x / 3).
Messy!
Lemma two_thirds_shift :
forall x y,
0 < y
-> x * two_thirds y < y * S (two_thirds x).
Lemma two_thirds_of_three :
forall x,
x >= 3
-> two_thirds x >= 2.
Lemma average_range :
forall x y, x <= y -> x <= (x + y) / 2 <= y.
Lemma one_half_plus_two :
forall x, (2 + x) / 2 = S (x / 2).
Lemma atleasthalf_le_all :
forall n,
S n / 2 <= n.
Lemma under_half_complement :
forall m n,
m < S n / 2
-> S n / 2 <= n - m.
forall x y,
0 < y
-> x * two_thirds y < y * S (two_thirds x).
Lemma two_thirds_of_three :
forall x,
x >= 3
-> two_thirds x >= 2.
Lemma average_range :
forall x y, x <= y -> x <= (x + y) / 2 <= y.
Lemma one_half_plus_two :
forall x, (2 + x) / 2 = S (x / 2).
Lemma atleasthalf_le_all :
forall n,
S n / 2 <= n.
Lemma under_half_complement :
forall m n,
m < S n / 2
-> S n / 2 <= n - m.