Kata

This Kata is a warm-up exercise for "Verified C array maximum" (coming soon).

Coq.Lists.List provides a built-in function list_max for computing the maximum natural number within a given list, or 0 if the list is empty; however, an equivalent function for integers is not present in the standard library.

Here, we present list_max_Z (list-max-ℤ in Agda), the integer equivalent of list_max which computes the maximum integer in a given list or 0 if all integers are negative. A specification for list_max_Z could be as follows:

1. No integer in the list exceeds the maximum returned by list_max_Z
2. The maximum returned by list_max_Z must appear in the list, or else it must be 0

Convince yourself that the above specification is complete, i.e. it fully describes the expected behavior of list_max_Z, and then proceed Your task is to prove it.

Preloaded

{-# OPTIONS --safe #-}
module Preloaded where

open import Data.List
open import Data.Integer

list-max-ℤ : List ℤ → ℤ
list-max-ℤ xs = foldr _⊔_ (+ 0) xs

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.ZArith.BinInt.
Open Scope Z_scope.

Definition list_max_Z : list Z -> Z := fold_right Z.max 0.

def list_max_Z : list ℤ → ℤ := list.foldr max 0