[Agda] Case split on λ()

[Marcus Christian Lehmann]

I have attached a more complete example but it boils down to convincing 
Agda that ¬ 2 ≡ 2 should be empty (following the very readable error 
message), e.g.

```
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)
>
> ```

-------------- next part --------------
module CaseSplit where

open import Data.Nat
open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Sum
open import Data.Product

-- (Agda translation from application -- example)
data Tree : Set where
  one : ℕ → Tree
  two : ℕ → ℕ → Tree
  three : ℕ → ℕ → Tree → Tree

-- (Agda translation from application -- example)
f : Tree → Tree
f (one x)           = one x   -- identity
f (two zero x)      = one x   -- different case
f (two x@(suc _) y) = two x y -- identity
f x                 = x       -- identity

-- this reproduces the definition of f, but becomes interesting for composed functions
f-map1 : (x : Tree) → (y : Tree) → f x ≡ y → ⊤
-- f-map1 x y p = ? -- split on x p
f-map1 (one x)          .(one x)          refl = tt
f-map1 (two zero x₁)    .(one x₁)         refl = tt
f-map1 (two (suc x) x₁) .(two (suc x) x₁) refl = tt
f-map1 (three x x₁ x₂)  .(three x x₁ x₂)  refl = tt

g : Tree → Tree
g x = x -- identity, just for the example

-- trying to observe, where f and g "differ"
f-map2 : (x : Tree) → (u : Tree) → (v : Tree) → f x ≡ u → g x ≡ v → u ≡ v → ⊤
-- f-map2 x u v pu pv p = ? -- split on x pu pv
f-map2 (one x)          .(one x)          .(one x)          refl refl refl = tt -- splits on p
-- f-map2 (two x x₁)       .(f (two x x₁))   .(two x x₁)       refl refl p    = {! !} -- refuses to split on p, so split on x again
f-map2 (two zero x₁)    .(one x₁)         .(two 0 x₁)       refl refl ()
f-map2 (two (suc x) x₁) .(two (suc x) x₁) .(two (suc x) x₁) refl refl refl = tt
f-map2 (three x x₁ x₂)  .(three x x₁ x₂)  .(three x x₁ x₂)  refl refl refl = tt -- also splits on p

-- using the observation (absurd cases of f-map2) to come up with theorems
thm1 : ∀ x → f (two zero x) ≢ g (two zero x)
thm1 x = λ ()

-- knowing all absurd cases to come up with
--   "f and g behave equally on all x, except when `x ≡ two zero u` for some u"
thm2 : ∀ x →  f x ≡ g x  ⊎  ∃[ u ] (x ≡ two zero u × f (two zero u) ≢ g (two zero u) )
-- proof works completely with C-c C-a
thm2 (one x) = inj₁ refl
thm2 (two zero x₁) = inj₂ (x₁ , refl , (λ ()))
thm2 (two (suc x) x₁) = inj₁ refl
thm2 (three x x₁ x₂) = inj₁ refl

-- using ≢ directly to observe these cases
f-map3 : (x : Tree) → (u : Tree) → (v : Tree) → f x ≡ u → g x ≡ v → u ≢ v → ⊥
-- f-map3 x u v pu pv p = ? -- split on x pu pv
f-map3 (one x)          .(one x)          .(one x)          refl refl p = p refl
f-map3 (two zero x₁)    .(one x₁)         .(two 0 x₁)       refl refl p = {!   !} -- impossible to create "one x₁ ≡ two 0 x₁"
f-map3 (two (suc x) x₁) .(two (suc x) x₁) .(two (suc x) x₁) refl refl p = p refl
f-map3 (three x x₁ x₂)  .(three x x₁ x₂)  .(three x x₁ x₂)  refl refl p = p refl

-- this might produce false positives, because "tt" is always accepted, where "⊥-elim (p refl)" only in the (now) absurd cases
f-map4 : (x : Tree) → (u : Tree) → (v : Tree) → f x ≡ u → g x ≡ v → u ≢ v → ⊤
-- f-map4 x u v pu pv p = ? -- split on x pu pv
f-map4 (one x)          .(one x)          .(one x)          refl refl p = ⊥-elim (p refl)
f-map4 (two zero x₁)    .(one x₁)         .(two 0 x₁)       refl refl p = tt               -- ⊥-elim (p refl) is not accepted (no refl for "one x₁ ≡ two 0 x₁")
f-map4 (two (suc x) x₁) .(two (suc x) x₁) .(two (suc x) x₁) refl refl p = ⊥-elim (p refl)
f-map4 (three x x₁ x₂)  .(three x x₁ x₂)  .(three x x₁ x₂)  refl refl p = ⊥-elim (p refl)

-- Wished this one
f-map5 : (x : Tree) → (u : Tree) → (v : Tree) → f x ≡ u → g x ≡ v → u ≢ v → ⊤
f-map5 (one x)          .(one x)          .(one x)          refl refl () -- ↯ Error: "one x ≢ one x should be empty, but that's not obvious to me"
f-map5 (two zero x₁)    .(one x₁)         .(two 0 x₁)       refl refl p = tt
f-map5 (two (suc x) x₁) .(two (suc x) x₁) .(two (suc x) x₁) refl refl () -- ↯ Error: "two (suc x) x₁ ≢ two (suc x) x₁ should be empty, but that's not obvious to me"
f-map5 (three x x₁ x₂)  .(three x x₁ x₂)  .(three x x₁ x₂)  refl refl () -- ↯ Error: "three x x₁ x₂ ≢ three x x₁ x₂ should be empty, but that's not obvious to me"