[Agda] Case split on λ()

[Martin Escardo]

Let me give a complete example of this situation written in Agda,
without solving your specific problem (deliberately), in a
self-contained way:

----
data _≡_ {X : Set} : X → X → Set where
   refl : (x : X) → x ≡ x

data 𝟘 : Set where

𝟘-induction : (A : 𝟘 → Set) → (x : 𝟘) → A x
𝟘-induction A ()

-- The above should be the only place you would ever *need* to use the
-- () pattern, as Martin-Löf type theory teaches us.

-- Even better, if the data definition of the empty type 𝟘 has zero
-- constructors, then 𝟘-induction should be defined by zero
-- equations in an ideal world.

𝟘-recursion : (B : Set) → 𝟘 → B
𝟘-recursion B = 𝟘-induction (λ (_ : 𝟘) → B)

¬ : Set → Set
¬ X = X → 𝟘

-- Example of how the pattern () can be avoided once we have
-- 𝟘-induction:

data Colour : Set where
  Black White : Colour

not-black-is-white : (c : Colour) → ¬ (c ≡ Black) → c ≡ White
not-black-is-white Black f = 𝟘-recursion (Black ≡ White) (f (refl Black))
not-black-is-white White f = refl White

-- Here f : c ≡ Black → 𝟘.

-- We don't pattern match on f, because it is a function.  We use it.
-- To use it, we have to apply it to an argument.  Once we have the
-- argument available, we get a mythical element of 𝟘, with which we
-- can do anything we like, using 𝟘-recursion.
----
Martin

On 14/03/2019 20:33, Martin Escardo wrote:
>
>
> On 14/03/2019 16:36, lehmann at tet.tu-berlin.de wrote:
>> convincing Agda that ¬ 2 ≡ 2 should be empty
>
> I am not going to give a solution in Agda. Instead, I will try to guide
> you.
>
>   * The type `2 ≡ 2` has an inhabitant. (By definition of `≡`.)
>
>   * To say that a type `X` is empty amounts to saying that we have an
>     inhabitant of `¬ X`.
>
>     That is, that you have a function X → R where R is the empty type.
>
>   * So you are trying to show that `¬(¬ 2 ≡ 2)` has an inhabitant.
>
>   * But for any type `A`, if `A` has an inhabitant, then so does `¬¬A`.
>
>     If you are a logician, you know that.
>
>     If you are a functional programmer, what you are trying to do is
>     from an inhabitant of the type `A` to get an inhabitant of the type
>     `(A → R) → R`, where `R` is the empty type.
>
>     But this can actually be done for an arbitrary type `R`, not just
>     the empty type. It is the evaluation map.
>
>   * Now if you read "`¬ (2 ≡ 2)` is empty" as `(2 ≡ 2 → R) → R` for `R`
>     the empty type, you are done.
>
> I hope this helps. Pattern matching is not what is needed here.
>
> Martin
>
>
>
>>
>> ```
>> fun : ¬ (2 ≡ 2) → ⊥
>> fun () -- Error: "¬ 2 ≡ 2 should be empty, but that's not obvious to me"
>> ```
>>
>>
>> Am 14.03.19 um 09:09 schrieb Apostolis Xekoukoulotakis:
>>> Marcus, I could not follow your example, but it seems that you are
>>> trying to case split a function, which is not possible.
>>>
>>> ```
>>> open import Relation.Binary.PropositionalEquality
>>> open import Data.Nat
>>> open import Data.Empty
>>> open import Relation.Nullary
>>>
>>>
>>> fun : ¬ (2 ≡ 2) → ⊥
>>> fun ¬x =  ? -- ⊥-elim (¬x refl)
>>>
>>> ```
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe