[Agda] Explain this strange effect from the order of arguments (and provide a workaround, if possible)

[Jacques Carette]

You will find an (operational) explanation at the bottom of
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching

So order of arguments (and order of clauses) matter, because of the 
semantics in terms of case trees.

Jacques

On 2015-08-10 05:49 , Martin Stone Davis wrote:
> (NB: Crossposted to http://stackoverflow.com/q/31913210/1312174)
>
> While trying to come up with a solution to a question I posed 
> [here](http://stackoverflow.com/questions/31900036/proof-help-in-agda-node-balancing-in-data-avl), 
> I discovered that the acceptability (by Agda) of a refl proof depends 
> in a strange way on the order of arguments of a function that is 
> called on one side of the equation.
>
> In code below, see how all but one of the bottom 4 theorems are proved 
> with refl. It's important to note that `join` and `join'` differ only 
> in the order of arguments. Correspondingly, I would think that the 
> `thm`s that invoke them should be proved equivalently, but apparently 
> that is not so.
>
> Why the discrepancy? Does this represent a bug in Agda? How would I 
> prove the remaining theorem (`thm1`)?
>
>     open import Data.Nat
>     open import Data.Product
>
>     -- Stolen (with little modification) from Data.AVL
>
>     data ℕ₂ : Set where
>       0# : ℕ₂
>       1# : ℕ₂
>
>     infixl 6 _⊕_
>
>     _⊕_ : ℕ₂ → ℕ → ℕ
>     0# ⊕ n = n
>     1# ⊕ n = suc n
>
>     infix 4 _∼_⊔_
>
>     data _∼_⊔_ : ℕ → ℕ → ℕ → Set where
>       ∼+ : ∀ {n} →     n ∼ suc n ⊔ suc n
>       ∼0 : ∀ {n} →     n ∼ n     ⊔ n
>       ∼- : ∀ {n} → suc n ∼ n     ⊔ suc n
>
>     max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m
>     max∼ ∼+ = ∼-
>     max∼ ∼0 = ∼0
>     max∼ ∼- = ∼0
>
>     ∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m
>     ∼max ∼+ = ∼0
>     ∼max ∼0 = ∼0
>     ∼max ∼- = ∼+
>
>     -- for simplicity, this tree has no keys
>     data Tree : ℕ → Set where
>       leaf : Tree 0
>       node : ∀ {l u h}
>              (L : Tree l)
>              (U : Tree u)
>              (bal : l ∼ u ⊔ h) →
>              Tree (suc h)
>
>     -- similar to joinˡ⁺ from Data.AVL
>
>     join : ∀ {hˡ hʳ h : ℕ} →
>            (∃ λ i → Tree (i ⊕ hˡ)) →
>            Tree hʳ →
>            (bal : hˡ ∼ hʳ ⊔ h) →
>            ∃ λ i → Tree (i ⊕ (suc h))
>     join (1# , node t₁
>                     (node t₃ t₅ bal)
>                     ∼+) t₇ ∼-  = (0# , node
>                                             (node t₁ t₃ (max∼ bal))
>                                             (node t₅ t₇ (∼max bal))
>                                             ∼0)
>     join (1# , node t₁ t₃ ∼-) t₅ ∼-  = (0# , node t₁ (node t₃ t₅ ∼0) ∼0)
>     join (1# , node t₁ t₃ ∼0) t₅ ∼-  = (1# , node t₁ (node t₃ t₅ ∼-) ∼+)
>     join (1# , t₁)            t₃ ∼0  = (1# , node t₁ t₃ ∼-)
>     join (1# , t₁)            t₃ ∼+  = (0# , node t₁ t₃ ∼0)
>     join (0# , t₁)            t₃ bal = (0# , node t₁ t₃ bal)
>
>     -- just like join but with "bal" earlier in the argument list
>     join' : ∀ {hˡ hʳ h : ℕ} →
>            (bal : hˡ ∼ hʳ ⊔ h) →
>            (∃ λ i → Tree (i ⊕ hˡ)) →
>            Tree hʳ →
>            ∃ λ i → Tree (i ⊕ (suc h))
>     join' ∼- (1# , node t₁
>                     (node t₃ t₅ bal)
>                     ∼+) t₇  = (0# , node
>                                             (node t₁ t₃ (max∼ bal))
>                                             (node t₅ t₇ (∼max bal))
>                                             ∼0)
>     join' ∼-  (1# , node t₁ t₃ ∼-) t₅ = (0# , node t₁ (node t₃ t₅ ∼0) ∼0)
>     join' ∼-  (1# , node t₁ t₃ ∼0) t₅ = (1# , node t₁ (node t₃ t₅ ∼-) ∼+)
>     join' ∼0  (1# , t₁)            t₃ = (1# , node t₁ t₃ ∼-)
>     join' ∼+  (1# , t₁)            t₃ = (0# , node t₁ t₃ ∼0)
>     join' bal (0# , t₁)            t₃ = (0# , node t₁ t₃ bal)
>
>     open import Relation.Binary.PropositionalEquality
>
>     thm0  : ∀ {h : ℕ} (tl : Tree      h ) (tr : Tree (suc h)) → join 
> (0# , tl) tr ∼+ ≡ (0# , node tl tr ∼+)
>     thm0 tl tr = refl
>
>     thm1  : ∀ {h : ℕ} (tl : Tree (suc h)) (tr : Tree (suc h)) → join 
> (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)
>     thm1 tl tr = {!!} -- FIXME refl doesn't work here!
>
>     thm0' : ∀ {h : ℕ} (tl : Tree      h ) (tr : Tree (suc h)) → join' 
> ∼+ (0# , tl) tr ≡ (0# , node tl tr ∼+)
>     thm0' tl tr = refl
>
>     thm1' : ∀ {h : ℕ} (tl : Tree (suc h)) (tr : Tree (suc h)) → join' 
> ∼+ (1# , tl) tr ≡ (0# , node tl tr ∼0)
>     thm1' tl tr = refl -- refl works fine here, and all I did was 
> switch the order of arguments to join(')
>
> If I try to prove `thm1` with refl, I get the following error:
>
>     proj₁ (join (1# , tl) tr ∼+) != 0# of type ℕ₂
>     when checking that the expression refl has type
>     join (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)
>
> NB: This is using Agda 2.4.2.3 and the stdlib of the same version 
> (pulled from github 
> [here](https://github.com/agda/agda-stdlib/tree/2.4.2.3).
> --
> Martin Stone Davis
>
> Postal/Residential:
> 1223 Ferry St
> Apt 5
> Eugene, OR 97401
> Talk / Text / Voicemail: (310) 699-3578 <tel:3106993578>
> Electronic Mail: martin.stone.davis at gmail.com 
> <mailto:martin.stone.davis at gmail.com>
> Website: martinstonedavis.com <http://martinstonedavis.com/>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150810/547c770b/attachment.html