<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>