Library Median

Copyright (c) 2018 by Swirlds, Inc. Implemented by Karl Crary.

Require Import Nat.
Require Import Bool.
Require Import Omega.
Require Import List.
Require Import Sorting.
Require Import Permutation.

Require Import Tact.
Require Import Decide.
Require Import Relation.
Require Import Weight.
Require Import Calculate.
Require Import Majority.

Lemma Forall_app :
  forall (A : Type) (P : A -> Prop) (l m : list A),
    Forall P l
    -> Forall P m
    -> Forall P (l ++ m).

Lemma NoDup_app_invert :
  forall T (l1 l2 : list T),
    NoDup (l1 ++ l2)
    -> NoDup l1 /\ NoDup l2.
Lemma sorted_unique :
  forall (U : Type) (R : U -> U -> Prop),
    order U R
    -> (forall x y, R x y \/ R y x)
    -> (forall x y, decidable (R x y))
    -> forall (l m : list U),
         Sorted R l
         -> Sorted R m
         -> Permutation l m
         -> l = m.
nil
Lemma map_sorted :
  forall (T U : Type) (R : U -> U -> Prop) (f : T -> U) (l : list T),
    Sorted (fun x y => R (f x) (f y)) l
    -> Sorted R (map f l).
Lemma sorted_impl :
  forall T R R' l,
    inclusion T R R'
    -> Sorted R l
    -> Sorted R' l.

Lemma strongly_sorted_app_inv :
  forall T (R : T -> T -> Prop) (l m : list T),
    StronglySorted R (l ++ m)
    -> forall x y,
         In x l
         -> In y m
         -> R x y.
Lemma strongly_sorted_remove_middle :
  forall T (R : T -> T -> Prop) (l : list T) (x : T) (m : list T),
    StronglySorted R (l ++ x :: m)
    -> StronglySorted R (l ++ m).
Module Type WEIGHT_AND_VALUE.

Parameter T : Type.
Parameter U : Type.

Axiom eqT_decide : forall (x y : T), decidable (x = y).

Parameter wt : T -> nat.
Parameter vl : T -> U.

Axiom wt_pos : forall x, wt x > 0.

Parameter lebU : U -> U -> bool.

Axiom lebU_order : order U (fun x y => lebU x y = true).
Axiom lebU_total : forall x y, lebU x y = true \/ lebU y x = true.

Parameter inh : U.

End WEIGHT_AND_VALUE.

Module MedianFun (Import X:WEIGHT_AND_VALUE).

Module TOrder.

Definition t := T.

Definition leb (x y : T) := X.lebU (vl x) (vl y).

Lemma leb_total : forall (x y : T), leb x y = true \/ leb y x = true.

End TOrder.

Module TSort := Sort TOrder.

Definition leU (x y : U) : Prop := lebU x y = true.
Definition leT (x y : T) : Prop := leU (vl x) (vl y).

Fixpoint sselect (l : list T) (n : nat) {struct l} : U :=
  match l with
  | nil => X.inh
  | cons x l' =>
      if ltb n (wt x) then
        vl x
      else
        sselect l' (n - wt x)
  end.

Fixpoint select (l : list T) (n : nat) {struct l} : U :=
  match l with
  | nil => X.inh
  | cons x l' =>
      if leb n (wt x) then
        vl x
      else
        select l' (n - wt x)
  end.

Definition median (l : list T) : U :=
  select (TSort.sort l) (S (sumweight wt l) / 2).

Lemma tsort_sorted :
  forall l,
    Sorted leT (TSort.sort l).
The lemmas Sorted_sort and LocallySorted_sort are reversed in the library.

Lemma leU_order : order U leU.

Lemma leU_total : forall x y, leU x y \/ leU y x.

Lemma leU_decide : forall x y, decidable (leU x y).

Lemma eqU_decide : forall (x y : U), decidable (x = y).

Lemma sselect_prefix :
  forall l m n x,
    Forall (fun y => x = vl y) l
    -> n < sumweight wt l
    -> sselect (l ++ m) n = x.
Lemma sselect_cons_r :
  forall (x : T) (l : list T) n,
    sselect (x :: l) (wt x + n) = sselect l n.

Lemma sselect_app_r :
  forall (l m : list T) n,
    sselect (l ++ m) (sumweight wt l + n) = sselect m n.
Lemma sselect_lift :
  forall (l : list T) (x : T) (m : list T),
    Forall (fun y => vl x = vl y) l
    -> forall n, sselect (l ++ x :: m) n = sselect (x :: l ++ m) n.

Lemma Transitive_leT : Relations_1.Transitive leT.

Lemma sselect_unique :
  forall (l m : list T) (n : nat),
    Sorted leT l
    -> Sorted leT m
    -> Permutation l m
    -> sselect l n = sselect m n.
Lemma sselect_eq_select :
  forall l n,
    sselect l n = select l (S n).
Lemma select_unique :
  forall (l m : list T) (n : nat),
    Sorted leT l
    -> Sorted leT m
    -> Permutation l m
    -> select l n = select m n.

Lemma median_unique :
  forall (l m : list T),
    Permutation l m
    -> median l = median m.

Lemma select_spec :
  forall (l : list T) (n : nat),
    0 < n
    -> n <= sumweight wt l
    -> exists l1 x l2,
         l = l1 ++ x :: l2
         /\ select l n = vl x
         /\ sumweight wt l1 < n
         /\ n <= sumweight wt (l1 ++ x :: nil).
Lemma median_spec :
  forall (l : list T),
    length l > 0
    -> NoDup l
    -> exists x m n,
         median l = vl x
         /\ In x l
         /\ weight wt (fun y => In y l /\ leT y x) m
         /\ S (sumweight wt l) / 2 <= m
         /\ weight wt (fun y => In y l /\ leT x y) n
         /\ S (sumweight wt l) / 2 <= n.

Lemma majority_median :
  forall (P : T -> Prop) (l : list T),
    NoDup l
    -> majority wt P (fun x => In x l)
    -> exists x y,
         P x
         /\ P y
         /\ leU (vl x) (median l)
         /\ leU (median l) (vl y).

End MedianFun.

Require Import Hashgraph.
Require Import HashgraphFacts.
Require Import Vote.

Module EventWeightAndValue.

Definition T := event.
Definition U := nat.

Definition eqT_decide := eq_event_decide.

Definition wt := creatorstake.
Definition vl := timestamp.

Lemma wt_pos : forall x, wt x > 0.

Definition lebU := Nat.leb.

Lemma lebU_order : order nat (fun x y => lebU x y = true).

Definition lebU_total := NatOrder.leb_total.

Definition inh := 0.

End EventWeightAndValue.

Module EventMedian := MedianFun EventWeightAndValue.

Export EventMedian.