Natural deduction rules directly in Agda

natded.agda

arrowelim : {A B : Set} → (A → B) → A → B
arrowelim f a = f a


data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

disjintro₁ : {A : Set} → A → (X : Set) → A ⊎ X
disjintro₁ a X = inl a

disjintro₂ : {B : Set} → B → (X : Set) → X ⊎ B
disjintro₂ b X = inr b

disjelim : {A B C : Set} → A ⊎ B → (A → C) → (B → C) → C
disjelim (inl a) f g = f a
disjelim (inr b) f g = g b


record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

_×_ : Set → Set → Set
A × B = Σ A λ _ → B

conjintro : {A B : Set} → A → B → A × B
conjintro a b = a , b

conjelim : {A B C : Set} → A × B → (A → B → C) → C
conjelim (a , b) f = f a b


existintro : {A : Set} {B : A → Set} {a : A} → B a → Σ A B
existintro x = _ , x

existelim : {A : Set} {B : A → Set} {C : Set} {a : A} → ((a , b) : Σ A B) → (B a → C) → C
existelim (a , b) f = f b


data Π (A : Set) (B : A → Set) : Set where
  π : ((a : A) → B a) → Π A B

univintro : {A : Set} {B : A → Set} → ((a : A) → B a) → Π A B
univintro f = π f

univexist : {A : Set} {B : A → Set} → Π A B → (a : A) → B a
univexist (π f) a = f a


data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

---


triv₀ : (P : Set) → P → ¬ P → ⊥
triv₀ P p ¬p = arrowelim ¬p p

triv₁ : (A B : Set) → A × B → A
triv₁ A B A×B = conjelim A×B λ a _ → a



demorgan : (A B : Set) → (¬ A) ⊎ (¬ B) → ¬(A × B)
demorgan A B ¬A⊎¬B = λ A×B →
                       disjelim
                         ¬A⊎¬B
                           (conjelim
                             A×B
                             λ a b ¬a → arrowelim ¬a a)
                           (conjelim
                             A×B
                             λ a b ¬b → arrowelim ¬b b)