PFAD3章最初の，fが狭義単調増加関数ならx ≤ f x y かつ y ≤ f x y という部分の証明

PFAD3.agda

module PFAD3 where

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Function

infixr 2 _かつ_
_かつ_ = _×_

1引数関数_が狭義単調増加 : (f : ℕ → ℕ) → Set
1引数関数 f が狭義単調増加 = ∀ {x₁ x₂} → x₁ < x₂ → f x₁ < f x₂

2引数関数_が狭義単調増加 : (f : ℕ → ℕ → ℕ) → Set
2引数関数 f が狭義単調増加 = fx?が狭義単調増加 かつ f?yが狭義単調増加
  where
    fx?が狭義単調増加 = ∀ {x} → 1引数関数 f x が狭義単調増加
    f?yが狭義単調増加 = ∀ {y} → 1引数関数 flip f y が狭義単調増加

1引数関数が狭義単調増加なら関数適用により増加 : ∀ {x f} → 1引数関数 f が狭義単調増加 → x ≤ f x
1引数関数が狭義単調増加なら関数適用により増加 {zero} {f} 1引数関数fが狭義単調増加 = z≤n
1引数関数が狭義単調増加なら関数適用により増加 {suc x} {f} 1引数関数fが狭義単調増加 =
  begin
    suc x
  ≤⟨ s≤s (1引数関数が狭義単調増加なら関数適用により増加 1引数関数fが狭義単調増加) ⟩
    suc (f x)
  ≤⟨ 1引数関数fが狭義単調増加 (s≤s (1引数関数が狭義単調増加なら関数適用により増加 id)) ⟩
    f (suc x)
  ∎
  where
    open ≤-Reasoning

2引数関数が狭義単調増加なら関数適用により増加 : ∀ {x y f} → 2引数関数 f が狭義単調増加 → x ≤ f x y かつ y ≤ f x y
2引数関数が狭義単調増加なら関数適用により増加 {x} {y} {f} (fx?が狭義単調増加 , f?yが狭義単調増加) =
  1引数関数が狭義単調増加なら関数適用により増加 f?yが狭義単調増加 ,
  1引数関数が狭義単調増加なら関数適用により増加 fx?が狭義単調増加