<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&#39;s important to note that `join` and `join&#39;` 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 &quot;bal&quot; earlier in the argument list<br>    join&#39; : âˆ€ {hË¡ hʳ h : â„•} â†’<br>           (bal : hË¡ âˆ¼ hʳ âŠ” h) â†’<br>           (∃ Î» i â†’ Tree (i âŠ• hË¡)) â†’<br>           Tree hʳ â†’<br>           âˆƒ Î» i â†’ Tree (i âŠ• (suc h))<br>    join&#39; âˆ¼- (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&#39; âˆ¼-  (1# , node t₁ t₃ âˆ¼-) tâ‚… = (0# , node t₁ (node t₃ tâ‚… âˆ¼0) âˆ¼0)<br>    join&#39; âˆ¼-  (1# , node t₁ t₃ âˆ¼0) tâ‚… = (1# , node t₁ (node t₃ tâ‚… âˆ¼-) âˆ¼+)<br>    join&#39; âˆ¼0  (1# , t₁)            t₃ = (1# , node t₁ t₃ âˆ¼-)<br>    join&#39; âˆ¼+  (1# , t₁)            t₃ = (0# , node t₁ t₃ âˆ¼0)<br>    join&#39; 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&#39;t work here!<br><br>    thm0&#39; : âˆ€ {h : â„•} (tl : Tree      h ) (tr : Tree (suc h)) â†’ join&#39; âˆ¼+ (0# , tl) tr â‰¡ (0# , node tl tr âˆ¼+)<br>    thm0&#39; tl tr = refl<br><br>    thm1&#39; : âˆ€ {h : â„•} (tl : Tree (suc h)) (tr : Tree (suc h)) â†’ join&#39; âˆ¼+ (1# , tl) tr â‰¡ (0# , node tl tr âˆ¼0)<br>    thm1&#39; tl tr = refl -- refl works fine here, and all I did was switch the order of arguments to join(&#39;)<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>