While trying to come up with a solution to a question I posed here, 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.
In code below, see how all but one of the bottom 4 theorems are proved with refl. It's important to note that join and join' differ only in the order of arguments. Correspondingly, I would think that the thms that invoke them should be proved equivalently, but apparently that is not so.
Why the discrepancy? Does this represent a bug in Agda? How would I prove the remaining theorem (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(')
If I try to prove thm1 with refl, I get the following error:
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: This is using Agda 2.4.2.3 and the stdlib of the same version (pulled from github here.
