[Agda] Why the light gray highlighting here?

[Thomas Lopatic]

Hello there,

I think that the most practical consequence of what Agda is warning you 
about is that some applications of _xor_ won't reduce as expected. Let's 
normalize something in Emacs based on your definitions:

   norm₁ : Bin → Bin
   norm₁ y = { ⟨⟩ xor y  }0

Normalizing the above goal reduces it to y. That's expected, because 
that's the definitional equality given by your first _xor_ clause, which 
says that "⟨⟩ xor y" is equal to y by definition.

Now for the highlighted line. Let's normalize again:

   norm₂ : Bin → Bin
   norm₂ x = { x xor ⟨⟩ }1

We normalize the above goal... and... and... aaaaaaaand... nothing 
happens. It's "normalized" to "x xor ⟨⟩".

What's going on? After all, the second clause says that, by definition, 
"x xor ⟨⟩" is equal to x. That's definitional equality! Go use it, Agda! 
Why would you use the first clause's definitional equality for 
reduction, but not the second clause's?

--- Start of undergraduate handwaving. Somebody please speak up, if I'm 
spreading fake news here. ---

For efficient reduction of applications of your _xor_ function, Agda 
builds a decision tree based on your pattern matches. When reducing an 
application, Agda consults this decision tree to figure out which of the 
clauses to pick for the arguments given in the application. At each 
level of the tree, one of the arguments is consulted to decide which 
branch to take to the next level of the tree. When Agda hits a leaf, 
this leaf tells her which clause to pick.

In your case, the first level of the decision tree corresponds to the 
first argument. Is it ⟨⟩? Or is it O? Or I? In the first normalization 
above, the one about "⟨⟩ xor y", this question can be answered: The 
first argument is ⟨⟩. So Agda can proceed to the second level of the 
decision tree, i.e., to the second argument. Progress!

In the second normalization above, however, Agda cannot answer this 
question. The first argument is x. Could be anything. Agda thus doesn't 
know which branch of the decision tree to take at the first level, so 
she can't proceed to the next level, i.e., to the second argument. End 
of story. No reduction to x for us. Too bad, so sad.

--- End of undergraduate handwaving. ---

I typically encounter this when it impacts propositional equality in 
proofs and my ability to refl my way out of a proof. Let's consider 
again the first of the above normalizations. I can refl my way out of 
this:

   proof₁ : ∀ y → ⟨⟩ xor y ≡ y
   proof₁ y = refl

Why does this work? Well, as seen above, "⟨⟩ xor y" reduces (normalizes) 
to y, so we have "y ≡ y", which is refl.

In contrast, I cannot refl my way out of this:

   proof₂ : ∀ x → x xor ⟨⟩ ≡ x
   proof₂ x = refl -- does not type-check

As seen in the second "normalization" above, "x xor ⟨⟩" doesn't reduce. 
So, we are stuck with "x xor ⟨⟩ ≡ x", which isn't refl.

What to do about it? In order to make it past the first level of the 
decision tree, we need to give Agda as the first argument a concrete 
data constructor for Bin to work with, instead of just x. Based on this 
data constructor Agda can then pick which branch to take from the first 
to the second level.

But which of the constructors do we use in lieu of x? Well, as x can be 
anything, the answer is: all of them. This is accomplished by a case 
split on x. Let's ask Agda's Emacs mode to do this for us:

   proof₂ ⟨⟩ =  { }2
   proof₂ (x O) =  { }3
   proof₂ (x I) =  { }4

Now we can refl out way out of this again:

   proof₂ ⟨⟩ = refl
   proof₂ (x O) = refl
   proof₂ (x I) = refl

While the above scenarios are easy to spot, this can also bite you in 
proofs where a function has a larger number of arguments. I find that I 
sometimes unexpectedly have to case-split on an argument, because that's 
what the decision tree wants, even though my proof doesn't require the 
resulting cases of the argument to be considered separately. I then put 
the proof shared between the resulting cases in a lemma and use that 
lemma to prove the cases in one simple step per case, just like the 
above three refls.

All in all, if a function application doesn't reduce, then you need to 
figure out what the decision tree really wants from you.

If you prefer a more rigorous answer to all of this, then there's the 
following paper by Jesper Cockx and Andreas Abel, which explains 
elaboration from clauses to a case tree in detail:

   
https://www.cambridge.org/core/journals/journal-of-functional-programming/article/elaborating-dependent-copattern-matching-no-pattern-left-behind/F13CECDAB2B6200135D45452CA44A8B3

So, that's how definitional equality seems to kind of break down 
sometimes. Thence the highlighting.

I hope all of this helps to provide some additional context.

Thomas

On 2020-09-29 16:01, David Banas wrote:
> Hi all,
> 
> I'm wondering why the second line in my definition for `XOR` below is
> being partially highlighted in a very light gray background, as shown.
> 
> Thanks,
> -db
> 
> data Bin : Set where
>   ⟨⟩ : Bin
>   _O : Bin → Bin
>   _I : Bin → Bin
> 
> _xor_ : Bin → Bin → Bin
> ⟨⟩    xor y      =  y
> x     xor ⟨⟩     =  x
> (x O) xor (y O)  = (x xor y) O
> (x O) xor (y I)  = (x xor y) I
> (x I) xor (y O)  = (x xor y) I
> (x I) xor (y I)  = (x xor y) O
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda