nat.agda

nat.agda

module nat where

data Nat : Set where  -- 項
  zero : Nat          -- zero
  succ : Nat → Nat    -- succ

-- 自然数の例
n0 = zero
n1 = succ zero
n2 = succ (succ zero)
n3 = succ (succ (succ zero))
n4 = succ (succ (succ (succ zero)))

-- 足し算の計算規則 (述語定義) 操作的意味
data _+_is_ : Nat → Nat → Nat → Set where
  EPlusZero : ∀ {N}
      ---------------
    → N + zero is N

  EPlusSucc : ∀ {M N P}
    → M + N is P
      ----------------------
    → M + succ N is (succ P)

-- 足し算の証明例 証明木が操作的意味
plus-n0+n0 : n0 + n0 is n0
plus-n0+n0 = EPlusZero
plus-n0+n1 : n1 + n0 is n1
plus-n0+n1 = EPlusZero
plus-n0+n2 : n2 + n0 is n2
plus-n0+n2 = EPlusZero
plus-n1+n0 : n0 + n1 is n1
plus-n1+n0 = EPlusSucc EPlusZero
plus-n1+n1 : n1 + n1 is n2
plus-n1+n1 = EPlusSucc EPlusZero
plus-n1+n2 : n2 + n1 is n3
plus-n1+n2 = EPlusSucc EPlusZero
plus-n2+n0 : n0 + n2 is n2
plus-n2+n0 = EPlusSucc (EPlusSucc EPlusZero)
plus-n2+n1 : n1 + n2 is n3
plus-n2+n1 = EPlusSucc (EPlusSucc EPlusZero)
plus-n2+n2 : n2 + n2 is n4
plus-n2+n2 = EPlusSucc (EPlusSucc EPlusZero)

-- 掛け算の計算規則 (述語定義) 操作的意味
data _*_is_ : Nat → Nat → Nat → Set where
  ETimesZero : ∀ {N}
      ---------------
    → N * zero is zero

  ETimesOne : ∀ {N}
      ----------------------
    → N * succ zero is N

  ETimesSucc : ∀ {M N P Q}
    → M * N is P → P + M is Q
      ----------------------
    → M * succ N is Q

-- 掛け算の証明例 証明木が操作的意味
times-n0-n0 : n0 * n0 is n0
times-n0-n0 = ETimesZero
times-n1-n0 : n1 * n0 is n0
times-n1-n0 = ETimesZero
times-n2-n0 : n2 * n0 is n0
times-n2-n0 = ETimesZero
times-n0-n1 : n0 * n1 is n0
times-n0-n1 = ETimesOne
times-n1-n1 : n1 * n1 is n1
times-n1-n1 = ETimesOne
times-n2-n1 : n2 * n1 is n2
times-n2-n1 = ETimesOne
times-n0-n2 : n0 * n2 is n0
times-n0-n2 = ETimesSucc ETimesOne EPlusZero
times-n1-n2 : n1 * n2 is n2
times-n1-n2 = ETimesSucc ETimesOne (EPlusSucc EPlusZero)
times-n2-n2 : n2 * n2 is n4
times-n2-n2 = ETimesSucc ETimesOne (EPlusSucc (EPlusSucc EPlusZero))

-- 補題1: zero + N is N
-- （意味論についての性質 = メタ理論） 操作的意味
EPlusZeroL : ∀ {N} → zero + N is N
-- 証明：Nat に関する構造的帰納法
-- （証明手法はメタレベル）証明木だけど操作的意味ではない
EPlusZeroL {zero} = EPlusZero
EPlusZeroL {succ N} = EPlusSucc EPlusZeroL

-- 補題2: succ M + N is succ P
-- （意味論についての性質 = メタ理論） 操作的意味
EPlusSuccL : ∀ {M N P}
  → M + N is P
    ----------------------
  → succ M + N is succ P
-- 証明：Nat に関する構造的帰納法
-- （証明手法はメタレベル）証明木だけど操作的意味ではない
EPlusSuccL EPlusZero = EPlusZero
EPlusSuccL (EPlusSucc p) = EPlusSucc (EPlusSuccL p)

-- 交換法則: M + N is P → N + M is P
-- （意味論についての性質 = メタ理論） 操作的意味
EPlusComm : ∀ {M N P}
  → M + N is P
    -------------
  → N + M is P
-- 証明：Nat に関する構造的帰納法
-- （証明手法はメタレベル）証明木だけど操作的意味ではない
EPlusComm EPlusZero = EPlusZeroL
EPlusComm (EPlusSucc p) = EPlusSuccL (EPlusComm p)

-- 依存対 (Σ型) と直積
data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

infixr 4 _×_
data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

-- 任意の N, K について「ある結果 R が存在して N + K is R」を構成
plusBuild : (N K : Nat)
    -------------------------
  → Σ Nat (λ R → N + K is R)
-- 証明：Nat に関する構造的帰納法
plusBuild N zero = N , EPlusZero
plusBuild N (succ K) with plusBuild N K
... | R , p = succ R , EPlusSucc p

-- 補助: M+N is P, P+K is Q, N+K is R から M+R is Q を構成
assocMR :
  ∀ {M N K P Q R}
  → M + N is P → P + K is Q
    -----------------------
  → N + K is R → M + R is Q
-- 証明：Nat に関する構造的帰納法
assocMR p EPlusZero EPlusZero = p
assocMR p (EPlusSucc q) (EPlusSucc nk') =
  EPlusSucc (assocMR p q nk')

-- 加算の結合法則
-- M + N is P, P + K is Q から、ある R が存在して
--   N + K is R かつ M + R is Q
EPlusAssoc :
  ∀ {M N K P Q}
  → M + N is P → P + K is Q
    -------------------
  → Σ Nat (λ R → (N + K is R) × (M + R is Q))
-- 証明：Nat に関する構造的帰納法
EPlusAssoc {M} {N} {K} p q with plusBuild N K
... | R , nk = R , ( nk , assocMR p q nk )


ETimesZeroL : ∀ {N}
    -------------------
  → zero * N is zero
ETimesZeroL {zero} = ETimesZero
ETimesZeroL {succ N} = ETimesSucc ETimesZeroL EPlusZero

-- 補題: N * succ zero is N を左右反転（one の左版）
ETimesOneL : ∀ {N}
    -------------------
  → succ zero * N is N
ETimesOneL {zero} = ETimesZero
ETimesOneL {succ N} =
  -- succ zero * succ N = (succ zero * N) + succ zero
  -- 帰納法で構成
  ETimesSucc (ETimesOneL {N}) (EPlusSucc EPlusZero)

-- 補題: 左側に succ を付けるための補題
-- M * N is P と P + N is Q から succ M * N is Q
ETimesSuccL :
  ∀ {M N P Q}
  → M * N is P → P + N is Q
    ----------------------
  → succ M * N is Q
-- ケース 1: N = zero のとき
-- P = zero, Q = zero となるため、EPlusZero が自然にマッチします。
ETimesSuccL ETimesZero EPlusZero = ETimesZero
-- ケース 2: N = succ zero のとき
-- M * succ zero is M なので P = M。
-- 第2引数は M + succ zero is Q となり、EPlusSucc EPlusZero にマッチして Q = succ M となります。
-- 目標は succ M * succ zero is succ M となるため、そのまま ETimesOne で証明完了です。
ETimesSuccL ETimesOne (EPlusSucc EPlusZero) = ETimesOne
-- ケース 3: N = succ N' のとき
ETimesSuccL (ETimesSucc p q1) (EPlusSucc q2) with EPlusAssoc (EPlusComm q1) q2
... | X , (p_n , m_x) =
    ETimesSucc (ETimesSuccL p p_n) (EPlusSucc (EPlusComm m_x))

-- 乗算の交換法則: M * N is P → N * M is P
-- （意味論についての性質 = メタ理論）
-- 乗算の交換法則
ETimesComm : ∀ {M N P}
  → M * N is P
    ------------
  → N * M is P
-- ケース 1: 右辺が zero (M * 0 is 0)
-- 結果は 0 * M is 0 なので ETimesZeroL
ETimesComm ETimesZero = ETimesZeroL
-- ケース 2: 右辺が succ zero (M * 1 is M)
-- 結果は 1 * M is M なので ETimesOneL
ETimesComm ETimesOne = ETimesOneL
-- ケース 3: 右辺が succ N (M * succ N is Q)
-- p : M * N is P
-- q : P + M is Q
-- 帰納法 r : N * M is P を使って、ETimesSuccL で succ N * M is Q を作る
ETimesComm (ETimesSucc p q) = ETimesSuccL (ETimesComm p) q