ネタ記録庫/Agda の変更点

• 追加された行はこの色です。
• 削除された行はこの色です。
• ネタ記録庫/Agda へ行く。
• ネタ記録庫/Agda の差分を削除

[[ネタ記録庫/Agda]]
#br
Coqはこちら -> ネタ記録庫/Coq
#contents

* Agdaで足し算のassociativityも証明してみた。 [#nb148916]

  -- 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を定義して、足し算の可換性を証明してみた。 [#g05efb3f]
 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)