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)))