OAI/Computability/QuantumFactoring/LoggedExecution.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ExactQuantumFactoring.Logged line 17

    Source documentation

    A bounded deterministic computation and the chronological requests it actually made. Failure retains its prefix and does not query later work.

    structure Logged (Q α : Type*) where
…
  2. def OAI.ExactQuantumFactoring.Logged.pure line 24
  3. def OAI.ExactQuantumFactoring.Logged.abort line 25
  4. def OAI.ExactQuantumFactoring.Logged.bind line 26
  5. def OAI.ExactQuantumFactoring.Logged.map line 30
  6. def OAI.ExactQuantumFactoring.Logged.Good line 31
  7. lemma OAI.ExactQuantumFactoring.Logged.good_bind_left line 33
  8. lemma OAI.ExactQuantumFactoring.Logged.good_bind_right line 40
  9. lemma OAI.ExactQuantumFactoring.Logged.bind_result_some line 45
  10. lemma OAI.ExactQuantumFactoring.Logged.map_result line 48
  11. lemma OAI.ExactQuantumFactoring.Logged.map_requests line 51
  12. lemma OAI.ExactQuantumFactoring.Logged.good_map line 54
  13. def OAI.ExactQuantumFactoring.Logged.traverse line 57
  14. lemma OAI.ExactQuantumFactoring.Logged.traverse_complete line 63

    Source documentation

    No hypothesis at unvisited requests: the induction uses the good prefix, obtains its successful result, then exposes the actual next prefix.

    lemma traverse_complete (P : Q→Prop) (f : α→Logged Q β) (g : α→β) (xs : List α)
    (hlocal : ∀ a∈xs, Good P (f a) → (f a).result=some (g a))
    (hg : Good P (traverse f xs)) : (traverse f xs).result=some (xs.map g) := by
…

    Mentions: OAI.ExactQuantumFactoring.Logged, OAI.ExactQuantumFactoring.Logged.Good, OAI.ExactQuantumFactoring.Logged.traverse

  15. lemma OAI.ExactQuantumFactoring.Logged.traverse_sound line 76