从参数的顺序解释这种奇怪的效果（并提供解决方法，如果可能的话）

Question

在尝试为我提出的问题提出解决方案时 here，我发现 refl 证明的可接受性（通过 Agda）以一种奇怪的方式取决于函数参数的顺序在等式的一侧调用。

在下面的代码中，看看除了底部 4 个定理中的一个以外，其他所有定理都是如何用 refl 证明的。重要的是要注意 join 和 join' 仅在参数顺序上有所不同。相应地，我认为调用它们的 thms 应该被等价地证明，但显然事实并非如此。

为什么会出现差异？这是否代表 Agda 中的错误？我将如何证明剩余的定理 (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(')

如果我尝试用 refl 证明 thm1，我会得到以下错误：

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)

注意：这是使用 Agda 2.4.2.3 和相同版本的标准库（来自 github here.

Answer 1

你可以写

thm1  : ∀ {h : ℕ} (tl : Tree (suc h)) (tr : Tree (suc h)) → join (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)
thm1 (node tl (node tl₁ tl₂ bal) ∼+) tr = refl
thm1 (node tl  leaf              ∼0) tr = refl
thm1 (node tl (node tl₁ tl₂ bal) ∼0) tr = refl
thm1 (node tl  leaf              ∼-) tr = refl
thm1 (node tl (node tl₁ tl₂ bal) ∼-) tr = refl

In thm1 Agda 强制第一个参数 (tl) 在 WHNF 中，即使可以通过查看 join 的第三个参数然后在第一个.

从参数的顺序解释这种奇怪的效果（并提供解决方法，如果可能的话）

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

agda