Agda での命題論理式の証明

Menu Menu

以下の論理式の証明図に対応する Lambda 式を Agda で作れ。

   (1)  A -> A
   (2)  A -> (B -> A)
   (3)  (A ∧ (A -> B)) -> B
   (4)  B -> (B ∧ (A -> B))

作成した Lambda 式の型が、上の式に一致するはずである。

∧ は以下の定義を使ってみよう。

    record ^ (A B : Set) : Set where
       field
          and1 : A
          and2 : B
    data _^d_ ( A B : Set ) : Set where
      and : A -> B -> A ^d B

---

ヒント

(A ∧ B ) -> A は、\a -> _∧_.and1 a で証明できるが、

   (3)  (A ∧ (A -> B)) -> B

は、かなり難しい。

_∧_.and1 a と _∧_.and2 b をいじって、直接構成してもなんとかできるはずだが、

   lemma31  (A ∧ (A -> B)) -> (A -> B)
   lemma32  (A ∧ (A -> B)) ->  A
   lemma33  A -> ( A -> B ) -> B

の三つに分解すると簡単になる。(3-1) は (A ∧ B) -> B と同じ。この三つの lemma を組み合わせて証明を作ると良い。