I am playing with joinˡ⁺ from the standard library's AVL tree implementation. This function is defined with six pattern matching clauses. When I apply the function to an argument, then Agda does or doesn't reduce my function application expression, depending on which of the six clauses matches my argument. (Or so it seems to me.)
Here's code that applies the function to an argument that matches the function's first clause. It's the left-hand side of the equality in the goal. Agda reduces it to the right-hand side and I can finish the proof with refl. So this one works as expected.
(Note that the code uses version 1.3 of the standard library. It seems that more recent versions moved the AVL tree code from Data.AVL to Data.Tree.AVL.)
module Repro2 where
open import Data.Nat using (ℕ ; suc)
open import Data.Nat.Properties using (<-strictTotalOrder)
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Data.AVL.Indexed <-strictTotalOrder
okay :
∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
≡
(0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)
okay k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl
The next example targets the second clause of the function definition. Unlike above, the goal does not reduce at all this time, i.e., the joinˡ⁺ doesn't go away.
not-okay : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
≡
(0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
not-okay k₄ k₂ t₁ t₃ t₅ = {!!}
What am I missing?
Addition after MrO's answer
MrO nailed it. What I knew was that if a clause pattern-matches a subterm of an argument (or the whole argument), then I obviously need to pass a matching data constructor for that subterm to make the evaluator pick that clause. However, that's not enough. As MrO pointed out, in some cases I also need to pass data constructors for subterms that other clauses (i.e., not just the clause I'm going for) pattern-match, even though the clause at hand doesn't care about them.
To explore this (to me: major new) insight, I tried out the remaining four clauses of joinˡ⁺. The last clause, clause #6, led to another insight.
Here's clause #3. It works pretty much the same as not-okay.
clause₃ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
≡
(1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
-- This does not work:
-- clause₃ k₄ k₂ t₁ t₃ t₅ = {!!}
clause₃ k₄ k₂ t₁ (node k t₃ t₄ bal) t₅ = refl
Clause #4 is more involved.
clause₄ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (1# , t₁) t₃ ∼0
≡
(1# , node k₂ t₁ t₃ ∼-)
-- This does not work:
-- clause₄ k₂ t₁ t₃ = {!!}
-- This still doesn't, because of t' (or so I thought):
-- clause₄ k₂ (node k t t′ b) t₃ = {!!}
-- Surprise! This still doesn't, because of b:
-- clause₄ k₂ (node k t (leaf l<u) b) t₃ = {!!}
-- clause₄ k₂ (node k t (node k′ t′′ t′′′ b') b) t₃ = {!!}
clause₄ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₄ k₂ (node k t (leaf l<u) ∼-) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼+) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼0) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼-) t₃ = refl
Clause #5 is analogous to clause #4.
clause₅ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
k₂ (1# , t₁) t₃ ∼+
≡
(0# , node k₂ t₁ t₃ ∼0)
clause₅ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₅ k₂ (node k t (leaf l<u) ∼-) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼+) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼0) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼-) t₃ = refl
Clause #6 was a bit of a surprise to me. I thought that I needed to pass data constructors wherever any of the clauses required them. But that's not what MrO said. And it shows in this clause:
clause₆ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (0# , t₁) t₃ b
≡
(0# , node k₂ t₁ t₃ b)
clause₆ k₂ t₁ t₃ b = refl
Easier than I thought: no additional data constructors required. Why? I went to read the pattern matching part of the Agda reference:
https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#case-trees
I had read it before, but had completely failed to apply what it says. Agda finds the clause to be picked by way of a decision tree, a case tree. To me, it now looks like Agda needs data constructors as long as it hasn't reached a leaf of the case tree, i.e., as long as it hasn't figured out which clause to pick.
For the function at hand, the case tree seems to start with the question: 0# or 1#? At least that would explain clause #6:
If it's
0#then we know that it must be clause #6, no more data constructors required. Clause #6 is the only match for0#. So, we're at a leaf, our case tree traversal is over.If it's
1#then we need to do more matching, i.e., move down in the case tree to the next level. There, we need another data constructor to look at. In total, we thus need a data constructor for each visited level of the case tree.
At least this is my current mental model, which seems to be supported by the observations made about joinˡ⁺.
Trying to validate this mental model a little more, I went and modified my copy of the standard library by reversing the order of the six clauses. As Agda builds the case tree by going through the clauses in order and going left to right within each clause, this should give us a much better case tree.
0# vs. 1# would still be the first level of the decision tree, but it would be followed by the outer balance, followed by the inner balance. We wouldn't need to split trees into nodes, except for the now last (previously first) clause, which actually matches on that.
And, indeed, things turn out as expected. Here's what the proofs look like with the reversed order of clauses in my modified standard library.
clause₁′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (0# , t₁) t₃ b
≡
(0# , node k₂ t₁ t₃ b)
clause₁′ k₂ t₁ t₃ b = refl
clause₂′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
k₂ (1# , t₁) t₃ ∼+
≡
(0# , node k₂ t₁ t₃ ∼0)
clause₂′ k₂ t₁ t₃ = refl
clause₃′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (1# , t₁) t₃ ∼0
≡
(1# , node k₂ t₁ t₃ ∼-)
clause₃′ k₂ t₁ t₃ = refl
clause₄′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
≡
(1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
clause₄′ k₄ k₂ t₁ t₃ t₅ = refl
not-okay′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
≡
(0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
not-okay′ k₄ k₂ t₁ t₃ t₅ = refl
okay′ :
∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
≡
(0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)
okay′ k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl
