51. Verified distance between numbers
Write distance : Nat → Nat → Nat and prove distance_spec : DistanceSpec distance: it is symmetric, the distance from a number to itself is 0, and when a ≤ b, going distance a b up from a reaches b.
b - a alone is not enough: subtraction on Nat stops at zero, so it is not symmetric.
What the judge checks
distance_spec : DistanceSpec distanceThe definitions these names refer to are the read-only lines above the editor. Write any helper lemmas you need before the final theorem.
1def DistanceSpec (d : Nat → Nat → Nat) : Prop :=
2 (∀ a b, d a b = d b a) ∧ (∀ a, d a a = 0) ∧ (∀ a b, a ≤ b → a + d a b = b)
givenLoading editor…
Type
\to in the editor, or click:Run checks your code against the examples and your custom inputs and records nothing. Submit also runs the hidden tests, confirms the axioms your proof uses and records the result. Each uses one compiler check.
ReadyLn 1, Col 1Lean 4
Draft saved in this browser