Agda のバックアップ(No.1)

• バックアップ一覧
• ソース を表示
• Agda は削除されています。
  • 1 (2008-07-18 (金) 01:19:36)

ネタ記録庫/Agda

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)