OAI/Combinatorics/ParityLifts/ListPrograms.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.Complexity.PolyProgram.recode line 7
  2. def OAI.ParityWL.Complexity.PolyProgram.tabulate line 18
  3. def OAI.ParityWL.Complexity.PolyProgram.filterWith line 28
  4. def OAI.ParityWL.Complexity.PolyProgram.mem line 37
  5. def OAI.ParityWL.Complexity.PolyProgram.subset line 49
  6. lemma OAI.ParityWL.Complexity.fold_dedup_append line 56
  7. def OAI.ParityWL.Complexity.dedupList line 66
  8. lemma OAI.ParityWL.Complexity.dedupList_toFinset line 69
  9. def OAI.ParityWL.Complexity.PolyProgram.dedup line 72
  10. def OAI.ParityWL.Complexity.findIndex line 87

    Source documentation

    First-index search, expressed by one polynomial fold rather than an oracle.

    def findIndex {α : Type} (p : α → Bool) (xs : List α) : ℕ := xs.takeWhile (fun x => !p x) |>.length
  11. lemma OAI.ParityWL.Complexity.findIndex_nil line 89
  12. lemma OAI.ParityWL.Complexity.findIndex_cons line 90
  13. lemma OAI.ParityWL.Complexity.fold_findIndex line 94
  14. lemma OAI.ParityWL.Complexity.findIndex_eq_length line 103
  15. lemma OAI.ParityWL.Complexity.findIndex_le line 111
  16. def OAI.ParityWL.Complexity.PolyProgram.findIndexWith line 114