<div dir="ltr">(NB: Crossposted to <a href="http://stackoverflow.com/q/31913210/1312174">http://stackoverflow.com/q/31913210/1312174</a>)<br><div><br>While trying to come up with a solution to a question I posed [here](<a href="http://stackoverflow.com/questions/31900036/proof-help-in-agda-node-balancing-in-data-avl">http://stackoverflow.com/questions/31900036/proof-help-in-agda-node-balancing-in-data-avl</a>), 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. <br><br>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.<br><br>Why the discrepancy? Does this represent a bug in Agda? How would I prove the remaining theorem (`thm1`)?<br><br>   open import Data.Nat<br>   open import Data.Product<br><br>   -- Stolen (with little modification) from Data.AVL<br><br>   data â„•â‚‚ : Set where<br>     0# : â„•â‚‚<br>     1# : â„•â‚‚<br><br>   infixl 6 _⊕_<br><br>   _⊕_ : â„•â‚‚ → â„• → â„•<br>   0# ⊕ n = n<br>   1# ⊕ n = suc n<br><br>   infix 4 _∼_⊔_<br><br>   data _∼_⊔_ : â„• → â„• → â„• → Set where<br>     ∼+ : ∀ {n} →    n ∼ suc n ⊔ suc n<br>     ∼0 : ∀ {n} →    n ∼ n    ⊔ n<br>     ∼- : ∀ {n} → suc n ∼ n    ⊔ suc n<br><br>   max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m<br>   max∼ ∼+ = ∼-<br>   max∼ ∼0 = ∼0<br>   max∼ ∼- = ∼0<br><br>   ∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m<br>   ∼max ∼+ = ∼0<br>   ∼max ∼0 = ∼0<br>   ∼max ∼- = ∼+<br><br>   -- for simplicity, this tree has no keys<br>   data Tree : â„• → Set where<br>     leaf : Tree 0<br>     node : ∀ {l u h}<br>            (L : Tree l)<br>            (U : Tree u)<br>            (bal : l ∼ u ⊔ h) →<br>            Tree (suc h)<br><br>   -- similar to joinˡ⺠from Data.AVL<br><br>   join : ∀ {hË¡ hʳ h : â„•} →<br>          (∃ λ i → Tree (i ⊕ hË¡)) →<br>          Tree hʳ →<br>          (bal : hË¡ ∼ hʳ ⊔ h) →<br>          ∃ λ i → Tree (i ⊕ (suc h))<br>   join (1# , node tâ‚<br>                   (node t₃ tâ‚… bal)<br>                   ∼+) t₇ ∼- = (0# , node <br>                                           (node tâ‚ t₃ (max∼ bal))<br>                                           (node tâ‚… t₇ (∼max bal))<br>                                           ∼0)<br>   join (1# , node tâ‚ t₃ ∼-) tâ‚… ∼- = (0# , node tâ‚ (node t₃ tâ‚… ∼0) ∼0)<br>   join (1# , node tâ‚ t₃ ∼0) tâ‚… ∼- = (1# , node tâ‚ (node t₃ tâ‚… ∼-) ∼+)<br>   join (1# , tâ‚)           t₃ ∼0 = (1# , node tâ‚ t₃ ∼-)<br>   join (1# , tâ‚)           t₃ ∼+ = (0# , node tâ‚ t₃ ∼0)<br>   join (0# , tâ‚)           t₃ bal = (0# , node tâ‚ t₃ bal)<br><br>   -- just like join but with "bal" earlier in the argument list<br>   join' : ∀ {hË¡ hʳ h : â„•} →<br>          (bal : hË¡ ∼ hʳ ⊔ h) →<br>          (∃ λ i → Tree (i ⊕ hË¡)) →<br>          Tree hʳ →<br>          ∃ λ i → Tree (i ⊕ (suc h))<br>   join' ∼- (1# , node tâ‚<br>                   (node t₃ tâ‚… bal)<br>                   ∼+) t₇ = (0# , node <br>                                           (node tâ‚ t₃ (max∼ bal))<br>                                           (node tâ‚… t₇ (∼max bal))<br>                                           ∼0)<br>   join' ∼- (1# , node tâ‚ t₃ ∼-) tâ‚… = (0# , node tâ‚ (node t₃ tâ‚… ∼0) ∼0)<br>   join' ∼- (1# , node tâ‚ t₃ ∼0) tâ‚… = (1# , node tâ‚ (node t₃ tâ‚… ∼-) ∼+)<br>   join' ∼0 (1# , tâ‚)           t₃ = (1# , node tâ‚ t₃ ∼-)<br>   join' ∼+ (1# , tâ‚)           t₃ = (0# , node tâ‚ t₃ ∼0)<br>   join' bal (0# , tâ‚)           t₃ = (0# , node tâ‚ t₃ bal)<br><br>   open import Relation.Binary.PropositionalEquality<br><br>   thm0 : ∀ {h : â„•} (tl : Tree     h ) (tr : Tree (suc h)) → join (0# , tl) tr ∼+ ≡ (0# , node tl tr ∼+)<br>   thm0 tl tr = refl<br><br>   thm1 : ∀ {h : â„•} (tl : Tree (suc h)) (tr : Tree (suc h)) → join (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)<br>   thm1 tl tr = {!!} -- FIXME refl doesn't work here!<br><br>   thm0' : ∀ {h : â„•} (tl : Tree     h ) (tr : Tree (suc h)) → join' ∼+ (0# , tl) tr ≡ (0# , node tl tr ∼+)<br>   thm0' tl tr = refl<br><br>   thm1' : ∀ {h : â„•} (tl : Tree (suc h)) (tr : Tree (suc h)) → join' ∼+ (1# , tl) tr ≡ (0# , node tl tr ∼0)<br>   thm1' tl tr = refl -- refl works fine here, and all I did was switch the order of arguments to join(')<br><br>If I try to prove `thm1` with refl, I get the following error:<br><br>   projâ‚ (join (1# , tl) tr ∼+) != 0# of type â„•â‚‚<br>   when checking that the expression refl has type<br>   join (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)<br><br>NB: This is using Agda 2.4.2.3 and the stdlib of the same version (pulled from github [here](<a href="https://github.com/agda/agda-stdlib/tree/2.4.2.3">https://github.com/agda/agda-stdlib/tree/2.4.2.3</a>).<br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div>