EFQ in Agda

efq.agda

-- The bottom type has the same power as bottom in intuitionistic logic
data ⊥ : Set where

-- Ex falso quodlibet is provable
efq : {S : Set} → ⊥ → S
efq ()

data _⊎_ (S T : Set) : Set where
  inl : S → S ⊎ T
  inr : T → S ⊎ T

-- Disjunctive syllogism is also provable
disjsyl : {S T : Set} → (T → ⊥) → S ⊎ T → S
disjsyl ¬T (inl x) = x
disjsyl ¬T (inr x) = efq (¬T x)

-- Disjunctive syllogism can also be proved directly without delegating to efq
disjsyl' : {S T : Set} → (T → ⊥) → S ⊎ T → S
disjsyl' ¬T (inl x) = x
disjsyl' ¬T (inr x) with (¬T x)
...                 | ()


-- To actually use EFQ, you have to prove a negative. Of course, bottom is not
-- actually derivable, but a derivation may be postulated.


-- For example, it may be postulated
postulate ℝ     : Set
postulate ℝ0 ℝ1 : ℝ
postulate _≈_   : ℝ → ℝ → Set
postulate ℝ0≢ℝ1 : ℝ0 ≈ ℝ1 → ⊥

-- For example
realcollapse : ℝ0 ≈ ℝ1 → ∀ x y → x ≈ y
realcollapse 0≈1 x y = efq (ℝ0≢ℝ1 0≈1)


-- Alternatively, instead of deriving bottom, we show that the required proof
-- is vacuous

data ℕ : Set where
  zero : ℕ
  suc  : ℕ  → ℕ
{-# BUILTIN NATURAL ℕ #-}

-- Typical definition of equality in Agda
data _≡_ {S : Set}(x : S) : S → Set where
  refl : x ≡ x

-- Agda can see that there is no way of constructing 0 ≡ 1 (same way efq works)
zero≢one : 0 ≡ 1 → ⊥
zero≢one ()


-- Sometimes more work is needed
data _≤_ : ℕ → ℕ → Set where
  n≤n : ∀{n} → n ≤ n
  n≤s : ∀{n m} → n ≤ m → n ≤ suc m

≤reduce : ∀{n m} → suc n ≤ suc m → n ≤ m
≤reduce {n} {.n} n≤n = n≤n
≤reduce {n} {zero} (n≤s {.(suc n)} {.0} ())
≤reduce {n} {suc m} (n≤s {.(suc n)} {.(suc m)} pf) = n≤s (≤reduce pf)


sucn≤̷n : ∀ n → suc n ≤ n → ⊥
sucn≤̷n zero ()
sucn≤̷n (suc n) sn≤n = sucn≤̷n n (≤reduce sn≤n)