ネタ記録庫/Agda

 

Coqはこちら -> ネタ記録庫/Coq

Agdaで足し算のassociativityも証明してみた。 †

 -- theorem associative
 thm_plus_assoc : (n m p : Nat) -> eq (n + (m + p)) ((n + m) + p)
 thm_plus_assoc zero m p = thm_eq_refl (m + p)
 thm_plus_assoc (succ n') m p =
   lem_eq_S (n' + (m + p)) ((n' + m) + p) (thm_plus_assoc n' m p)
↑

AgdaでeqとNatとplusを定義して、足し算の可換性を証明してみた。 †

module Plus where

 data Nat : Set where
   zero : Nat
   succ : Nat -> Nat

 _+_ : Nat -> Nat -> Nat
 zero + y = y
 succ x + y = succ (x + y)

 {- Leibniz equality -}
 -- definition
 eq : {A : Set} -> A -> A -> Set1
 eq x y = (P : _ -> Set) -> P x -> P y

 -- reflexive
 thm_eq_refl : {A : Set} (x : A) -> eq x x
 thm_eq_refl x P px = px

 -- symmetric
 thm_eq_sym : {A : Set} (x y : A) -> eq x y -> eq y x
 thm_eq_sym x y xy P py = xy (\z -> P z -> P x) (\px -> px) py

 -- transitive
 thm_eq_trans : {A : Set} (x y z : A) -> eq x y -> eq y z -> eq x z
 thm_eq_trans x y z xy yz P px = yz P (xy P px)

 -- my lemma
 lem_eq_S : (m n : Nat) -> eq m n -> eq (succ m) (succ n)
 lem_eq_S m n H1 = \P -> \H2 -> H1 (\x -> P (succ x)) H2
 {- end of Leibniz equality -}


 -- lemma 1
 lem_plus_n_O : (n : Nat) -> eq (n + zero) n
 lem_plus_n_O zero = thm_eq_refl zero
 lem_plus_n_O (succ p) = \P -> \H -> lem_plus_n_O p (\x -> P (succ x)) H

 -- lemma 2
 lem_plus_n_Sm : (m n : Nat) -> eq (succ (m + n)) (m + succ n)
 lem_plus_n_Sm zero n = thm_eq_refl (succ n)
 lem_plus_n_Sm (succ p) n = lem_eq_S (succ (p + n)) (p + succ n) (lem_plus_n_Sm p n)

 -- theorem commutative
 thm_plus_comm : (m n : Nat) -> eq (m + n) (n + m)
 thm_plus_comm zero n = thm_eq_sym (n + zero) n (lem_plus_n_O n)
 thm_plus_comm (succ p) n = thm_eq_trans (succ (p + n)) (succ (n + p)) (n + succ p) (lem_eq_S (p + n) (n + p) (thm_plus_comm p n)) (lem_plus_n_Sm n p)

トップ   編集 凍結 差分 バックアップ 添付 複製 名前変更 リロード   新規 一覧 単語検索 最終更新   ヘルプ   最終更新のRSS
Last-modified: 2008-07-19 (土) 17:59:10 (5752d)