[Agda] Case split on λ()

[Marcus Christian Lehmann]

Hello Martin,

Thank you for the guidance and once more for the comprehensive example! 
I'll try to turn them into progress:

To convince Agda, that ¬( 2 ≡ 2 ) is empty "is" to get
> thm : ¬( 2 ≡ 2 ) → 𝟘
> thm p = p (refl 2)
type checked.

Applying this to the concrete problem, my line of thought is the following:

For two functions f and g of type B → B, the type of all choices that 
"make f and g differ" I think of as

Σ[ x ∈ B ] ¬(P x)

where
     P : A → Set
     P x = f x ≡ g x

and when explicitly constructing such pair

x1 : Σ[ x ∈ B ] ¬(P x)
x1 = …some-construction… , (λ ())

it is impossible to give a construction where P x holds, because then 
it'd be impossible to give (λ ()) accepted for ¬(P x).

But now, when this becomes an assumption, so we receive an hypothetical 
inhabitant of this type "Σ[ x ∈ B ] ¬(P x)" as in

thm : Σ[ x ∈ B ] ¬(P x) → ⊤
thm (x , ¬p) = ?

then (when we are in the hole `?`) there "are" hypothetical inhabitants  
x : B and ¬p : ¬(P x) available.

We might split x into it's constructors over and over. And cases may 
occur where in their holes `?` it is possible to construct an inhabitant 
refl : P x out of the given, hypothetical inhabitants. Then these cases 
should not matter at all: it is impossible to give an actual inhabitant 
of "Σ[ x ∈ B ] ¬(P x) " that would make such construction possible. I am 
sorry about wrong terminology, when referring to this as an 
"uninhabitated case"; and grateful for every correction.

 From your example I get a more detailed understanding of where 
Data.Empty.⊥-elim is rooted (in 𝟘-recursion) and when filling such 
uninhabitated holes, I understand ⊥-elim (¬p refl) as giving "nothing, 
but of the right type".

Now if we assume that I may just not see refl : P x being constructable 
in such case's hole `?`, then I would not notice that this is an 
uninhabitated case. I understand that my not-noticing is perfectly fine, 
and the construction I might come up without ⊥-elim will never occur on 
an actual inhabitant of Σ[ x ∈ B ] ¬(P x).

So I think "having" a mystical inhabitant  of 𝟘 / ⊥ as "currently 
deriving in an unreachable case" (every time 𝟘 occurs as a hypothesis).

The goal `… → ⊤` in my signature makes `thm` trivial. Even in an 
uninhabitated case one can give tt : ⊤ without the necessity of using 
𝟘-recursion / ⊥-elim. But with a non-trivial goal, one might has no 
other choice to obtain the right type for the goal.

Similarly I would think that every time ⊥-elim / 𝟘-recursion is used, 
the case is also uninhabitated anyways.

I guess the more proper question is: how to enumerate (or just 
"observe") all inhabitated cases of a theorem (function)? (And is that 
even a sound thing to ask?)

I know that the compactness of that, i.e the amount of cases, depends on 
how clever x is split with regard to f and g.  And I might want to split 
often enough to eliminate f and g, for which they better not be 
recursive. So it might be an approach from a wrong direction, but to 
obtain this information, I tried to come up with a proper function 
signature and "look" at the cases to figure out whether they are 
inhabitated.

My current understanding is that for a case-split Agda expands all the 
constructors and removes every case that is rendered impossible by 
unification (e.g. when an inhabitant of ≡ was deduced).

So I think, when one is really up for "eliminating" a case, in a way 
that we will not end up "implementing" it, then a signature needs to be 
set up that puts an impossible constraint in the assumptions of a 
function, but just in that case. It was puzzling me a day how to achieve 
this for ≢ and whether it can be done at all.

Again, thank you for providing the insights: they aid a lot for 
reviewing literature and experimenting with Agda.

regards,

Am 14.03.19 um 23:39 schrieb 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


-- 
Marcus Christian Lehmann, M.Sc.
Research Associate

Technische Universität Berlin
Institute of High-Frequency and Semiconductor System Technologies
Faculty IV – Electrical Engineering and Computer Science
Department Theoretische Elektrotechnik

Secretariat EN 2
Einsteinufer 17
D-10587 Berlin
Germany
  
Phone: +49 (30) 314-21363
Mail:lehmann at tet.tu-berlin.de