/usr/share/agda-stdlib/Induction/Lexicographic.agda is in agda-stdlib 0.7-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic induction
------------------------------------------------------------------------
module Induction.Lexicographic where
open import Induction
open import Data.Product
-- The structure of lexicographic induction.
Σ-Rec : ∀ {ℓ} {A : Set ℓ} {B : A → Set ℓ} →
RecStruct A → (∀ x → RecStruct (B x)) → RecStruct (Σ A B)
Σ-Rec RecA RecB P (x , y) =
-- Either x is constant and y is "smaller", ...
RecB x (λ y' → P (x , y')) y
×
-- ...or x is "smaller" and y is arbitrary.
RecA (λ x' → ∀ y' → P (x' , y')) x
_⊗_ : ∀ {ℓ} {A B : Set ℓ} →
RecStruct A → RecStruct B → RecStruct (A × B)
RecA ⊗ RecB = Σ-Rec RecA (λ _ → RecB)
-- Constructs a recursor builder for lexicographic induction.
Σ-rec-builder :
∀ {ℓ} {A : Set ℓ} {B : A → Set ℓ}
{RecA : RecStruct A}
{RecB : ∀ x → RecStruct (B x)} →
RecursorBuilder RecA → (∀ x → RecursorBuilder (RecB x)) →
RecursorBuilder (Σ-Rec RecA RecB)
Σ-rec-builder {RecA = RecA} {RecB = RecB} recA recB P f (x , y) =
(p₁ x y p₂x , p₂x)
where
p₁ : ∀ x y →
RecA (λ x' → ∀ y' → P (x' , y')) x →
RecB x (λ y' → P (x , y')) y
p₁ x y x-rec = recB x
(λ y' → P (x , y'))
(λ y y-rec → f (x , y) (y-rec , x-rec))
y
p₂ : ∀ x → RecA (λ x' → ∀ y' → P (x' , y')) x
p₂ = recA (λ x → ∀ y → P (x , y))
(λ x x-rec y → f (x , y) (p₁ x y x-rec , x-rec))
p₂x = p₂ x
[_⊗_] : ∀ {ℓ} {A B : Set ℓ} {RecA : RecStruct A} {RecB : RecStruct B} →
RecursorBuilder RecA → RecursorBuilder RecB →
RecursorBuilder (RecA ⊗ RecB)
[ recA ⊗ recB ] = Σ-rec-builder recA (λ _ → recB)
------------------------------------------------------------------------
-- Example
private
open import Data.Nat
open import Induction.Nat as N
-- The Ackermann function à la Rózsa Péter.
ackermann : ℕ → ℕ → ℕ
ackermann m n =
build [ N.rec-builder ⊗ N.rec-builder ]
(λ _ → ℕ)
(λ { (zero , n) _ → 1 + n
; (suc m , zero) (_ , ackm•) → ackm• 1
; (suc m , suc n) (ack[1+m]n , ackm•) → ackm• ack[1+m]n
})
(m , n)
|