Let's play Agda 
{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ComputationalContent.Blueprints.Minima where

最小值#

open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Base
open import Padova2025-zh-TW.ProvingBasics.Negation
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
postulate
  oracle : {A : Set} → A ⊎ ¬ A
習題 1go
go : (α : ℕ → ℕ) → (i : ℕ) → Acc _<'_ (α i) → Σ[ i ∈ ℕ ] ((j : ℕ) → α i ≤ α j)
go α i (acc f) with oracle {Σ[ j ∈ ℕ ] α j < α i}
... | left  (j , p) = {!!}
... | right q       = {!!}
  where
  h : (j : ℕ) → α i ≤ α j
  h j with ≤-<-connex (α i) (α j)
  ... | left  αi≤αj = {!!}
  ... | right αj<αi = {!!}
參考解答用到： <⇒<' ⊥-elim
參考解答
go : (α : ℕ → ℕ) → (i : ℕ) → Acc _<'_ (α i) → Σ[ i ∈ ℕ ] ((j : ℕ) → α i ≤ α j)
go α i (acc f) with oracle {Σ[ j ∈ ℕ ] α j < α i}
... | left  (j , p) = go α j (f (<⇒<' p))
... | right q       = (i , h)
  where
  h : (j : ℕ) → α i ≤ α j
  h j with ≤-<-connex (α i) (α j)
  ... | left  αi≤αj = α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))