[Agda] proof run time cost

[Serge D. Mechveliani]

On Sat, Oct 06, 2012 at 11:06:07PM +0200, Andreas Abel wrote:
> Hi Serge,
>
> you can make your stuff work if you avoid matching on the proof of (n <=  
> m).  Here is your program where I do not match on p, but use an  
> inversion lemma (inv<=) in the recursive call.  Since evaluation is  
> lazy, your postulate is never evaluated.
> [..]
(I replace some math symbols -- SM). 

>   inv<= : forall {m n} -> suc m <= suc n -> m <= n
>   inv<= (s<=s p) = p
>
>   proofLength : (n : Nat) -> (m : Nat) -> n <= m -> Nat
>   proofLength 0       _       p  = 1
>   proofLength (suc n) 0       ()
>   proofLength (suc n) (suc m) p  = suc (proofLength n m (inv<= p))
>
>   f : Nat -> Nat
>   f n = proofLength (min n 4) 4 p
>         where
>         postulate p : (min n 4) <= 4
> []

Laziness makes it trivial here. Because this contrived example occurs 
unlucky for my intended demonstration:  the result of  proofLength  
can be found from  n and m  without actually using  p.
In other examples `postulate' will probably lead to a run time error.
I expect that in most cases `postulate' will not help to avoid the run 
time cost overhead of a proof, when this proof value is essentially used.
I am going to continue and to see the related effects in practice.

So far, Agda makes a very good impression.

Regards,

------
Sergei