从论点的顺序解释这种奇怪的影响(如果可能的话,提供一个解决方法)

在试图解决我提出的问题时 here ,我发现refl证明的可接受性(由Agda)以一种奇怪的方式取决于在方程一侧调用的函数的参数顺序。

在下面的代码中,看看除了下面4个定理中的一个之外,其他所有定理都是如何用refl证明的。需要注意的是 join 和 join' 仅在参数的顺序上不同。相应地,我认为 thm 调用它们的s应该被等价地证明,但显然不是这样。

为什么会出现这种差异?这是否代表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(')

如果我想证明 第1页 使用refl,我得到以下错误:

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和相同版本的stdlib(从github中提取 here .