T2_atomicity

formal source

  78  postedAt : Nat → M.U → Prop
  79  unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u
  80
  81theorem T2_atomicity {M} [AtomicTick M] :
  82  ∀ t u v, AtomicTick.postedAt (M:=M) t u → AtomicTick.postedAt (M:=M) t v → u = v := by
  83  intro t u v hu hv
  84  rcases (AtomicTick.unique_post (M:=M) t) with ⟨w, hw, huniq⟩
  85  have huw : u = w := huniq u hu
  86  have hvw : v = w := huniq v hv
  87  exact huw.trans hvw.symm
  88
  89end Recognition
  90
  91namespace Demo
  92
  93open Recognition
  94
  95structure U where
  96  a : Unit
  97
  98/-- Recognition relation by structural equality -/
  99def recog : U → U → Prop := fun x y => x = y
 100
 101def M : RecognitionStructure := { U := U, R := recog }
 102
 103def L : Ledger M := { debit := fun _ => 1, credit := fun _ => 1 }
 104
 105def twoStep : Chain M :=
 106  { n := 1
 107  , f := fun _ => ⟨()⟩
 108  , ok := by intro i; trivial }
 109
 110example : chainFlux L twoStep = 0 := by
 111  have hbal : ∀ u, L.debit u = L.credit u := by intro _; rfl