tmiyaさんの練習問題をラムダ式で解いてみた

2010-09-26 を見て同じ命題を Agda2 で証明してみた。
Functional Programming Memo: [Coq] Coq-99 : Part 1
agda-mode が証明するのを手伝ってくれるのでお気楽です。

module Practice1 where

data True : Prop where
  tt : True
data False : Prop where

data _∧_ (P Q : Prop) : Prop where
  ∧-intro : P → Q → P ∧ Q
∧-eliml : ∀ {P Q} → P ∧ Q → P
∧-eliml (∧-intro y y') = y
∧-elimr : ∀ {P Q} -> P ∧ Q -> Q
∧-elimr (∧-intro y y') = y'

data _∨_ (P Q : Prop) : Prop where
  ∨-introl : P -> P ∨ Q
  ∨-intror : Q -> P ∨ Q
∨-elim : ∀ {P Q R : Prop} -> (P ∨ Q) -> (P -> R) -> (Q -> R) -> R
∨-elim (∨-introl y) a b = a y
∨-elim (∨-intror y) a b = b y

~_ : Prop -> Prop
~ p = p -> False

infixl 10 _∧_
infixl 9  _∨_

lemma01 : ∀ (A B C : Prop) → (A → B → C) → (A → B) → A → C
lemma01 a b c d e f = d f (e f)

lemma02 : ∀ A B C → A ∧ (B ∧ C) → (A ∧ B) ∧ C
lemma02 a b c d = ∧-intro (∧-intro (∧-eliml d) (∧-eliml (∧-elimr d)))
                          (∧-elimr (∧-elimr d))

lemma03 : ∀ A B C D → (A → C) ∧ (B → D) ∧ A ∧ B → C ∧ D
lemma03 a b c d e = ∧-intro (∧-eliml (∧-eliml (∧-eliml e))
                                     (∧-elimr (∧-eliml e)))
                            (∧-elimr (∧-eliml (∧-eliml e)) (∧-elimr e))

lemma04 : ∀ A → ~(A ∧ (~ A))
lemma04 a b = ∧-elimr b (∧-eliml b)

lemma05 : ∀ A B C → A ∧ (B ∨ C) → (A ∨ B) ∨ C
lemma05 a b c d = ∨-introl (∨-introl (∧-eliml d))

lemma06 : ∀ A → ~(~(~ A)) → ~ A
lemma06 a b c = b (λ x → x c)

lemma07 : ∀ A B → (A → B) → ~ B → ~ A
lemma07 a b c d e = d (c e)

lemma08 :  ∀ (A B : Prop) → ((((A → B) → A) → A) → B) → B
lemma08 a b c = c (λ x → x (λ x' → c (λ _ -> x')))

lemma09 : ∀ A → ~(~(A ∨ (~ A)))
lemma09 a b = b (∨-intror (λ x → b (∨-introl x)))