VantageTriple

formal source

  75
  76/-- A triple of values indexed by vantage.
  77    Used to express that X_inside, X_act, X_outside are the same underlying X. -/
  78structure VantageTriple (α : Type*) where
  79  inside  : α
  80  act     : α
  81  outside : α
  82
  83namespace VantageTriple
  84
  85/-- Project a value by vantage. -/
  86def get {α : Type*} (t : VantageTriple α) (v : Vantage) : α :=
  87  match v with
  88  | Vantage.inside  => t.inside
  89  | Vantage.act     => t.act
  90  | Vantage.outside => t.outside
  91
  92/-- A unified triple: all three vantages see the same value. -/
  93def unified {α : Type*} (x : α) : VantageTriple α :=
  94  { inside := x, act := x, outside := x }
  95
  96/-- Predicate: the triple is unified (all equal). -/
  97def isUnified {α : Type*} [DecidableEq α] (t : VantageTriple α) : Prop :=
  98  t.inside = t.act ∧ t.act = t.outside
  99
 100theorem unified_is_unified {α : Type*} [DecidableEq α] (x : α) :
 101    isUnified (unified x) := ⟨rfl, rfl⟩
 102
 103end VantageTriple
 104
 105end RRF.Core
 106end IndisputableMonolith