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
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78

import CaseStudies.Velvet.Std

set_option loom.semantics.termination "total"
set_option loom.semantics.choice "demonic"

method lsb (i : ℕ) return (j : ℕ)
  require 0 < i
  ensures 0 < j ∧ j ≤ i
  do
    if 0 < i ∧ 2 ∣ i then
      let res ← lsb (i / 2)
      return 2 * res
    else
      return 1
prove_correct lsb
by loom_solve

lemma lsb_add (i : ℕ) (hi : 0 < i) :
    let j := lsb i |>.extract
    let k := lsb (i + j) |>.extract
    2 * j ≤ k := by
  by_cases h : 0 < i ∧ 2 ∣ i
  · have := lsb_add (i / 2) (by grind)
    simp at this
    have : (lsb i).extract = 2 * (lsb (i / 2)).extract := by sorry
    simp [this]
    grind

  · have : (lsb i).extract = 1 := by sorry
    simp [this]
    grind






method GCD (a : Nat) (b : Nat) return (res : Nat)
  require a > 0
  ensures res > 0
  do
    if b = 0 then
      return a
    else
      let remainder := a % b
      let result ← GCD b remainder
      return result
  termination_by b
  decreasing_by
    apply Nat.mod_lt
    grind

attribute [solverHint] Nat.mod_lt

prove_correct GCD
termination_by b
decreasing_by all_goals(
  apply Nat.mod_lt
  grind
  )
by
  loom_solve



method Minimum (a: Int) (b: Int) return (minValue: Int)
    ensures minValue ≤ a
    ensures minValue ≤ b
    ensures minValue = a ∨ minValue = b
    do
    if a ≤ b then
        assert a - 1 ≤ b
        return a
    else
        return b

prove_correct Minimum by
  loom_solve