[Agda] proof run time cost

[Serge D. Mechveliani]

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.
It is actually about using Agda, about what it is for.

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