functional-programmingagdaagda-mode

Agda proving Bool ≢ ⊤


So this is the problem I have in a homework task, I have to prove that bool is not equal with top, also I have a redefined equalsign that I have to use.

module TranspEq where

open import Agda.Primitive
open import Agda.Builtin.Equality renaming (_≡_ to _≡ᵣ_ ; refl to reflᵣ)
open import Agda.Builtin.Nat renaming (Nat to ℕ)

_≡_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
_≡_ {A = A} a b = ∀{κ}(P : A → Set κ) → P a → P b

infix 4 _≡_

-- define conversion between the two 'equals'
transp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ b → a ≡ᵣ b
transp a b x = x (_≡ᵣ_ a) reflᵣ

untransp : ∀{ℓ}{A : Set ℓ}(a b : A) → a ≡ᵣ b → a ≡ b
untransp a .a reflᵣ P y = y

-- prove properties of ≡

refl : ∀{ℓ}{A : Set ℓ}{a : A} → a ≡ a
refl P a = a

sym : ∀{ℓ}{A : Set ℓ}{a b : A} → a ≡ b → b ≡ a
sym {l} {A} {a} {b} = λ z P → z (λ z₁ → (x : P z₁) → P a) (λ x → x)

trans : ∀{ℓ}{A : Set ℓ}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans = λ a b P c → b P (a P c)

cong : ∀{ℓ κ}{A : Set ℓ}{B : Set κ}(f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong = λ f a P → a (λ b → P (f b))

-- types
record ⊤ : Set where
  instance constructor tt

data Bool : Set where
  true : Bool
  false : Bool

data ⊥ : Set where

_≢_ : ∀{ℓ}{A : Set ℓ} → A → A → Setω
a ≢ b = a ≡ b → ⊥

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ = {!!}

I tried something like this, but yeah I couldn't succeed :/ can't create a predicate that is Set -> Set


⊤≠⊥ : ⊤ ≢ ⊥ 
⊤≠⊥ x = x (λ x → x) tt
 

Bool≠⊤ : Bool ≢ ⊤
Bool≠⊤ x = ⊤≠⊥ λ P y → {!   !}
--Bool≠⊤ : Bool ≢ ⊤
--Bool≠⊤ x = x (λ y → y tt) p
--    where
--    p : {Set : (Bool ≡ ⊤)}→ ⊥
--    p (true ≡ tt) = ⊥
--    p (false ≡ tt) = ⊥

Solution

  • The only way to prove that two sets are different in Agda is to exploit their differences in terms of cardinality.

    In case of Bool and this is particularly handy to exploit, because every element of is equal to every other element of it, which isn't true for Bool (true isn't equal to false). Hence all you need is

    Bool≠⊤ : Bool ≢ ⊤
    Bool≠⊤ x with sym x (λ A -> (x y : A) -> x ≡ᵣ y) (λ _ _ -> reflᵣ) true false
    ... | ()