ProofState

formal source

  35
  36The key invariant: past, present, and future are mutually disjoint.
  37-/
  38structure ProofState where
  39  /-- Verified propositions (the past). -/
  40  verified : Set Prop
  41  /-- Current proposition being verified (the present). -/
  42  current : Prop
  43  /-- Unverified candidates (the future). -/
  44  unverified : Set Prop
  45  /-- Current is not in past. -/
  46  current_not_in_past : current ∉ verified
  47  /-- Current is not in future (it's the present). -/
  48  current_not_in_future : current ∉ unverified
  49  /-- Future candidates are not yet verified. -/
  50  future_not_verified : ∀ p ∈ unverified, p ∉ verified
  51
  52/-- The recognition step: verify current, move to next. -/
  53def recognize (s : ProofState) (next : Prop)
  54    (h_next : next ∈ s.unverified)
  55    (h_next_ne : next ≠ s.current)
  56    (_h_current_true : s.current) : ProofState := {
  57  verified := s.verified ∪ {s.current},
  58  current := next,
  59  unverified := s.unverified \ {next},
  60  current_not_in_past := by
  61    simp only [Set.mem_union, Set.mem_singleton_iff]
  62    intro h
  63    cases h with
  64    | inl h => exact s.future_not_verified next h_next h
  65    | inr h => exact absurd h h_next_ne
  66  current_not_in_future := by
  67    -- Goal: next ∉ s.unverified \ {next}
  68    -- This is true because we remove next from s.unverified