50. Verified maximum of two numbers
Write max2 : Nat → Nat → Nat and prove max2_spec : MaxSpec max2: the result is at least a, at least b, and equal to one of them.
Those three properties pin the maximum down completely, so no tests are needed. A function that returns a + b satisfies the first two but fails the third.
What the judge checks
max2_spec : MaxSpec max2The definitions these names refer to are the read-only lines above the editor. Write any helper lemmas you need before the final theorem.
1def MaxSpec (f : Nat → Nat → Nat) : Prop :=
2 ∀ a b, a ≤ f a b ∧ b ≤ f a b ∧ (f a b = a ∨ f 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