[Agda] Case split on λ()

[Martin Escardo]

On 15/03/2019 01:27, lehmann at tet.tu-berlin.de wrote:
> So I think "having" a mystical inhabitant  of 𝟘 / ⊥ as "currently
> deriving in an unreachable case" (every time 𝟘 occurs as a hypothesis).

Yes, unreachable case is right. A mathematician would say, in such a
situation, "suppose, for the sake of contradiction, a hypothetical
unicorn is given". (I had said "mythical" in my message. :-) )

Hypothetical things that don't necessarily actually exist happen
often, even without an explicit mention of an empty type or negation,
because it is very easy to get a type depending on a parameter that
happens to be empty for some values of the parameters. And this is the
whole point of predicates, of course.

Because you mentioned Σ, here is a common example that doesn't involve
any explicit negation. Suppose for a given function f : ℕ → ℕ, you
want to show that if there is n : ℕ with f n ≡ 0, then there is a
minimal n with f n ≡ 0. So you want to show that

(f : ℕ → ℕ) → (Σ[ n ∈ ℕ ] (f n ≡ 0))
             → (Σ[ n' ∈ ℕ ] (f n' ≡ 0) × ((k : ℕ) → f k ≡ 0 → n' ≤ k))

(I apologize I don't know the notation of the standard library.)

The type (Σ[ n ∈ ℕ ] (f n ≡ 0)) will be empty for a lot of f's, but
its emptiness is not decidable in general.  But it is perfectly
legitimate to assume a given hypothetical element (n , p) of this
type, and then compute, by search bounded by the given n, the required
output data (n' , p' , φ).

When you try to run this program/proof for an f for which the type
(Σ[ n ∈ ℕ ] (f n ≡ 0)) happens to be empty, you won't be able to
produce a suitable *actual* input to even invoke the program. The
whole program becomes unreachable in your terminology. So when you use
programs, you have to supply actual data, but when you write these
programs, you work with hypothetical data (aka "formal parameters" in
programming).

Martin