Library Famous

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

Require Import Nat.
Require Import Bool.
Require Import List.
Require Import Omega.

Require Import Tact.
Require Import Relation.
Require Import Decide.
Require Import Weight.
Require Import Calculate.
Require Import Majority.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.
Require Import Vote.
Require Import Decision.
Require Import Consensus.

Definition famous (s : sample) (W : world) (x : event) : Prop :=
  exists y, member W y /\ decision s x y true.

Definition fwitness s W i x :=
  rwitness i x
  /\ famous s W x.

Lemma extends_famous :
   forall s W W' x,
     extends W W'
     -> famous s W x
     -> famous s W' x.

Lemma fame_reaches_every_world :
  forall s W W' x,
    extends W W'
    -> nonterminating W
    -> famous s W' x
    -> famous s W x.

Lemma famous_decide_finite :
  forall s W x,
    finite (member W)
    -> decidable (famous s W x).

Lemma famous_decide_nonterm :
  forall s W x,
    extends W (global s)
    -> nonterminating W
    -> member W x
    -> witness x
    -> decidable (famous s W x).

Lemma elector_cardinality :
  forall i y,
    exists n, weight creatorstake (fun x => elector i x y) n.

Lemma no_true_votes_election :
  forall s i x y t f,
    (forall z, z @ y -> ~ vote s x z true)
    -> election (vote s x) i y t f
    -> t = 0.

Lemma unknown_event_vote :
  forall s x y,
    ~ x @= y
    -> ~ vote s x y true.
first
Lemma no_late_fame :
  forall s i x y w b,
    rwitness i x
    -> rwitness i y
    -> decision s x w b
    -> ~ y @= w
    -> decision s y w false.

Lemma 5.18
Corollary no_late_fame_world :
  forall s W i x y w b,
    member W w
    -> ~ member W y
    -> rwitness i x
    -> rwitness i y
    -> decision s x w b
    -> decision s y w false.

Lemma decision_ancestor :
  forall s x y,
    decision s x y true
    -> x @= y.

Lemma famous_member :
  forall s W x,
    famous s W x
    -> member W x.