[Agda] proof for insertion to a list

[Sergei Meshveliani]

I am sorry for confusing files.
Please, see now the attached  Feb14-2017.agda.

------
Sergei


On Mon, 2017-02-13 at 20:21 +0300, Sergei Meshveliani wrote:
> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
{- 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 are postulated by `anything'. 

I think that for the last  PE.refl  normalizataion 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₁)
-}


-----------------------------------------------------------------------------
open import Relation.Binary using (Tri; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Empty   using (⊥-elim) 
open import Data.Product using (_×_; _,_)
open import Data.List    using (List; []; _∷_)
open import Data.Nat     using (ℕ; _>_)
open import Data.Nat.Properties using (strictTotalOrder) 


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

open StrictTotalOrder strictTotalOrder using (compare) 

Mon = ℕ × ℕ  

open Tri 

add : (mon : Mon) → List Mon → List Mon

add (a , e) []                 =  (a , e) ∷ []
add (a , e) ((b , e') ∷ mons)  with compare e e'
...
    | tri> _ _ _ = (a , e ) ∷ (b , e') ∷ mons
... | tri< _ _ _ = (b , e') ∷ (add (a , e) mons)
... | tri≈ _ _ _ = mons


----------------------------------------------------------------------------
add-comm :  (mon mon' : Mon) → (mons : List Mon) → 
            (add mon (add mon' mons)) ≡ (add mon' (add mon mons))

add-comm (a , e) (b , e') []  with compare e e' | compare e' e 

... | tri< _ _ _ | tri> _ _ _ = PE.refl 
... | tri> _ _ _ | tri< _ _ _ = PE.refl 

... | tri< e<e' _    _    | tri< e'<e _    e'≯e = ⊥-elim (e'≯e e<e') 
... | tri< e<e' _    _    | tri≈ _    e'≡e e'≯e = ⊥-elim (e'≯e e<e')
... | tri≈ _    _    e'≯e | tri< e'<e _    _    = ⊥-elim (e'≯e e'<e)
... | tri≈ e≮e' _    _    | tri> _    _    e'>e = ⊥-elim (e≮e' e'>e)
... | tri> _    _    e>e' | tri> e'≮e _    _    = ⊥-elim (e'≮e e>e')
... | tri> _    _    e>e' | tri≈ e'≮e _    _    = ⊥-elim (e'≮e e>e') 
... | tri≈ _    e≡e' _    | tri≈ _    _    _    =  PE.refl

add-comm (a , e) (b , e') ((c , e₁) ∷ mons) 
         with compare e e₁ | compare e' e₁ | compare e e' | compare e' e 

... | tri> _ _ e>e₁ | tri> _ _ e'>e₁ | tri> _ _ e>e' | tri< _ _ _ = PE.refl   
... | _             | _              | _             | _          = anything



{- --------------------------------------------------
For the last  PE.refl,  normalize LHS and RHS of the goal:

LHS =  
  add (a , e) (add (b , e') ((c , e₁) ∷ mons))    ≡[ by e'>e₁ ]  
  
  add (a , e) ((b , e') ∷ (c , e₁) ∷ mons)        ≡[ by e>e' ]  

  (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons

RHS =  
  add (b , e') (add (a , e) ((c , e₁) ∷ mons))    ≡[ by e>e₁ ]  
  
  add (b , e') ((a , e) ∷ (c , e₁) ∷ mons)        ≡[ by e'<e ]

  (a , e) ∷ (add (b , e') ((c , e₁) ∷ mons)       ≡[ by e'>e₁ ]

  (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons


Hence,  PE.refl   needs to be a proof.
----------------------------------------------------
-}