トップ
新規
単語検索
ヘルプ
ネタ記録庫/Agda
をテンプレートにして作成
開始行:
[[ネタ記録庫/Agda]]
#br
Coqはこちら -> ネタ記録庫/Coq
#contents
* Agdaで足し算のassociativityも証明してみた。 [#nb148916]
-- theorem associative
thm_plus_assoc : (n m p : Nat) -> eq (n + (m + p)) ((n ...
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_asso...
* 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 -> ...
-- transitive
thm_eq_trans : {A : Set} (x y z : A) -> eq x y -> eq y ...
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 ...
-- lemma 2
lem_plus_n_Sm : (m n : Nat) -> eq (succ (m + n)) (m + s...
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 +...
-- 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_plu...
thm_plus_comm (succ p) n = thm_eq_trans (succ (p + n)) ...
終了行:
[[ネタ記録庫/Agda]]
#br
Coqはこちら -> ネタ記録庫/Coq
#contents
* Agdaで足し算のassociativityも証明してみた。 [#nb148916]
-- theorem associative
thm_plus_assoc : (n m p : Nat) -> eq (n + (m + p)) ((n ...
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_asso...
* 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 -> ...
-- transitive
thm_eq_trans : {A : Set} (x y z : A) -> eq x y -> eq y ...
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 ...
-- lemma 2
lem_plus_n_Sm : (m n : Nat) -> eq (succ (m + n)) (m + s...
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 +...
-- 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_plu...
thm_plus_comm (succ p) n = thm_eq_trans (succ (p + n)) ...
ページ名: