Coqはこちら -> ネタ記録庫/Coq
-- 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)
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)