1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34

import Std.Data.ExtHashSet
import Lean.Elab

def gensym (S : Std.ExtHashSet String) := Id.run do
  for i in List.range (S.size + 1) do
    if toString i ∉ S then
      return toString i
  return ""

open Std Do ExtHashSet in
/-- `gensym` returns a string not in its input set -/
theorem gensym_correct : gensym S ∉ S := by
  generalize h : gensym S = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · Invariant.withEarlyReturnNewDo
      (onReturn := fun ret () ↦ ⌜ret ∉ S⌝)
      (onContinue := fun xs () ↦ ⌜∀ i < xs.prefix.length, toString i ∈ S⌝)
  with (expose_names; try grind)
  · left
    simp_all
    intro i hi
    by_cases h : i = pref.length
    · grind [congrArg (·[pref.length]?) h_1]
    · exact h_3.2 i (by grind)
  · let T := List.range (List.range (S.size + 1) |>.length) |>.map toString
    have : S ∪ ofList T = S := by
      ext i -- This is why we need `ExtHashSet` instead of just `HashSet`
      constructor
      · simp_all
        grind
      · simp_all
    have : (ofList T).size = T.length := size_ofList (by simp [List.pairwise_iff_getElem, T]; grind)
    grind [size_right_le_size_union]