# [Agda] proof run time cost

Serge D. Mechveliani mechvel at botik.ru
Sat Oct 6 14:59:11 CEST 2012

```People,
I have a beginner question about usage of `postulate' and about a
particular run time cost of proofs.
I am trying to find out what cost may present a verified programming.

First, consider a contrived program

lemma4 : (n : Nat) -> (min n 4) <= 4
lemma4 n =  some silly implementation which running cost is O(n^4).

proofLength : (n : Nat) -> (m : Nat) -> n <= m -> Nat
proofLength 0       _       z<=n     = 1
proofLength (suc n) 0       ()
proofLength (suc n) (suc m) (s<=s p) = suc \$ proofLength n m p

f : Nat -> Nat
f n = proofLength (min n 4) 4 p
where
postulate p : (min n 4) <= 4

main : IO Unit
main = putStrLn \$ toCostring \$ show \$ f 5

(for this letter, I replace the math symbols:
\bn -> Nat,  \<=  ->  <=,  \sqcap -> min ).

The idea is as follows.
Imagine that  lemma4  is difficult to implement for a small enough run
time cost.
(For example, sorting a list costs  O(n*(log n)),  and some proofs
related to this sorting cost  O(n^2),  and I do not see how to make it
smaller).

f  does not use  lemma4,  because its running cost is not appropriate.

Still  lemma4  is used as a verification for  f.
Because as everything  is compiled,  it is verified by this that in  f,
the type   (min n 4) <= 4   is not empty. So, f  is verified, despite its
`postulate' clause.
Right?

Further,  f  boldly tries to analyse possible values of  p,  because it
knows of which constructors are built the members of  (min n 4) <= 4.
The compiler allows this.
But at the run time Agda reports
MAlonzo Runtime Error: postulate evaluated: OrdListTest._.p

I think, this is because the pattern required a concrete value of  p.

So, if  f  somehow transmits  p,  whithout pattern matching against  p,
everything must work.
Right?
And to analyse a value of  p,  f  needs to call  lemma4  and to spend
O(n^4).
Right?

And my real example is sorting a list:

orderList : (xs : List Nat) -> OrderList xs       -- returns a record
-- including proofs
orderList xs =  merge sort method of the cost  O(n*(log n)) where
n = length  xs.
Halve  xs,  order the halfs,  merge the results,
process the proof parts respectively.

The proof part for  ordered \$ orderList xs  :  OrderedList? xs
costs  O(n*(log n)).
But for a full verification, one needs to add a proof for that  xs  and
orderList xs  have the same multiset, that is the same element
multiplicities. As  xs  is not ordered, the simplest definition for
a multiplicity list check in it costs  O(n^2).

With using the approach of the above code for  f,  I am going to add to
orderList  a certain  multiplicityLemma  function. So  orderList  will
be fully verified by just compiling the program.
But if a client function needs to  analyse a proof  for the multiset
part, one needs to call  multiplicityLemma  and thus to spend  O(n^2)
at run time.

The subject is totally new for me.
Can you comment, please? Am I missing something?

Thanks,

-------
Sergei
```