{-# OPTIONS --cubical-compatible #-}
module Padova2025.ComputationalContent.Dickson where

Case study: Dickson’s lemma

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Termination.Ordering
import Padova2025.ComputationalContent.DoubleNegation
import Padova2025.ComputationalContent.Fictions.Minima

The purpose of this module is to give a constructive proof of (a baby version of) Dickson’s lemma, using a constructively preposterous assertion as a central ingredient, namely the claim that every function ℕ → ℕ has a minimum.

In its basic form, Dickson’s lemma states that for every map α : ℕ → ℕ, there is a number i such that α i ≤ α (succ i).

Dickson : (ℕ → ℕ) → Set
Dickson α = Σ[ i ∈ ℕ ] α i ≤ α (succ i)

theorem : (α : ℕ → ℕ) → Dickson α
theorem α = escape do
  (i , p) ← minimum α
  q       ← p (succ i)
  return (i , q)
  where
  open Padova2025.ComputationalContent.DoubleNegation  (Dickson α)
  open Padova2025.ComputationalContent.Fictions.Minima (Dickson α)
-- Equivalently:
-- theorem α = escape (minimum f ⟫= λ (i , p) → p (succ i) ⟫= λ fi≤fsucci → return (i , fi≤fsucci))
--   where
--   open Padova2025.ComputationalContent.DoubleNegation  (Dickson α)
--   open Padova2025.ComputationalContent.Fictions.Minima (Dickson α)