{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProgrammingBasics.Naturals.DecisionProcedures where

Decision procedures

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Booleans

This file contains a couple of decision procedures—functions which have the task of answering certain yes/no questions, such as: Is the given input number zero? Is it even?

We will later improve on the definitions suggested here. The issue is that the functions of this file do not actually return a witness (“yes, the number is zero, here is why” or “no, the number is not zero, here is why”) but instead merely a non-informative Boolean value (true or false).

Exercise: Equality checking

Define a function eq? which determines whether its two input numbers are equal. For instance, eq? three three should reduce to true while eq? three four should reduce to false.

eq? : ℕ → ℕ → Bool
eq? = {!!}

Exercise: Inequality checking

Define a function ≤? which determines whether its first argument is less than or equal to its second. For instance, ≤? two four should reduce to true while ≤? four two should reduce to false.

≤? : ℕ → ℕ → Bool
≤? = {!!}

Building on ≤?, we can implement a decision procedure for the strict less-than relation:

<? : ℕ → ℕ → Bool
<? a b = ≤? (succ a) b

Exercise: Even and odd numbers

Define a function even? which determines whether its input is even.

For instance, even? zero and even? two should both reduce to true, while even? three should evaluate to false.

even? : ℕ → Bool
even? = {!!}

Define a function odd? which determines whether its input is odd. You may use the even? function from before.

odd? : ℕ → Bool
odd? = {!!}