pred

formal source

  55  | outside => inside
  56
  57/-- Cyclic predecessor. -/
  58def pred (v : Vantage) : Vantage :=
  59  match v with
  60  | inside  => outside
  61  | act     => inside
  62  | outside => act
  63
  64theorem succ_pred_id (v : Vantage) : succ (pred v) = v := by
  65  cases v <;> rfl
  66
  67theorem pred_succ_id (v : Vantage) : pred (succ v) = v := by
  68  cases v <;> rfl
  69
  70/-- Three applications of succ returns to start. -/
  71theorem succ_succ_succ (v : Vantage) : succ (succ (succ v)) = v := by
  72  cases v <;> rfl
  73
  74end Vantage
  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