[Agda] hidden proofs

[Wojciech Jedynak]

2013/7/30 Sergei Meshveliani <mechvel at botik.ru>:

Hello Sergei, Liam and others,

> If the checker was only for this example with Even, then all right,
> there is a clear special algorithm.
> But suppose that one defines
>
>   data Foo : ℕ → Set where
>                      foo1 : Bool -> (n : ℕ) → Foo n
>                      foo2 : <something complex>
>                      ...
>                      foo9 : ... -> Foo (f n)
>
>   foo? : ℕ → Dec $ Foo n
>   foo? 100 = no (λ ())
>   ...
>
> How does the checker decide on whether  foo? 100
> is an absurd pattern or not?

I believe that the usual approach is to analyze the result types of
constructors and use first-order unification.
In the Even case when checking if Even (suc zero) is inhabitable Agda
inspects both constructors:
a) could Even (suc zero) be obtained from the even0 constuctor? No,
because zero and suc zero cannot be unified.
b) could  Even (suc zero) be obtained from the  even-suc constuctor?
No, because (suc (suc n)) and suc zero cannot be unified for any n.
Since there are no more constructors of Even, then Even 1 is empty, so
the absurd pattern is in place.
In general, the problem of inhabitance checking is undecidable, so
absurd patterns can work only in such simple cases.

I think this is the basic idea. I recall reading that the recent
versions of Agda can also see that 'n == suc n' is empty, but this
is slightly more complicated and not that common in my experience.

When learning Agda it is very useful to use the interactive Emacs
mode. Very often the automation
is able to fill terms like 'no  (λ ())'... automatically (using C-c
C-a in agda-mode). Also, the automatic case split (C-c C-c) will spot
when the absurd pattern can be used and/or place dots in patterns (eg.
when destructing an equality).

Hope that helps,
Wojtek Jedynak

2013/7/30 Sergei Meshveliani <mechvel at botik.ru>:
> On Wed, 2013-07-31 at 03:46 +1000, Liam O'Connor wrote:
>> Hi Sergei,
>>
>>
>> I was pretty easily able to define "even" using a similar definition
>> to your first one:
>>
>>
>> open import Data.Nat
>>
>>
>> mutual
>>  data Even : ℕ → Set
>>   where
>>    even0 : Even 0
>>    even-suc : {n : ℕ} → Even n → Even (suc (suc n))
>>
>>
>> open import Relation.Nullary
>>
>>
>> even : (n : ℕ) -> Dec (Even n)
>> even zero = yes even0
>> even (suc zero) = no (λ ()) -- absurd pattern :)
>> even (suc (suc n)) with even n
>> ... | yes p = yes (even-suc p)
>> ... | no p = no (λ { (even-suc x) → p x })
>>
>
> Great! Thank you. A good point for me.
>
> Initially I also had this precise definition of Even.
> But I was stupid enough and has not guessed that  even (suc 0)
> is an absurd pattern here.
>
> There remains a (beginner) question here:
> how does the programmer know which pattern the type checker will agree
> to qualify as absurd?
> This is a matter of the Language definition.
>
> If the checker was only for this example with Even, then all right,
> there is a clear special algorithm.
> But suppose that one defines
>
>   data Foo : ℕ → Set where
>                      foo1 : Bool -> (n : ℕ) → Foo n
>                      foo2 : <something complex>
>                      ...
>                      foo9 : ... -> Foo (f n)
>
>   foo? : ℕ → Dec $ Foo n
>   foo? 100 = no (λ ())
>   ...
>
> How does the checker decide on whether  foo? 100
> is an absurd pattern or not?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda