[Agda] Case split on λ()

[Marcus Christian Lehmann]

Am 15.03.19 um 07:55 schrieb Martin Escardo:
> (I had said "mythical" in my message. :-) ) 
That was a subconscious, but revealing confusion.

For the example yo gave it is indeed very convincing that the 
reachability of a case should not be knowable in general (not for ℕ → ℕ 
with the assumption Σ[ n ∈ ℕ ] (f n ≡ 0) because we intuitively know 
there exist such functions, but when restricted with arbitrary 
assumptions, yes, this is should not be generally decidable).

Then the reachability of RHS for predicates P in

∀(f : ℕ → ℕ) → ∃[ x ] (P f x) → RHS

is the ability to give an actual inhabitant of

Σ[ f ∈ ℕ → ℕ ] ∃[ x ] (P f x)

Now I see that even for an inductively defined datatype A this becomes

Σ[ a ∈ A ] ∃[ x ] (P a x)

so when I am able to implement in the other mail

∀(a : A) → ∃[ x ] (P a x) ⊎ ∃[ x ] ¬(P a x)

or rather, what I came up with was

∀(x : C++Type) → ∀(z : Bool) → P x z ⊎ ¬(P x z)

this amounts to the decidability of P. And it seems that  this is what 
Relation.Nullary.Dec is for.

For my application I really can implement (or mostly just choose the 
case-split and let Agda use its C-c C-a powers)

dec-P : ∀(x : C++Type) → ∀(z : Bool) → Dec (P x z)

and with

absurdify-yes : ∀{X : Set} → Dec X → Set
absurdify-yes (yes p) = ⊥
absurdify-yes (no ¬p) = ⊤

the signature

cases : ∀(x : C++Type) → ∀(z : Bool) → absurdify-yes(dec-P x z) → RHS

does ()-out (leaves out with () pattern) all the cases where P holds and 
only the ¬P cases remain.
Which means that in every such remaining, non-absurd case was "backed" 
by a (free-variable-)proof of ¬P.

This is exactly what I was looking for, and I can see why it works in my 
specific case and how it breaks down in general when dec-P is not 
implementable (and we have to apply ¬p : P → ⊥ in the RHS with ⊥-elim / 
𝟘-recursion).

Well, due to our discussion, not only "reachability" is limited to 
decidable cases, but even RHS still depends on the "reachability" of ∀(x 
: C++Type) → ∀(z : Bool) so I also see that this is a very limited, if 
not even misleading, terminology.

Thank you for the clarification!

regards,