[Agda] proof run time cost
Serge D. Mechveliani
mechvel at botik.ru
Sun Oct 7 15:17:39 CEST 2012
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
More information about the Agda
mailing list