Search code examples
agdatheorem-provinginduction

Proving a Type is Uninhabited in Agda

I've been learning Agda recently and I've been making a lot of progress but I'm stuck on one thing: proving that a type is NOT inhabited.

I have a relation on Bools defined as follows:

data Test : Rel Bool 0ℓ where
    direct   : Test false true
    indirect : {j0 j1 j2 : Bool} → Test j0 j1 → Test j1 j2 → Test j0 j2

The direct constructor defined some of the relation, while the indirect constructor adds the transitive closure. Obviously in this example the transitive closure adds nothing, but in the actual problem I'm working on it's important.

I would like to prove testNot : ¬ Test true false but I can't work out how.

My feeling is that the type checker is smart enough to know that the direct constructor isn't useful, and in the indirect constructor j0 is obviously true and j2 is obviously false. This leaves only the two possible cases for j1 to consider. The code I tried was:

testNot (indirect {true} {false} {false} () _)
testNot (indirect {true} {true}  {false} _ ())

I thought that the type checker would know that the only thing that can go in either of those absurd patterns is one of those two indirect constructors with the same arguments, leading to an infinite chain of constructors which is disallowed, hence the absurd patterns. This didn't work -- the error I get is

Test true false should be empty, but the following constructor
patterns are valid:
  indirect {._} {_} {._} _ _
when checking the clause left hand side
testNot (indirect {true} {false} {false} () _)

So I guess I need to prove this by induction on the depth of constructors: fist prove that direct does not have type Test true false, then prove that if no "shallower" constructors have this type then no "deeper" constructor can either and the theorem follows from induction. The problem is I don't know how to express this. What do you suggest?

Solution

  • I would start by proving a positive statement about the value the Test indices take:

    open import Relation.Nullary
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Function.Base

test-indices : ∀ {i j} → Test i j → (i ≡ false × j ≡ true)
test-indices direct = refl , refl
test-indices (indirect p q) =
  let (_ , eq₁) = test-indices p in
  let (eq₂ , _) = test-indices q in
  let absurd = trans (sym eq₁) eq₂ in
  case absurd of λ where ()

    Your result is then a direct corollary:

    testNot : ¬ (Test true false)
testNot p = case proj₁ (test-indices p) of λ where ()