Let's play Agda 
{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ComputationalContent.Fictions.Minima (⊥ : Set) where

最小值#

open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Base
open import Padova2025-zh-TW.ProvingBasics.Termination.Ordering
open import Padova2025-zh-TW.ProvingBasics.Termination.WellFounded.Base
open import Padova2025-zh-TW.ProvingBasics.Connectives.Disjunction
open import Padova2025-zh-TW.ProvingBasics.Connectives.Existential
open import Padova2025-zh-TW.ProvingBasics.Connectives.Conjunction
open import Padova2025-zh-TW.ComputationalContent.DoubleNegation (⊥)

函數在雙重否定意義下的最小值#

習題 1go
go : (α : ℕ → ℕ) → (i : ℕ) → Acc _<'_ (α i) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
go α i (acc f) = oracle {Σ[ j ∈ ℕ ] α j < α i} ⟫= λ
  { (left  (j , p)) → {!!}
  ; (right q)       → {!!}
  }
  where
  h : ¬ (Σ[ j ∈ ℕ ] α j < α i) → (j : ℕ) → ¬ ¬ (α i ≤ α j)
  h q j with ≤-<-connex (α i) (α j)
  ... | left  αi≤αj = {!!}
  ... | right αj<αi = {!!}
參考解答用到： <⇒<' return ⊥-elim
參考解答
go : (α : ℕ → ℕ) → (i : ℕ) → Acc _<'_ (α i) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
go α i (acc f) = oracle {Σ[ j ∈ ℕ ] α j < α i} ⟫= λ
  { (left  (j , p)) → go α j (f (<⇒<' p))
  ; (right q)       → return (i , h q)
  }
  where
  h : ¬ (Σ[ j ∈ ℕ ] α j < α i) → (j : ℕ) → ¬ ¬ (α i ≤ α j)
  h q j with ≤-<-connex (α i) (α j)
  ... | left  αi≤αj = return αi≤αj
  ... | right αj<αi = ⊥-elim (q (j , αj<αi))
習題 2minimum
minimum : (α : ℕ → ℕ) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
minimum = {!!}
參考解答用到： go zero ℕ-wf
參考解答
minimum : (α : ℕ → ℕ) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
minimum α = go α zero (ℕ-wf (α zero))

有居民的自然數集合的變體#

習題 3go'
go' : (P : ℕ → Set) (n : ℕ) → P n → Acc _<'_ n → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
go' = {!!}
參考解答用到： acc _,_ <⇒<'
參考解答
go' : (P : ℕ → Set) (n : ℕ) → P n → Acc _<'_ n → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
go' P n Pn (acc f) k = k (n , Pn , λ b b<n Pb → go' P b Pb (f (<⇒<' b<n)) k)
習題 4minimum'
minimum' : (P : ℕ → Set) → (∃[ n ] P n) → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
minimum' = {!!}
參考解答用到： _,_ go' ℕ-wf
參考解答
minimum' : (P : ℕ → Set) → (∃[ n ] P n) → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
minimum' P (n , Pn) = go' P n Pn (ℕ-wf n)

最大的自然數？#

請仔細思考下面這段程式碼，它宣稱在雙重否定的意義下證明了存在最大的自然數。它是如何嘗試運作的？Agda 為什麼會拒絕它？

largest-number : ¬ ¬ (Σ[ a ∈ ℕ ] ((b : ℕ) → ¬ ¬ a ≥ b))
largest-number = f zero
  where
  f : ℕ → ¬ ¬ (Σ[ a ∈ ℕ ] ((b : ℕ) → ¬ ¬ a ≥ b))
  f a k = k (a , h)
    where
    h : (b : ℕ) → ¬ ¬ a ≥ b
    h b with ≤-<-connex b a
    ... | left  b≤a = return m≤n
    ... | right a<b = λ k' → f b k
習題 5lemma
lemma : {x : ℕ} → succ x ≤ x → ⊥
lemma = {!!}
參考解答用到： s≤s
參考解答
lemma : {x : ℕ} → succ x ≤ x → ⊥
lemma (s≤s p) = lemma p
習題 6no-largest-number
no-largest-number : ¬ (¬ ¬ (∃[ a ] ((b : ℕ) → ¬ ¬ b ≤ a)))
no-largest-number = {!!}
參考解答用到： escape _,_ succ return lemma
參考解答
no-largest-number : ¬ (¬ ¬ (∃[ a ] ((b : ℕ) → ¬ ¬ b ≤ a)))
no-largest-number m = escape do
  (a , f) ← m
  absurd  ← f (succ a)
  return (lemma absurd)