[Agda] Case split on λ()

[Martin Escardo]

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