`chooseCandidate`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.Atomicity
domain: Foundation
line: 332 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.Atomicity on GitHub at line 332.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 329  · simpa [hn]
 330  · simpa [hn] using helig
 331
 332noncomputable def chooseCandidate (picked : Finset E.Event) :
 333    Option (Candidate (ev:=ev) (E:=E) picked) :=
 334  if h : ∃ e, e ∉ picked then
 335    let hx := exists_candidate_index (ev:=ev) (E:=E) picked h
 336    let n := Nat.find hx
 337    let hn := Nat.find_spec hx
 338    let e := enum (E:=E) n
 339    some
 340      { idx := n
 341      , event := e
 342      , event_def := rfl
 343      , not_mem := hn.left
 344      , eligible_event := hn.right }
 345  else
 346    none
 347
 348lemma chooseCandidate_none_iff (picked : Finset E.Event) :
 349    chooseCandidate (ev:=ev) (E:=E) picked = none ↔
 350      ¬∃ e, e ∉ picked := by
 351  classical
 352  unfold chooseCandidate
 353  split_ifs with h
 354  · simp [h]
 355  · simp [h]
 356
 357lemma chooseCandidate_some_spec {picked : Finset E.Event}
 358    {c : Candidate (ev:=ev) (E:=E) picked}
 359    (h : chooseCandidate (ev:=ev) (E:=E) picked = some c) :
 360    c.not_mem ∧ eligible (ev:=ev) picked c.event := by
 361  classical
 362  unfold chooseCandidate at h

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.