Skip to content

Instantly share code, notes, and snippets.

@louisswarren
Forked from milesrout/meme.agda
Last active March 21, 2019 10:26
Show Gist options
  • Save louisswarren/f78de2c6821e8689cb06f30f411c6402 to your computer and use it in GitHub Desktop.
Save louisswarren/f78de2c6821e8689cb06f30f411c6402 to your computer and use it in GitHub Desktop.
open import Agda.Builtin.Bool
data ⊥ : Set where
record ⊤ : Set where
isTrue : Bool → Set
isTrue true = ⊤
isTrue false = ⊥
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
variable
n m p : ℕ
_≤_ : ℕ → ℕ → Bool
zero ≤ m = true
suc n ≤ zero = false
suc n ≤ suc m = n ≤ m
data _⊔_≡_ : ℕ → ℕ → ℕ → Set where
m≥⊔n≡m : {_ : isTrue (n ≤ m)}
---------
→ m ⊔ n ≡ m
m≤⊔n≡n : {_ : isTrue (m ≤ n)}
---------
→ m ⊔ n ≡ n
_ : 0 ⊔ 4 ≡ 4
_ = m≤⊔n≡n
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
variable
n m p : ℕ
data _≤_ : ℕ → ℕ → Set where
z≤n : zero ≤ n
s≤s : m ≤ n
-------------
→ suc m ≤ suc n
data _⊔_≡_ : ℕ → ℕ → ℕ → Set where
m≥⊔n≡m : n ≤ m
---------
→ m ⊔ n ≡ m
m≤⊔n≡n : m ≤ n
---------
→ m ⊔ n ≡ n
infix 4 _≤_
data Formula : ℕ → Set where
var : (n : ℕ) → n ≤ m → Formula m
∩_ : Formula m → Formula (suc m)
∪_ : Formula m → Formula (suc m)
α : Formula m → Formula n → (m ⊔ n ≡ p) → Formula 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