[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