[Agda] proof overhead

[Serge D. Mechveliani]

People,
I have certain beginner questions on the practice of the verified 
programming with dependent types.

In DT programming, I see the two main new features for me: 
1) a notion of a proof defined by each particular user program, 
   and even defining this individually for each statement,
2) evaluating proofs together with evaluating ordinary values.

Consider the Agda function  orderList  for sorting  xs : List Nat  
non-decreasingly by `<'.  And let it return a record 

record OrderList (xs : List Nat) : Set where 
                       field  
                         resList       : List Nat;
                         ordProof      : IsOrdred resList;
                         multisetProof : multiset xs == multiset resList

(for this letter I replace  \equiv  with  `=='),

with  resList  standing for the resulting list,
IsOrdered  and  multilset  reasonably defined

I have programmed merge sorting, which evaluation cost is  O(n*(log n))
-- together with  resList  and  ordProof.
I can easily add the value for  multisetProof  
-- but with making the evaluation cost  O(n^2).
To preserve  O(n*(log n))  looks like a certain problem.
In particular, one also needs to think of a possible initial programmer's 
definition of a  multiset of a list  and of defining  the relation of
multiset xs == multiset ys.

I do not know, may be I manage to reasonably program this three fields, 
with preserving O(n*(log n)) -- may be, by using the AVL tree, or by 
other means.
Still there may exist other problems, for which it is more difficult, 
-- may be impossible, -- to preserve the usual evaluation cost order.

Question 1 
----------
Consider the two problem kinds.
(I)  To solve algorithmically (say, in Agda) a given problem  P.
(II) To solve P algorithmically (say, in Agda), with the algorithm 
     providing also the corresponding proof.

For example,  (I):   to solve  P = sorting  as  resList  only,
              (II):  to solve  P       with also returning the two proofs.

Can you give a clear example of a simply formulated practical problem  P
such that all known solutions for  P-II  have essentially greater
evaluation cost order than for  P-I ?
(O(n) -> O(n^2), O(n^3) -> O(2^n), and such). 

(Though, I doubt about correctness of this question, because, for example,
the proof size depends on the constructor set which the programmer puts 
for representing a proof for P).


Question 2 
----------
What do you think of the following way out?

Step 1. Program the function   orderList   which 
        a) has evaluation cost  O(n*(log n)),
        b) returns for  resList  the true value, 
        c) returns  p1 and p2  for the two proofs, with declaring
           postulate p1 : IsOrdred resList,  
           postulate p2 : multiset xs == multiset resList.

Step 2. Program  orderList-withProofs   which has evaluation cost  O(n^2) 
        and returns  a) resList,  b) ordProof,  c) multisetProof,
                     d) the proof for  resList (orderList xs) == resList

Step 3. Compile the whole program which includes the two sorting functions.

Step 4. Use   orderList  instead of  orderList-withProofs  everywhere in 
        the program where the evaluation cost matters.

To use this approach for all problems where the proof evaluation cost
adds an essential overhead to evaluation-without-proof.

It comes out that
(1) the whole program with both sorting variants is veryfied
    (because the types have been checked),
(2) sorting has evaluation cost  O(n*(log n))  everywhere where the 
    programmer needed,

(are (1) and (2) right?).

But what to do with a client function which uses the result of  p2
and also attempts to analyze the structure of the  p2  value,  to see 
its constructors?
The programmer needs to estimate the cost: whether using the structure of 
p2  is essential for saving the total cost
(for example, if  ys  is close to  xs,  then forming  p2 for ys  may be 
shorter when using the structure of  p2 for xs).
If it worths, the programmer uses  orderList-withProofs,
otherwise -- orderList.

Are the above questions known?
Am I missing something in this discourse?

Thanks,

------
Sergei