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.