[Agda] proof for insertion to a list

[Sergei Meshveliani]

Who can tell, please: 
                                                                                
why the following proof for  add-comm  is rejected by Agda 2.5.2 ? 
                                                                                
(see the attached  .agda  file, it is about 30 nonempty lines).
                                                                                
It is about certain insertion  add  of a pair to a pair list, 
with add-comm  meaning

     add (a , e) ∘ add (b , e') ≗ add (b , e') ∘ add (a , e).

And it is only for the case of  e > e' > e₁,

with other cases postulated in the code by `anything'.
                                                                                
I expect that for the last  PE.refl,  normalization of LHS and RHS 
yields the same term 
                     (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons.       
                                                                                
But Agda reports  

e != e' of type ℕ                              
when checking that the expression PE.refl has type  
add (a , e) (add (b , e') ((c , e₁) ∷ mons) | tri> .¬a₁ .¬b₁ e'>e₁)
≡ add (b , e') (add (a , e) ((c , e₁) ∷ mons) | tri> .¬a .¬b e>e₁) 


Thanks,

------
Sergei

-------------- next part --------------
{-
Can anybody, please, 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.

But 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?

Thanks,

------
Sergei
-}

open import Function using (_∘_; case_of_)
open import Algebra.FunctionProperties using (Op₂)
open import Relation.Binary using (Rel; Tri; DecTotalOrder; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty   using (⊥-elim) 
open import Data.Sum     using (_⊎_)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.List    using (List; []; _∷_) 
open import Data.List.All as AllM using (All) 
open import Data.Nat as Nat       using (ℕ; suc; _≤_; _<_; _>_) 
open import Data.Nat.Properties as NatProp using ()


--****************************************************************************
postulate anything : ∀ {a} {A : Set a} → A   -- for debug 

natSTO = NatProp.strictTotalOrder 
open StrictTotalOrder natSTO using (compare) 


------------------------------------------------------------------------------
data DecrOrdered :  List ℕ → Set 
     where
     nil    : DecrOrdered []
     single : (x : ℕ) → DecrOrdered (x ∷ [])
     prep2  : (x y : ℕ) → (xs : List ℕ) → x > y → DecrOrdered (y ∷ xs) →
                                                  DecrOrdered (x ∷ y ∷ xs)

tailDecrOrdered :  ∀ {x xs} → DecrOrdered (x ∷ xs) → DecrOrdered xs
tailDecrOrdered (single _)                = nil
tailDecrOrdered (prep2 x y xs _ ord-y:xs) = ord-y:xs


------------------------------------------------------------------------------
E : Set 
E = ℕ 

record Pol :  Set where
                  constructor pol′

                  field  exps    : List E
                         ordered : DecrOrdered exps   -- e1 > ... > en 

monPol : E → Pol
monPol e =  pol′ (e ∷ []) (DecrOrdered.single e)

hdExp' : List E → ℕ
hdExp' []      = 0
hdExp' (e ∷ _) = suc e
   
deg' : Pol → ℕ
deg' = hdExp' ∘ Pol.exps

------------------------------------------------------------------------------
open Tri 

------------------------------------------------------------------------------
insert : E → List E → List E 
insert e []         = e ∷ [] 
insert e (e' ∷ es)  with compare e e'
... 
    | tri> _ _ e>e' =  e ∷ e' ∷ es
... | tri≈ _ e≡e' _ =  e ∷ es
... | tri< e<e' _ _ =  e' ∷ (insert e es)

 
insert-preserves-DecrOrdered :  ∀ e → (insert e) Preserves DecrOrdered 

insert-preserves-DecrOrdered e {[]}      _         =   DecrOrdered.single e 
insert-preserves-DecrOrdered e {e' ∷ es} ord-e'es  with compare e e'
...
    | tri> _ _ e>e' =  decrOrdered-cons e>e'es ord-e'es
                       where
                       ...
... | tri≈ _ e≡e'   =  ord-e'es  with compare e e'
... | tri< _ _      =  
                       where
                       ord-es = ..
                       es'    = insert e 



{-
------------------------------------------------------------------------------
mon+ : E → Pol → Pol 
mon+ e =  proj₁ ∘ extMon+ e


------------------------------------------------------------------------------
lemma1 : ∀ e e' → e < e' →  Pol.exps (mon+ e (monPol e')) ≡ e' ∷ e ∷ []

lemma1 e e' e<e'  with compare e e'
...               | tri< _    _ _ = PE.refl
...               | tri> e≮e' _ _ = ⊥-elim (e≮e' e<e')
...               | tri≈ e≮e' _ _ = ⊥-elim (e≮e' e<e')


-- Problem
lemma2 : ∀ e e' es → (ord-e'es : DecrOrdered (e' ∷ es)) → e < e' →
                     let 
                       f = pol′ (e' ∷ es) ord-e'es

                       ord-es : DecrOrdered es 
                       ord-es = tailDecrOrdered ord-e'es 

                       f' = pol′ es ord-es
                     in
                     Pol.exps (mon+ e f) ≡ e' ∷ (Pol.exps (mon+ e f'))

lemma2 e e' es ord-e'es e<e'  with compare e e'

... | tri< _ _ _ =  PE.refl
                    -- anything
... | _ = anything
-}