Specify a maximum implementation

3/4 ~35 minlean

Prove that both inputs are below the result of `max2`.

7 lines · Lean 4

import Mathlib

def max2 (a b : Nat) : Nat := if a ≤ b then b else a

theorem max2_spec (a b : Nat) :
    a ≤ max2 a b ∧ b ≤ max2 a b := by
  sorry

Objectifs

Prove that both inputs are below the result of `max2`.

Indices

Voir la solution

import Mathlib

def max2 (a b : Nat) : Nat := if a ≤ b then b else a

theorem max2_spec (a b : Nat) :
    a ≤ max2 a b ∧ b ≤ max2 a b := by
  unfold max2
  split
  · constructor <;> omega
  · constructor <;> omega