Skip to content

Instantly share code, notes, and snippets.

@milesrout
Last active March 21, 2019 09:03
Show Gist options
  • Save milesrout/0c577db60c0478197e4964706040b0b4 to your computer and use it in GitHub Desktop.
Save milesrout/0c577db60c0478197e4964706040b0b4 to your computer and use it in GitHub Desktop.
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ}
-------
→ zero ≤ n
s≤s : {m n : ℕ}
→ m ≤ n
-------------
→ suc m ≤ suc n
data _⊔_≡_ : ℕ → ℕ → ℕ → Set where
m≥⊔n≡m : {m n : ℕ}
→ n ≤ m
---------
→ m ⊔ n ≡ m
m≤⊔n≡n : {m n : ℕ}
→ m ≤ n
---------
→ m ⊔ n ≡ n
infix 4 _≤_
data Formula : ℕ → Set where
var : ∀{m} → (n : ℕ) → n ≤ m → Formula m
∩_ : ∀{m} → Formula m → Formula (suc m)
∪_ : ∀{m} → Formula m → Formula (suc m)
α : ∀{m n p} → Formula m → Formula n → (m ⊔ n ≡ p) → Formula p
ν : ∀{m n p} → Formula m → Formula n → (m ⊔ n ≡ p) → Formula p
x : Formula zero
x = var zero z≤n
∩xx : Formula (suc zero)
∩xx = ∩ (var zero z≤n)
xα∩xx : Formula (suc zero)
xα∩xx = α x ∩xx (m≤⊔n≡n z≤n)
∩xxαx : Formula (suc zero)
∩xxαx = α ∩xx x (m≥⊔n≡m z≤n)
∩xxα∩xx : Formula (suc zero)
∩xxα∩xx = α ∩xx ∩xx (m≥⊔n≡m (s≤s z≤n))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment