Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Natural deduction rules directly in 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.