Library Sees

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

Require Import Decide.

Require Import Tact.
Require Import Relation.
Require Import Majority.
Require Import HashgraphFacts.

y sees x
Definition sees (x y : event) : Prop :=
  x @= y
  /\ ~ exists z z', z @= y /\ z' @= y /\ fork z z' /\ creator z = creator x.

y strongly sees x
Definition stsees (x y : event) : Prop :=
  exists w,
    w @= y
    /\ supermajority
         stake
         (fun a => exists z, creator z = a /\ sees x z /\ sees z w)
         every.

Lemma sees_impl_ancestor :
  forall x y, sees x y -> x @= y.

Lemma 5.12
Lemma strongly_seeing :
  forall W x y v w,
    member W v
    -> member W w
    -> fork x y
    -> stsees x v
    -> stsees y w
    -> False.

Lemma stsees_impl_strict_ancestor :
  forall x y, stsees x y -> x @ y.

Lemma stsees_impl_ancestor :
  forall x y, stsees x y -> x @= y.

Lemma sees_decide :
  forall x y,
    decidable (sees x y).

Lemma stsees_decide :
  forall x y,
    decidable (stsees x y).
Lemma self_ancestor_sees_trans :
  forall x y z,
    x $= y
    -> sees y z
    -> sees x z.

Lemma self_ancestor_stsees_trans :
  forall x y z,
    x $= y
    -> stsees y z
    -> stsees x z.

Lemma stsees_ancestor_trans :
  forall x y z,
    stsees x y
    -> y @= z
    -> stsees x z.

Lemma ancestor_sees :
  forall x y,
    honest (creator x)
    -> x @= y
    -> sees x y.