[Agda] example with insertion to list

[Sergei Meshveliani]

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?

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) 

record Max (x y : ℕ) :  Set 
       where
       constructor max′
       field
         it      : ℕ
         x-or-y  : it ≡ x ⊎ it ≡ y
         both≤it : x ≤ it × y ≤ it

postulate  extMax :  (x y : ℕ) → Max x y

_⊔_ : Op₂ ℕ
_⊔_ x =  Max.it ∘ extMax x

both≤⊔ :  ∀ x y → x ≤ x ⊔ y × y ≤ x ⊔ y
both≤⊔ x =
           Max.both≤it ∘ extMax x

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

------------------------------------------------------------------------------
extMon+ : (e : E) → (f : Pol) → (∃ \h → deg' h ≤ (suc e) ⊔ (deg' f)) 

extMon+ e (pol′ es ord) =  aux es ord 
  where
  se = suc e

  aux : (es0 : List E) → DecrOrdered es0 → (∃ \h → deg' h ≤ se ⊔ (hdExp' es0)) 

  aux []        _        = (monPol e , leq)  where
                                             leq : se ≤ se ⊔ 0  
                                             leq = proj₁ (both≤⊔ se 0)
  aux (e' ∷ es) ord-e'es  with compare e e'
  ... 
      | tri> _ _ e>e' =  (pol′ (e ∷ e' ∷ es) ord-ee'se , leq)
                         where
                         leq : se ≤ se ⊔ (suc e')
                         leq = proj₁ (both≤⊔ se (suc e'))

                         postulate  ord-ee'se : DecrOrdered (e ∷ e' ∷ es)

  ... | tri< e<e' _ _ =  (pol′ (e' ∷ esG) ord-e'esG , leq)
                         where
                         ord-es : DecrOrdered es
                         ord-es = tailDecrOrdered ord-e'es

                         esG = Pol.exps (proj₁ (aux es ord-es))  

                         leq :  (suc e') ≤ se ⊔ (suc e') 
                         leq =  proj₂ (both≤⊔ se (suc e'))
 
                         postulate  ord-e'esG : DecrOrdered (e' ∷ esG)

  ... | tri≈ _ e≡e' _ =  (pol′ (e ∷ es) ord-ees , leq) 
                         -- here  e  is contrived 
                         where
                         e'es≡ees : e' ∷ es ≡ e ∷ es 
                         e'es≡ees = PE.cong (_∷ es) (PE.sym e≡e')

                         ord-ees : DecrOrdered (e ∷ es)
                         ord-ees = PE.subst DecrOrdered e'es≡ees ord-e'es 
                                
                         leq : se ≤ se ⊔ (suc e')
                         leq = proj₁ (both≤⊔ se (suc 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

      {- Intended: 
         = goal
           where
           ord-es = tailDecrOrdered ord-e'es
           f'     = pol′ es ord-es  
           goal   = 
             begin
               Pol.exps (mon+ e (pol′ (e' ∷ es) ord-e'es))   ≡[ PE.refl ]

               let esG = Pol.exps (proj₁ (aux es ord-es))  
               in
               Pol.exps (pol′ (e' ∷ esG) _)                  ≡[ PE.refl ]

               e' ∷ esG                                      ≡[ PE.refl ]
               e' ∷ (Pol.exps (proj₁ (aux es ord-es)))       ≡[ PE.refl ]
               e' ∷ (Pol.exps (mon+ e f')) 
             end
      -}  

... | _ = anything