Skip to content

Instantly share code, notes, and snippets.

@nicball

nicball/classical_logic.agda

Last active May 24, 2022 08:19
Show Gist options
  • Save nicball/1d542828c7cf2c9bdfde4427dd5c3b06 to your computer and use it in GitHub Desktop.
Save nicball/1d542828c7cf2c9bdfde4427dd5c3b06 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
classical_logic.agda
open import Data.Nat using (ℕ ; zero ; suc ; _≤_; z≤n ; s≤s ; _≤?_)
open import Relation.Nullary using (Dec ; yes ; no)
open import Relation.Nullary.Decidable using (True ; toWitness)
open import Function using (id ; _∘_)
open import Data.List using (List ; [] ; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
infix 25 #ᵗ_
infix 25 #ᶠ_
infix 24 ¬_
infixl 23 _∧_
infixl 22 _∨_
infixr 21 _⇒_
infixl 20 _,_
infix 19 _∋_
infix 19 _#_
infix 18 _-→_
data Proposition : Set where
⊤ ⊥ : Proposition
_∧_ _∨_ _⇒_ : Proposition → Proposition → Proposition
¬_ : Proposition → Proposition
pattern ∅ = []
pattern _,_ xs x = x ∷ xs
data _∋_ : List Proposition → Proposition → Set where
here : ∀ { xs x }
→ (xs , x) ∋ x
there : ∀ { xs x y }
→ xs ∋ x
→ (xs , y) ∋ x
length : List Proposition → ℕ
length ∅ = 0
length (rest , _) = suc (length rest)
lookup : ∀ { xs i } → suc i ≤ length xs → Proposition
lookup {_ , p} {zero} (s≤s z≤n) = p
lookup {rest , _} {suc i} (s≤s i≤l) = lookup i≤l
scoped : ∀ { xs i } → (p : suc i ≤ length xs) → xs ∋ (lookup p)
scoped {_ , p} {zero} (s≤s z≤n) = here
scoped {rest , _} {suc _} (s≤s s≤l) = there (scoped s≤l)
mutual
data _,_⊢_true (Δ : List Proposition) (Γ : List Proposition) : Proposition → Set where
trivial : Δ , Γ ⊢ ⊤ true
reference : ∀ { ϕ }
→ Δ ∋ ϕ
→ Δ , Γ ⊢ ϕ true
absurd : ∀ { ϕ }
→ Δ , (Γ , ϕ) ⊢#
→ Δ , Γ ⊢ ϕ true
∧-true : ∀ { ϕ₁ ϕ₂ }
→ Δ , Γ ⊢ ϕ₁ true
→ Δ , Γ ⊢ ϕ₂ true
→ Δ , Γ ⊢ ϕ₁ ∧ ϕ₂ true
∨-true₁ : ∀ { ϕ₁ ϕ₂ }
→ Δ , Γ ⊢ ϕ₁ true
→ Δ , Γ ⊢ ϕ₁ ∨ ϕ₂ true
∨-true₂ : ∀ { ϕ₁ ϕ₂ }
→ Δ , Γ ⊢ ϕ₂ true
→ Δ , Γ ⊢ ϕ₁ ∨ ϕ₂ true
¬-true : ∀ { ϕ }
→ Δ , Γ ⊢ ϕ false
→ Δ , Γ ⊢ ¬ ϕ true
⇒-true : ∀ { ϕ₁ ϕ₂ }
→ (Δ , ϕ₁) , Γ ⊢ ϕ₂ true
→ Δ , Γ ⊢ ϕ₁ ⇒ ϕ₂ true
data _,_⊢_false (Δ : List Proposition) (Γ : List Proposition) : Proposition → Set where
trivial : Δ , Γ ⊢ ⊥ false
reference : ∀ { ϕ }
→ Γ ∋ ϕ
→ Δ , Γ ⊢ ϕ false
absurd : ∀ { ϕ }
→ (Δ , ϕ) , Γ ⊢#
→ Δ , Γ ⊢ ϕ false
∧-false₁ : ∀ { ϕ₁ ϕ₂ }
→ Δ , Γ ⊢ ϕ₁ false
→ Δ , Γ ⊢ ϕ₁ ∧ ϕ₂ false
∧-false₂ : ∀ { ϕ₁ ϕ₂ }
→ Δ , Γ ⊢ ϕ₂ false
→ Δ , Γ ⊢ ϕ₁ ∧ ϕ₂ false
∨-false : ∀ { ϕ₁ ϕ₂ }
→ Δ , Γ ⊢ ϕ₁ false
→ Δ , Γ ⊢ ϕ₂ false
→ Δ , Γ ⊢ ϕ₁ ∨ ϕ₂ false
¬-false : ∀ { ϕ }
→ Δ , Γ ⊢ ϕ true
→ Δ , Γ ⊢ ¬ ϕ false
⇒-false : ∀ { ϕ₁ ϕ₂ }
→ Δ , Γ ⊢ ϕ₁ true
→ Δ , Γ ⊢ ϕ₂ false
→ Δ , Γ ⊢ ϕ₁ ⇒ ϕ₂ false
data _,_⊢# (Δ : List Proposition) (Γ : List Proposition) : Set where
_#_ : ∀ { ϕ }
→ Δ , Γ ⊢ ϕ true
→ Δ , Γ ⊢ ϕ false
→ Δ , Γ ⊢#
#ᵗ_ : ∀ { Δ Γ }
→ (i : ℕ)
→ { p : True (suc i ≤? length Δ) }
→ Δ , Γ ⊢ (lookup (toWitness p)) true
#ᵗ_ i {p} = reference (scoped (toWitness p))
#ᶠ_ : ∀ { Δ Γ }
→ (i : ℕ)
→ { p : True (suc i ≤? length Γ) }
→ Δ , Γ ⊢ (lookup (toWitness p)) false
#ᶠ_ i {p} = reference (scoped (toWitness p))
extension : ∀ { Δ Γ }
→ (∀ { ϕ } → Δ ∋ ϕ → Γ ∋ ϕ)
→ (∀ { ϕ ψ } → Δ , ψ ∋ ϕ → Γ , ψ ∋ ϕ)
extension ρ here = here
extension ρ (there n) = there (ρ n)
mutual
renameᵗ : ∀ { Δ Δ' Γ Γ' }
→ (∀ { ϕ } → Δ ∋ ϕ → Δ' ∋ ϕ)
→ (∀ { ϕ } → Γ ∋ ϕ → Γ' ∋ ϕ)
→ (∀ { ϕ } → Δ , Γ ⊢ ϕ true → Δ' , Γ' ⊢ ϕ true)
renameᵗ ρ σ trivial = trivial
renameᵗ ρ σ (reference i) = reference (ρ i)
renameᵗ ρ σ (absurd c) = absurd (rename-# ρ (extension σ) c)
renameᵗ ρ σ (∧-true l-true r-true) = ∧-true (renameᵗ ρ σ l-true) (renameᵗ ρ σ r-true)
renameᵗ ρ σ (∨-true₁ l-true) = ∨-true₁ (renameᵗ ρ σ l-true)
renameᵗ ρ σ (∨-true₂ r-true) = ∨-true₂ (renameᵗ ρ σ r-true)
renameᵗ ρ σ (¬-true a-false) = ¬-true (renameᶠ ρ σ a-false)
renameᵗ ρ σ (⇒-true a-true) = ⇒-true (renameᵗ (extension ρ) σ a-true)
renameᶠ : ∀ { Δ Δ' Γ Γ' }
→ (∀ { ϕ } → Δ ∋ ϕ → Δ' ∋ ϕ)
→ (∀ { ϕ } → Γ ∋ ϕ → Γ' ∋ ϕ)
→ (∀ { ϕ } → Δ , Γ ⊢ ϕ false → Δ' , Γ' ⊢ ϕ false)
renameᶠ ρ σ trivial = trivial
renameᶠ ρ σ (reference i) = reference (σ i)
renameᶠ ρ σ (absurd c) = absurd (rename-# (extension ρ) σ c)
renameᶠ ρ σ (∨-false l-false r-false) = ∨-false (renameᶠ ρ σ l-false) (renameᶠ ρ σ r-false)
renameᶠ ρ σ (∧-false₁ l-false) = ∧-false₁ (renameᶠ ρ σ l-false)
renameᶠ ρ σ (∧-false₂ r-false) = ∧-false₂ (renameᶠ ρ σ r-false)
renameᶠ ρ σ (¬-false a-true) = ¬-false (renameᵗ ρ σ a-true)
renameᶠ ρ σ (⇒-false a-true b-false) = ⇒-false (renameᵗ ρ σ a-true) (renameᶠ ρ σ b-false)
rename-# : ∀ { Δ Δ' Γ Γ' }
→ (∀ { ϕ } → Δ ∋ ϕ → Δ' ∋ ϕ)
→ (∀ { ϕ } → Γ ∋ ϕ → Γ' ∋ ϕ)
→ (Δ , Γ ⊢# → Δ' , Γ' ⊢#)
rename-# ρ σ (a-true # a-false) = renameᵗ ρ σ a-true # renameᶠ ρ σ a-false
extend_mapᵗ : ∀ { Δ Δ' Γ }
→ (∀ { ϕ } → Δ ∋ ϕ → Δ' , Γ ⊢ ϕ true)
→ (∀ { ϕ ψ } → Δ , ψ ∋ ϕ → (Δ' , ψ) , Γ ⊢ ϕ true)
extend_mapᵗ ρ here = reference here
extend_mapᵗ ρ (there n) = renameᵗ there id (ρ n)
extend_mapᶠ : ∀ { Δ Γ Γ' }
→ (∀ { ϕ } → Γ ∋ ϕ → Δ , Γ' ⊢ ϕ false)
→ (∀ { ϕ ψ } → Γ , ψ ∋ ϕ → Δ , (Γ' , ψ) ⊢ ϕ false)
extend_mapᶠ σ here = reference here
extend_mapᶠ σ (there n) = renameᶠ id there (σ n)
mutual
substituteᵗ : ∀ { Δ Δ' Γ Γ' }
→ (∀ { ϕ } → Δ ∋ ϕ → Δ' , Γ' ⊢ ϕ true)
→ (∀ { ϕ } → Γ ∋ ϕ → Δ' , Γ' ⊢ ϕ false)
→ (∀ { ϕ } → Δ , Γ ⊢ ϕ true → Δ' , Γ' ⊢ ϕ true)
substituteᵗ ρ σ trivial = trivial
substituteᵗ ρ σ (reference n) = ρ n
substituteᵗ ρ σ (absurd r) = absurd (substitute-# (renameᵗ id there ∘ ρ) (extend_mapᶠ σ) r)
substituteᵗ ρ σ (∧-true ϕ-true ψ-true) = ∧-true (substituteᵗ ρ σ ϕ-true) (substituteᵗ ρ σ ψ-true)
substituteᵗ ρ σ (∨-true₁ ϕ-true) = ∨-true₁ (substituteᵗ ρ σ ϕ-true)
substituteᵗ ρ σ (∨-true₂ ψ-true) = ∨-true₂ (substituteᵗ ρ σ ψ-true)
substituteᵗ ρ σ (¬-true ϕ-false) = ¬-true (substituteᶠ ρ σ ϕ-false)
substituteᵗ ρ σ (⇒-true ϕ-true) = ⇒-true (substituteᵗ (extend_mapᵗ ρ) (renameᶠ there id ∘ σ) ϕ-true)
substituteᶠ : ∀ { Δ Δ' Γ Γ' }
→ (∀ { ϕ } → Δ ∋ ϕ → Δ' , Γ' ⊢ ϕ true)
→ (∀ { ϕ } → Γ ∋ ϕ → Δ' , Γ' ⊢ ϕ false)
→ (∀ { ϕ } → Δ , Γ ⊢ ϕ false → Δ' , Γ' ⊢ ϕ false)
substituteᶠ ρ σ trivial = trivial
substituteᶠ ρ σ (reference n) = σ n
substituteᶠ ρ σ (absurd r) = absurd (substitute-# (extend_mapᵗ ρ) (renameᶠ there id ∘ σ) r)
substituteᶠ ρ σ (∧-false₁ ϕ-false) = ∧-false₁ (substituteᶠ ρ σ ϕ-false)
substituteᶠ ρ σ (∧-false₂ ψ-false) = ∧-false₂ (substituteᶠ ρ σ ψ-false)
substituteᶠ ρ σ (∨-false ϕ-false ψ-false) = ∨-false (substituteᶠ ρ σ ϕ-false) (substituteᶠ ρ σ ψ-false)
substituteᶠ ρ σ (¬-false ϕ-true) = ¬-false (substituteᵗ ρ σ ϕ-true)
substituteᶠ ρ σ (⇒-false ϕ-true ψ-false) = ⇒-false (substituteᵗ ρ σ ϕ-true) (substituteᶠ ρ σ ψ-false)
substitute-# : ∀ { Δ Δ' Γ Γ' }
→ (∀ { ϕ } → Δ ∋ ϕ → Δ' , Γ' ⊢ ϕ true)
→ (∀ { ϕ } → Γ ∋ ϕ → Δ' , Γ' ⊢ ϕ false)
→ (Δ , Γ ⊢# → Δ' , Γ' ⊢#)
substitute-# ρ σ (ϕ-true # ϕ-false) = substituteᵗ ρ σ ϕ-true # substituteᶠ ρ σ ϕ-false
_[_ᵗ]# : ∀ { Δ Γ ϕ }
→ (Δ , ϕ) , Γ ⊢#
→ Δ , Γ ⊢ ϕ true
→ Δ , Γ ⊢#
_[_ᵗ]# {Δ} {Γ} {ϕ} f x = substitute-# ρ reference f
where
ρ : ∀ { ψ } → (Δ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ true
ρ here = x
ρ (there n) = reference n
_[_ᶠ]# : ∀ { Δ Γ ϕ }
→ Δ , (Γ , ϕ) ⊢#
→ Δ , Γ ⊢ ϕ false
→ Δ , Γ ⊢#
_[_ᶠ]# {Δ} {Γ} {ϕ} f x = substitute-# reference σ f
where
σ : ∀ { ψ } → (Γ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ false
σ here = x
σ (there n) = reference n
_[_ᵗ]ᵗ : ∀ { Δ Γ ϕ ψ }
→ (Δ , ϕ) , Γ ⊢ ψ true
→ Δ , Γ ⊢ ϕ true
→ Δ , Γ ⊢ ψ true
_[_ᵗ]ᵗ {Δ} {Γ} {ϕ} f x = substituteᵗ ρ reference f
where
ρ : ∀ { ψ } → (Δ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ true
ρ here = x
ρ (there n) = reference n
_[_ᶠ]ᵗ : ∀ { Δ Γ ϕ ψ }
→ Δ , (Γ , ϕ) ⊢ ψ true
→ Δ , Γ ⊢ ϕ false
→ Δ , Γ ⊢ ψ true
_[_ᶠ]ᵗ {Δ} {Γ} {ϕ} f x = substituteᵗ reference σ f
where
σ : ∀ { ψ } → (Γ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ false
σ here = x
σ (there n) = reference n
_[_ᵗ]ᶠ : ∀ { Δ Γ ϕ ψ }
→ (Δ , ϕ) , Γ ⊢ ψ false
→ Δ , Γ ⊢ ϕ true
→ Δ , Γ ⊢ ψ false
_[_ᵗ]ᶠ {Δ} {Γ} {ϕ} f x = substituteᶠ ρ reference f
where
ρ : ∀ { ψ } → (Δ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ true
ρ here = x
ρ (there n) = reference n
_[_ᶠ]ᶠ : ∀ { Δ Γ ϕ ψ }
→ Δ , (Γ , ϕ) ⊢ ψ false
→ Δ , Γ ⊢ ϕ false
→ Δ , Γ ⊢ ψ false
_[_ᶠ]ᶠ {Δ} {Γ} {ϕ} f x = substituteᶠ reference σ f
where
σ : ∀ { ψ } → (Γ , ϕ) ∋ ψ → Δ , Γ ⊢ ψ false
σ here = x
σ (there n) = reference n
data _-→_ { Δ Γ } : Δ , Γ ⊢# → Δ , Γ ⊢# → Set where
∧-→1 : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ψ-true : Δ , Γ ⊢ ψ true } { ϕ-false : Δ , Γ ⊢ ϕ false }
→ ∧-true ϕ-true ψ-true # ∧-false₁ ϕ-false -→ ϕ-true # ϕ-false
∧-→2 : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ψ-true : Δ , Γ ⊢ ψ true } { ψ-false : Δ , Γ ⊢ ψ false }
→ ∧-true ϕ-true ψ-true # ∧-false₂ ψ-false -→ ψ-true # ψ-false
∨-→1 : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ϕ-false : Δ , Γ ⊢ ϕ false } { ψ-false : Δ , Γ ⊢ ψ false }
→ ∨-true₁ ϕ-true # ∨-false ϕ-false ψ-false -→ ϕ-true # ϕ-false
∨-→2 : ∀ { ϕ ψ } { ψ-true : Δ , Γ ⊢ ψ true } { ϕ-false : Δ , Γ ⊢ ϕ false } { ψ-false : Δ , Γ ⊢ ψ false }
→ ∨-true₂ ψ-true # ∨-false ϕ-false ψ-false -→ ψ-true # ψ-false
¬-→ : ∀ { ϕ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ϕ-false : Δ , Γ ⊢ ϕ false }
→ ¬-true ϕ-false # ¬-false ϕ-true -→ ϕ-true # ϕ-false
⇒-→ : ∀ { ϕ ψ } { ϕ-true : Δ , Γ ⊢ ϕ true } { ψ-true : (Δ , ϕ) , Γ ⊢ ψ true } { ψ-false : Δ , Γ ⊢ ψ false }
→ ⇒-true ψ-true # ⇒-false ϕ-true ψ-false -→ ψ-true [ ϕ-true ᵗ]ᵗ # ψ-false
absurdᵗ-→ : ∀ { ϕ ψ } { p : Δ , (Γ , ϕ) ⊢ ψ true } { k : Δ , (Γ , ϕ) ⊢ ψ false } { ϕ-false : Δ , Γ ⊢ ϕ false }
→ absurd (p # k) # ϕ-false -→ p [ ϕ-false ᶠ]ᵗ # k [ ϕ-false ᶠ]ᶠ
absurdᶠ-→ : ∀ { ϕ ψ } { p : (Δ , ϕ) , Γ ⊢ ψ true } { k : (Δ , ϕ) , Γ ⊢ ψ false } { ϕ-true : Δ , Γ ⊢ ϕ true }
→ ϕ-true # absurd (p # k) -→ p [ ϕ-true ᵗ]ᵗ # k [ ϕ-true ᵗ]ᶠ
data _isPrefixOf_ : List Proposition → List Proposition → Set where
refl : ∀ { Δ } → Δ isPrefixOf Δ
weaken : ∀ { Δ Γ ϕ } → Δ isPrefixOf Γ → Δ isPrefixOf (Γ , ϕ)
∅-bottom : ∀ { Δ } → ∅ isPrefixOf Δ
∅-bottom {∅} = refl
∅-bottom {Δ , _} = weaken ∅-bottom
_isPrefixOf?_ : (Δ : List Proposition) → (Γ : List Proposition) → Dec (Δ isPrefixOf Γ)
_isPrefixOf?_ ∅ _ = yes ∅-bottom
_isPrefixOf?_ (Δ , _) ∅ = no λ()
_isPrefixOf?_ (Δ , ϕ) (Γ , ψ) with (Δ , ϕ) isPrefixOf? Γ
... | yes p = yes (weaken p)
... | no _ = {!!}
wow-such-logic : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ ϕ false
→ Δ , Γ ⊢ ϕ ⇒ ψ true
wow-such-logic ϕ-false = ⇒-true (absurd (#ᵗ 0 # renameᶠ there there ϕ-false))
ap : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ ϕ true
→ Δ , Γ ⊢ ϕ ⇒ ψ true
→ Δ , Γ ⊢ ψ true
ap ϕ-true ϕ⇒ψ-true = absurd (renameᵗ id there ϕ⇒ψ-true # ⇒-false (renameᵗ id there ϕ-true) (#ᶠ 0))
∧-true-elim₁ : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ ϕ ∧ ψ true
→ Δ , Γ ⊢ ϕ true
∧-true-elim₁ ϕ∧ψ-true = absurd (renameᵗ id there ϕ∧ψ-true # ∧-false₁ (#ᶠ 0))
∨-false-elim₁ : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ ϕ ∨ ψ false
→ Δ , Γ ⊢ ϕ false
∨-false-elim₁ ϕ∨ψ-false = absurd (∨-true₁ (#ᵗ 0) # renameᶠ there id ϕ∨ψ-false)
∨-false-elim₂ : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ ϕ ∨ ψ false
→ Δ , Γ ⊢ ψ false
∨-false-elim₂ ϕ∨ψ-false = absurd (∨-true₂ (#ᵗ 0) # renameᶠ there id ϕ∨ψ-false)
refl-true : ∀ { Δ Γ ϕ }
→ (Δ , ϕ) , Γ ⊢ ϕ true
refl-true = #ᵗ 0
deMorgan : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ ϕ ∨ ψ false
→ Δ , Γ ⊢ (¬ ϕ) ∧ (¬ ψ) true
deMorgan ϕ∧ψ-false = ∧-true (¬-true (∨-false-elim₁ ϕ∧ψ-false)) ((¬-true (∨-false-elim₂ ϕ∧ψ-false)))
¬¬-elimᵗ : ∀ { Δ Γ ϕ }
→ Δ , Γ ⊢ ¬ (¬ ϕ) true
→ Δ , Γ ⊢ ϕ true
¬¬-elimᵗ ¬¬ϕ-true = absurd (renameᵗ id there ¬¬ϕ-true # ¬-false (¬-true (#ᶠ 0)))
¬¬-elimᶠ : ∀ { Δ Γ ϕ }
→ Δ , Γ ⊢ ¬ (¬ ϕ) false
→ Δ , Γ ⊢ ϕ false
¬¬-elimᶠ ¬¬ϕ-false = absurd (¬-true (¬-false (#ᵗ 0)) # renameᶠ there id ¬¬ϕ-false)
¬-elimᵗ : ∀ { Δ Γ ϕ }
→ Δ , Γ ⊢ ¬ ϕ false
→ Δ , Γ ⊢ ϕ true
¬-elimᵗ = ¬¬-elimᵗ ∘ ¬-true
¬-elimᶠ : ∀ { Δ Γ ϕ }
→ Δ , Γ ⊢ ¬ ϕ true
→ Δ , Γ ⊢ ϕ false
¬-elimᶠ = ¬¬-elimᶠ ∘ ¬-false
contraposition : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ ϕ ⇒ ψ true
→ Δ , Γ ⊢ (¬ ψ) ⇒ (¬ ϕ) true
contraposition ϕ⇒ψ-true = ⇒-true (absurd (ap (¬-elimᵗ (#ᶠ 0)) (renameᵗ there there ϕ⇒ψ-true) # ¬-elimᶠ (#ᵗ 0)))
decontraposition : ∀ { Δ Γ ϕ ψ }
→ Δ , Γ ⊢ (¬ ψ) ⇒ (¬ ϕ) true
→ Δ , Γ ⊢ ϕ ⇒ ψ true
decontraposition ¬ψ⇒¬ϕ = ⇒-true (¬¬-elimᵗ (ap (¬-true (¬-false (#ᵗ 0))) (renameᵗ there id (contraposition ¬ψ⇒¬ϕ))))
∨-true-elim : ∀ { Δ Γ ϕ ψ ω }
→ Δ , Γ ⊢ ϕ ∨ ψ true
→ (Δ , ϕ) , Γ ⊢ ω true
→ (Δ , ψ) , Γ ⊢ ω true
→ Δ , Γ ⊢ ω true
∨-true-elim ϕ∨ψ-true f g = absurd (renameᵗ id there ϕ∨ψ-true # ∨-false (absurd (ap (#ᵗ 0) (renameᵗ there there (⇒-true f))# (#ᶠ 0)))
(absurd (ap (#ᵗ 0) (renameᵗ there there (⇒-true g)) # (#ᶠ 0))))
∧-false-elim : ∀ { Δ Γ ϕ ψ ω }
→ Δ , Γ ⊢ ϕ ∧ ψ false
→ Δ , (Γ , ϕ) ⊢ ω false
→ Δ , (Γ , ψ) ⊢ ω false
→ Δ , Γ ⊢ ω false
∧-false-elim ϕ∧ψ-false f g = absurd (∧-true (absurd ((#ᵗ 0) # {!!})) {!!} # renameᶠ there id ϕ∧ψ-false)
_ : ∀ { Δ Γ ϕ ψ θ }
→ Δ , Γ ⊢ (ϕ ∧ (ψ ∧ θ)) ⇒ (ϕ ∧ θ) true
_ = ⇒-true (absurd ((#ᵗ 0) # ∧-false₂ (∧-false₂ (absurd ((#ᵗ 1) # ∧-false₁ (absurd (∧-true (#ᵗ 0) (#ᵗ 1) # (#ᶠ 0))))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment