[Agda] example with nested `with'

Sergei Meshveliani mechvel at botik.ru
Thu Mar 2 10:52:33 CET 2017


(This was a reply to my letter, with copying the reply to the list, but
I discover that it has missed the list. So, I resend it separately). 

Dear Agda developers,

the attached code presents problems with nested "with - inspect"
construct.
Can you tell, please, what am I missing about using this tool?
Also I suspect a bug in "with - inspect".
 
The code is about the lemma  comm  below:

----------------------------
Mon = ℕ × ℕ

add : 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≈ _ _ _ = (a + b , e) ∷ mons

comm :  ∀ a e b e' mons → add (a , e ) (add (b , e') mons) ≡
                          add (b , e') (add (a , e ) mons)
----------------------------
 
The question is about the pattern

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

The attached code contains a full proof for this  comm  statement.

You see, it must be proved trivially, by testing nested comparisons 
compare x y  
for (x , y) =  (e , e₁), (e' , e₁), (e , e'), (e' , e).

In the end of each branch, the proof is by  PE.refl,
and unreachable branches are done by the constructs like 
" = ⊥-elim (e'≮e e>e') ".

A proof for this does not need any detailed explanation, it needs only
a comment:
-- Test the comparison cases for (e , e₁), (e' , e₁), (e , e'),
-- and the proof there is set by normalization".

And the reader does not need to look into its code. 
So that the code needs only to process all these cases in a shortest
way, without care for readability. 

But the given proof is rather long, it is about 130 nonempty lines.
I failed to invent anything smaller.

1) Many comparison results are processed by  with - inspect - rewrite.
   Some of such bindings occur necessary, and they do work. 
   But  Agda 2.6.0-e384ae7  forgets of some others, so that I need to 
   repeat applying  (with compare ei ej ...)  down the branch for a
   value which must be reduced earlier. 

   Is this a bug in Agda ?

   The comments  (c1), (c3) ...  mark such places in the program.

2) The code has the fragment
 
   ... | tri≈ _ e≡e' _ | PE.[ rw-e≡e' ] rewrite rw-e≡e' =  aux001
       where                                                 
       aux001 :  (a + b , e) ∷ (c , e₁) ∷ mons  ≡
                 add (b , e') ((a , e ) ∷ (c , e₁) ∷ mons)
       aux001
           with compare e' e
       ... | tri> _ e'≢e _ =  ⊥-elim (e'≢e (PE.sym e≡e'))
       ... | tri< _ e'≢e _ =  ⊥-elim (e'≢e (PE.sym e≡e'))
       ... | tri≈ _ _    _ =  PE.cong (_∷ ((c , e₁) ∷ mons)) monEq
                              where
                              monEq : (a + b , e) ≡ (b + a , e')
                              monEq = PE.cong₂ _,_ (+-comm a b) e≡e'

Here I would like to avoid introducing extra function  aux001,  it is
better to write  "with compare e' e ..."  directly in the first line. 
But Agda does not allow this.
Neither it is type-checked  "= case compare e' e of \ ...". 

So that I am forced to insert many parasitic functions  aux-ijkl,  and
cannot omit their signatures.

Can anybody, please, demonstrate how to avoid this aux001 ?
(see this place in the code).

3) A naive question: why does one need to write these  inspect - 
   rewrite  construct in the fragments like

       with compare e e' | PE.inspect (compare e) e'
   ... | tri< _ _ _ | PE.[ rw-e<e' ] rewrite rw-e<e'  <foo>
 
   ?
   By writing  
               with compare e e' 
           ... | tri< e<e' _ _ = <foo>
 
   does not one presume that  <foo>  is rewritten by  e<e' ?  

Thanks,

------
Sergei


-------------- next part --------------
open import Relation.Binary using (Tri; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
                                                          _∎ to _≡end)
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.Simple using (+-comm; +-assoc)
open import Data.Nat.Properties using (strictTotalOrder)

open import Function using (case_of_)

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

open StrictTotalOrder strictTotalOrder using (compare)
                                       renaming (trans to <-trans)

Mon : Set 
Mon = ℕ × ℕ 

open Tri 

add : 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≈ _ _ _ = (a + b , e) ∷ mons
  
------------------------------------------------------------------------------
comm :  ∀ a e b e' mons → add (a , e ) (add (b , e') mons) ≡ 
                          add (b , e') (add (a , e ) mons)

comm a e b e' []  with compare e e' 

comm a e b e' [] | tri> _ _ e>e'  with compare e' e 

comm a e b e' [] | tri> _ _ _    | tri< _    _ _ = PE.refl
comm a e b e' [] | tri> _ _ e>e' | tri> e'≮e _ _ = ⊥-elim (e'≮e e>e')
comm a e b e' [] | tri> _ _ e>e' | tri≈ e'≮e _ _ = ⊥-elim (e'≮e e>e')

comm a e b e' [] | tri≈ _ e≡e' _ =  aux 
     where
     e'≡e = PE.sym e≡e'

     aux : (a + b , e) ∷ [] ≡ add (b , e') ((a , e) ∷ []) 
     aux 
         with compare e' e
     ... | tri> _ e'≢e _ =  ⊥-elim (e'≢e e'≡e)
     ... | tri< _ e'≢e _ =  ⊥-elim (e'≢e e'≡e)
     ... | tri≈ _ _    _ =  PE.cong (_∷ []) monEq
                            where
                            monEq : (a + b , e) ≡ (b + a , e')
                            monEq = PE.cong₂ _,_ (+-comm a b) e≡e'

comm a e b e' [] | tri< e<e' _ _  with compare e' e 

comm a e b e' [] | tri< _    _ _ | tri> _    _ _ =  PE.refl 
comm a e b e' [] | tri< e<e' _ _ | tri≈ _ _ e'≯e =  ⊥-elim (e'≯e e<e')
comm a e b e' [] | tri< e<e' _ _ | tri< _ _ e'≯e =  ⊥-elim (e'≯e e<e')


comm a e b e' ((c , e₁) ∷ mons)  with compare e e₁ | PE.inspect (compare e) e₁
...
    | tri> _ _ e>e₁ | PE.[ rw-e>e₁ ] rewrite rw-e>e₁ =  aux0
    where
    aux0 : add (a , e ) (add (b , e') ((c , e₁) ∷ mons)) ≡ 
           add (b , e') ((a , e ) ∷ (c , e₁) ∷ mons)
    aux0 
        with compare e' e₁ | PE.inspect (compare e') e₁
    ... | tri> _ _ e'>e₁ | PE.[ rw-e'>e₁ ] rewrite rw-e'>e₁ =  aux00 
        where
        aux00 : add (a , e ) ((b , e') ∷ (c , e₁) ∷ mons) ≡ 
                add (b , e') ((a , e ) ∷ (c , e₁) ∷ mons)
        aux00 
            with compare e e' | PE.inspect (compare e) e'
        ... | tri> _ _ e>e' | PE.[ rw-e>e' ] rewrite rw-e>e' =  aux000
            where
            aux000 : (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons  ≡ 
                     add (b , e') ((a , e ) ∷ (c , e₁) ∷ mons)
            aux000 
                   with compare e' e | PE.inspect (compare e') e
            aux000 | tri< e'<e _ _ | PE.[ rw-e'<e ] rewrite rw-e'<e 
                                                            with compare e' e₁
            -- (c1)  but  e'>e₁  is inspected above

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

        -- e>e₁ e'>e₁
        ... | tri≈ _ e≡e' _ | PE.[ rw-e≡e' ] rewrite rw-e≡e' =  aux001  
            where
            -- (c2) Failed with avoiding extra function aux001.
            --      Why direct   compare e' e  ...  is rejected?

            -- e>e₁ e'>e₁ e≡e'
            aux001 :  (a + b , e) ∷ (c , e₁) ∷ mons  ≡ 
                      add (b , e') ((a , e ) ∷ (c , e₁) ∷ mons)
            aux001 
                with compare e' e
            ... | tri> _ e'≢e _ =  ⊥-elim (e'≢e (PE.sym e≡e'))
            ... | tri< _ e'≢e _ =  ⊥-elim (e'≢e (PE.sym e≡e'))
            ... | tri≈ _ _    _ =  PE.cong (_∷ ((c , e₁) ∷ mons)) monEq
                                   where
                                   monEq : (a + b , e) ≡ (b + a , e')
                                   monEq = PE.cong₂ _,_ (+-comm a b) e≡e'
 
        ... | tri< e<e' _ _ | PE.[ rw-e<e' ] rewrite rw-e<e'
                                             with compare e e₁ | compare e' e
        -- (c3) but  e>e₁  is inspected above 

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


    ... | tri≈ _ e'≡e₁ _ | PE.[ rw-e'≡e₁ ] rewrite rw-e'≡e₁ =  aux01
        where
        -- e>e₁ e'≡e₁
        e₁≡e' = PE.sym e'≡e₁

        e>e' : e > e'
        e>e' = PE.subst (e >_) e₁≡e' e>e₁

        aux01 :  add (a , e) ((b + c , e') ∷ mons) ≡ 
                 add (b , e') ((a , e) ∷ (c , e₁) ∷ mons)
        aux01 
            with compare e e' | PE.inspect (compare e) e'   
        ... | tri≈ _ _ e≯e' | _              = ⊥-elim (e≯e' e>e') 
        ... | tri< _ _ e≯e' | _              = ⊥-elim (e≯e' e>e') 
        ... | tri> _ _ e>e' | PE.[ rw-e>e' ] rewrite rw-e>e' =  aux010
            where
            aux010 :  (a , e) ∷ (b + c , e') ∷ mons ≡ 
                      add (b , e') ((a , e) ∷ (c , e₁) ∷ mons)
            aux010 
                with compare e' e | compare e' e₁ | PE.inspect (compare e') e₁

            -- (c4) but  e'≡e₁  is inspected above

            ... | tri< _ _ _    | tri≈ _ _ _     | PE.[ rw-e'≡e₁ ] 
                                                   rewrite rw-e'≡e₁ =  PE.refl
            ... | tri> e≯e' _ _ | _              | _ = ⊥-elim (e≯e' e>e') 
            ... | tri≈ e≯e' _ _ | _              | _ = ⊥-elim (e≯e' e>e') 
            ... | _             | tri> _ e'≢e₁ _ | _ = ⊥-elim (e'≢e₁ e'≡e₁) 
            ... | _             | tri< _ e'≢e₁ _ | _ = ⊥-elim (e'≢e₁ e'≡e₁) 


    ... | tri< e'<e₁ _ _ | PE.[ rw-e'<e₁ ] rewrite rw-e'<e₁ =  aux02
        where
        -- e>e₁ e'<e₁ 
        e'<e = <-trans e'<e₁ e>e₁

        aux02 :  add (a , e ) ((c , e₁) ∷ (add (b , e') mons)) ≡ 
                 add (b , e') ((a , e ) ∷ (c , e₁) ∷ mons)
        aux02 
            with compare e e₁ 

        -- (c5) but  e>e₁  is inspected above

        ... | tri≈ _ _ e≯e₁  =  ⊥-elim (e≯e₁ e>e₁) 
        ... | tri< _ _ e≯e₁  =  ⊥-elim (e≯e₁ e>e₁) 
        ... | tri> _ _ e>e₁  with compare e' e 

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

        -- (c6) but  e'<e₁  is inspected above

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


... | tri≈ e≮e₁ e≡e₁ e≯e₁  | PE.[ rw-e≡e₁ ] rewrite rw-e≡e₁ =  aux0
    where
    aux0 :  add (a , e ) (add (b , e') ((c , e₁) ∷ mons))  ≡ 
            add (b , e') ((a + c , e) ∷ mons)
    aux0 
        with compare e' e₁ | PE.inspect (compare e') e₁
    ... | tri> _ _ e'>e₁ | PE.[ rw-e'>e₁ ] rewrite rw-e'>e₁ =  aux00
        where
        -- e≡e₁ e'>e₁ 
        e'>e = PE.subst (e' >_) (PE.sym e≡e₁)  e'>e₁ 

        aux00 :  add (a , e) ((b , e') ∷ (c , e₁) ∷ mons)  ≡ 
                 add (b , e') ((a + c , e) ∷ mons)
        aux00 
            with compare e' e | PE.inspect (compare e') e
        ... | tri≈ _    _    e'≯e | _              =  ⊥-elim (e'≯e e'>e)
        ... | tri< _    _    e'≯e | _              =  ⊥-elim (e'≯e e'>e)
        ... | tri> e'≮e e'≢e e'>e | PE.[ rw-e'>e ] rewrite rw-e'>e 
                                 with compare e e' | PE.inspect (compare e) e'
        ...   | tri> _ _    e>e' | _          =  ⊥-elim (e'≮e e>e')
        ...   | tri≈ _ e≡e' _    | _          =  ⊥-elim (e'≢e (PE.sym e≡e'))
        ...   | tri< e<e' _ _    | PE.[ rw-e<e' ] rewrite rw-e<e'
                                                             with compare e e₁ 
        ...                        | tri≈ _  e≡e₁ _    = PE.refl
        ...                        | tri> _  _    e>e₁ = ⊥-elim (e≯e₁ e>e₁)
        ...                        | tri< e<e₁ _ _     = ⊥-elim (e≮e₁ e<e₁)


    ... | tri≈ e'≮e₁ e'≡e₁ e'≯e₁ | PE.[ rw-e'≡e₁ ] rewrite rw-e'≡e₁ =  aux01
        -- e≡e₁ e'≡e₁ 
        where
        e≡e' = PE.trans e≡e₁ (PE.sym e'≡e₁)  

        aux01 :  add (a , e)  ((b + c , e') ∷ mons)  ≡ 
                 add (b , e') ((a + c , e)  ∷ mons)
        aux01 
            with compare e e' | compare e' e
        ... | tri> _ e≢e' _ | _             =  ⊥-elim (e≢e' e≡e')
        ... | tri< _ e≢e' _ | _             =  ⊥-elim (e≢e' e≡e')
        ... | _             | tri> _ e'≢e _ =  ⊥-elim (e'≢e (PE.sym e≡e'))
        ... | _             | tri< _ e'≢e _ =  ⊥-elim (e'≢e (PE.sym e≡e'))
        ... | tri≈ _ _ _    | tri≈ _ _ _    =  PE.cong (_∷ mons) monEq
              where
              a+b+c≡b+a+c = ≡begin 
                              a + (b + c)    ≡[ PE.sym (+-assoc a b c) ]
                              (a + b) + c    ≡[ PE.cong (_+ c) (+-comm a b) ] 
                              (b + a) + c    ≡[ +-assoc b a c ] 
                              b + (a + c)
                            ≡end
              monEq = PE.cong₂ _,_ a+b+c≡b+a+c e≡e'

    ... | tri< e'<e₁ e'≢e₁ e'≯e₁ | PE.[ rw-e'<e₁ ] =  aux02
        where
        -- e≡e₁ e'<e₁.  Why is  e≡e₁  forgotten?
        e₁≡e = PE.sym e≡e₁
        e'≢e = PE.subst (e' ≢_) (PE.sym e≡e₁) e'≢e₁
        e'≯e = PE.subst (_≮ e') e₁≡e e'≯e₁

        aux02 :  add (a , e) ((c , e₁) ∷ (add (b , e') mons))  ≡ 
                 add (b , e') ((a + c , e) ∷ mons)
        aux02 
            with compare e e₁ | PE.inspect (compare e) e₁
        ... | tri> _ e≢e₁ _ | _        = ⊥-elim (e≢e₁ e≡e₁)
        ... | tri< _ e≢e₁ _ | _        = ⊥-elim (e≢e₁ e≡e₁)
        ... | tri≈ _ e≡e₁ _ | PE.[ rw-e≡e₁ ] rewrite rw-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)


... | tri< e<e₁ _ _ | PE.[ rw-e<e₁ ] rewrite rw-e<e₁ =  aux0
    where
    aux0 : add (a , e ) (add (b , e') ((c , e₁) ∷ mons)) ≡ 
           add (b , e') ((c , e₁) ∷ (add (a , e) mons))
    aux0 
        with compare e' e₁ | PE.inspect (compare e') e₁
    ... | tri> _ _ e'>e₁ | PE.[ rw-e'>e₁ ] rewrite rw-e'>e₁ =  aux00 
        where
        e<e' = <-trans e<e₁ e'>e₁
        
        -- e<e₁ e'>e₁ e<e'
        aux00 :  add (a , e) ((b , e') ∷ (c , e₁) ∷ mons) ≡ 
                 (b , e') ∷ (c , e₁) ∷ (add (a , e) mons)
        aux00 
            with compare e e' 
        ... | tri≈ e≮e' _ _  = ⊥-elim (e≮e' e<e') 
        ... | tri> e≮e' _ _  = ⊥-elim (e≮e' e<e') 
        ... | tri< _    _ _  with compare e e₁
        ...                  | tri< _    _ _ =  PE.refl
        ...                  | tri> e≮e₁ _ _ =  ⊥-elim (e≮e₁ e<e₁)
        ...                  | tri≈ e≮e₁ _ _ =  ⊥-elim (e≮e₁ e<e₁)

    ... | tri≈ _ e'≡e₁ _ | _ =  aux01
        where
        -- e<e₁ e'≡e₁
        e<e' = PE.subst (e <_) (PE.sym e'≡e₁) e<e₁

        aux01 :  add (a , e) ((b + c , e') ∷ mons) ≡ 
                 (b + c , e') ∷ (add (a , e) mons)
        aux01 
            with compare e e' 
        ... | tri< _    _ _ = PE.refl  
        ... | tri> e≮e' _ _ = ⊥-elim (e≮e' e<e')
        ... | tri≈ e≮e' _ _ = ⊥-elim (e≮e' e<e')

    ... | tri< e'<e₁ _ _ | PE.[ rw-e'<e₁ ] rewrite rw-e'<e₁ 
                                                   with compare e e₁
    ...                       | tri> e≮e₁ _ _ =  ⊥-elim (e≮e₁ e<e₁)
    ...                       | tri≈ e≮e₁ _ _ =  ⊥-elim (e≮e₁ e<e₁)
    ...                       | tri< _    _ _ =  
                                    PE.cong ((c , e₁) ∷_) (comm a e b e' mons)


More information about the Agda mailing list