[Agda] example with insertion to list

[Sergei Meshveliani]

On Tue, 2017-02-07 at 15:20 +0300, Sergei Meshveliani wrote:
> Please,
> 
> can anybody fix the proof for  lemma2  in the attached code 
> (about 140 lines) ?
> 
> It is about a certain insertion of a natural into a decreasingly ordered
> list of naturals. Such a list is called  Pol.
> Insertion of  e  into  es  is according to _>_, and it is without
> copying, that is when  es  contains any  e' ≡ e,  the result is  es.
> 
> Insertion is called  mon+. 
> lemma1 and lemma2  are certain two very simple statements about
> insertion of  e  into  (e' ∷ es)  for  e < e'.
> 
> lemma1  is for the case of  es = [].  And it is proved trivially.
> 
> And a similar proof for  lemma2  is not type-checked (in Agda 2.5.2).
> Moreover, I do not find any proof to satisfy Agda.
> 
> Maybe, this is a bug in Agda?


In this code, the  Max  structure and inequality are brought there to
mon+ and extMon+  in order to prove termination. 
This complicates  mon+,  and proof search for its properties.
  
mon+  can be greatly simplified by introducing `insert' for insertion of
e  into  es  without providing a proof in recursion,
and then, by adding a proof for 
                      DecrOrdered es -> DecrOrdered (insert e es).

I hope, there  lemma2  will be easier to prove. 

Still:  what can be a proof for Agda for the original implementation of
mon+ ?

Regards,

------
Sergei