[Agda] hidden proofs

[Sergei Meshveliani]

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