recognize

formal source

  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
  69    simp only [Set.mem_diff, Set.mem_singleton_iff, not_and, not_not]
  70    intro _
  71    trivial
  72  future_not_verified := by
  73    intro p hp hv
  74    simp only [Set.mem_diff, Set.mem_singleton_iff] at hp
  75    simp only [Set.mem_union, Set.mem_singleton_iff] at hv
  76    cases hv with
  77    | inl h => exact s.future_not_verified p hp.1 h
  78    | inr h =>
  79      -- p = s.current, but hp says p ∈ s.unverified \ {next}
  80      -- So p ∈ s.unverified. But s.current ∉ s.unverified by current_not_in_future
  81      rw [h] at hp
  82      exact s.current_not_in_future hp.1
  83}