Объясните этот странный эффект по порядку аргументов (и, если возможно, предоставьте обходной путь)

Question

При попытке найти решение вопроса, заданного мной here, я обнаружил, что приемлемость (по Agda) refl proof зависит от странным образом по порядку аргументов функции, вызываемой с одной стороны уравнения.

В приведенном ниже коде смотрите, как доказано, что все, кроме одного из нижних 4 теорем, refl. Важно отметить, что join и join' отличаются только порядком аргументов. Соответственно, я думаю, что thm s, которые их вызывают, должны быть доказаны эквивалентно, но, видимо, это не так.

Почему разница? Означает ли это ошибку в Агда? Как доказать оставшуюся теорему (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(') 

Если я пытаюсь доказать thm1 с 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) 

NB: Это использует Agda 2.4.2.3 и STDLIB той же версии (извлекается из 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 

В thm1 Agda заставляет первый аргумент (tl) находиться в WHNF, даже если предложение можно определить, посмотрев третий аргумент join, а затем на первый.