module A2 where

open import Data.Nat
open import Data.Bool hiding(_∧_;_∨_)

------------------------------------------------------

-- ⊥ は証明がひとつもないような命題だから, 空集合によって表す
-- 帰納的定義によって次のように表現することができる
data ⊥ : Set where

-- record 型は指定された値の型を1組にまとめたもの
-- つまり何も指定しなければ全体の集合 すなわち ⊤ が表現できる
record ⊤ : Set where

-- 連言
record _∧_ (P Q : Set) : Set where
  field
    Elim1 : P
    Elim2 : Q

test1 : (P Q : Set) → Set
test1 p q = p ∧ q

-- 導入規則
∧Intro : {P Q : Set} → P → Q → P ∧ Q
∧Intro p q = record { Elim1 = p ; Elim2 = q }

-- 除去規則 P ∧ Q → P は　∧.Elim1 のようにかける
-- 選言
data _∨_ (P Q : Set) : Set where
  ∨Intro1 : P → P ∨ Q
  ∨Intro2 : Q → P ∨ Q

∨Elim : {P Q R : Set} → P ∨ Q  →  (P  →  R)  →  (Q  →  R)  →  R
∨Elim (∨Intro1 a) prfP _ = prfP a
∨Elim (∨Intro2 b) _ prfQ = prfQ b

test2 : (P Q : Set) → Set
test2 p q = p ∨ q

-- 含意
data _⊃_ (P Q : Set) : Set where
  ⊃Intro : (P → Q) → P ⊃ Q

-- ⊥Elim : 偽の除去規則
-- 存在のしない値は()としてmatchする
⊥Elim : {P : Set} → ⊥ → P
⊥Elim ()

-- ⊃Elim : 導入の除去規則
-- P ⊃ Q 型から P → Q 型の値への写像が存在する
⊃Elim : {P Q : Set} → P ⊃ Q → P → Q
⊃Elim (⊃Intro x) q = x q

_!_ : {P Q : Set} → P ⊃ Q → P → Q
_!_ = ⊃Elim

-- 否定
-- 否定は p → ⊥ すなわち p ⊃ ⊥ として表現される
¬ : Set → Set
¬ p = p ⊃ ⊥


-- 命題1
-- ((A ∧ B) → (A ∨ B)) の証明
-- A ∧ B が与えられたら，A から A ∨ B が作れる
prop1 : (A B : Set) → (A ∧ B) ⊃ (A ∨ B)
prop1 A B = ⊃Intro (λ x → ∨Intro1 (_∧_.Elim1 x))

-- 命題2
-- A ∧ ¬ A → A (Elim1)
-- A ∧ ¬ A → ¬ A (Elim2)
-- (A → ⊥) → A → ⊥ (⊃Elim)
-- ¬ A → (A → ⊥) (negの定義から)
prop2 : (A : Set) → (A ∧ ¬ A) → ⊥
prop2 A p = ⊃Elim (_∧_.Elim2 p) (_∧_.Elim1 p)

-- 全称
data all (P : Set) (Q : P → Set) : Set where
  ∀Intro : ((a : P) → Q a) → all P Q

-- 存在
record exist (P : Set) (Q : P → Set) : Set where
  field
    evidence : P
    Elim : Q evidence

∃Intro : {P : Set} → {Q : P → Set} → (a : P) → Q a → exist P Q
∃Intro a p = record { evidence = a ; Elim = p }

-- 古典論理へ
-- 古典論理では，二重否定除去(DNE)または排中律(LEM)を与える
-- Agda は直観論理に基づいて構成されているので，それを拡張してやる

--postulate DNE : {P : Set} → ¬ (¬ P) → P
postulate LEM : (P : Set) → (P ∨ ¬ P)

-- この二つは同じ拡張をしているので，一方からもう一方を導き出せる
DNE : (P : Set) → ¬ (¬ P) ⊃ P
DNE p = ⊃Intro (λ x → ∨Elim (LEM p) (λ y → y) (λ z → ⊥Elim (⊃Elim x z)))