How to tell Agda to unfold a definition to prove an equivalency

I have a function like this:

open import Data.Char
open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true = 123
... | false = 456

I would like to prove that when I call it with the same argument (foo c c), it always yields 123:

foo-eq⇒123 : ∀ (c : Char) → foo c c ≡ 123
foo-eq⇒123 c =
  foo c c ≡⟨ {!!} ⟩
  123 ∎

I am able to use refl to prove a trivial example:

foo-example : foo 'a' 'a' ≡ 123
foo-example = refl

So, I would think that I could just put refl in the hole since all Agda needs to do is beta-reduce foo c c. However, replacing the hole with refl yields the following error:

.../Unfold.agda:15,14-18
(foo c c
 | Relation.Nullary.Decidable.Core.isYes
   (Relation.Nullary.Decidable.Core.map′ Data.Char.Properties.≈⇒≡
    Data.Char.Properties.≈-reflexive
    (Relation.Nullary.Decidable.Core.map′
     (Data.Nat.Properties.≡ᵇ⇒≡ (toℕ c) (toℕ c))
     (Data.Nat.Properties.≡⇒≡ᵇ (toℕ c) (toℕ c)) (T? (toℕ c ≡ᵇ toℕ c)))))
!= 123 of type ℕ
when checking that the expression refl has type foo c c ≡ 123

I suspect the issue is that Agda doesn't automatically understand that c == c is true for all c:

c==c : ∀ (c : Char) → (c == c) ≡ true
c==c c = refl

.../Unfold.agda:23,10-14
Relation.Nullary.Decidable.Core.isYes
(Relation.Nullary.Decidable.Core.map′ Data.Char.Properties.≈⇒≡
 Data.Char.Properties.≈-reflexive
 (Relation.Nullary.Decidable.Core.map′
  (Data.Nat.Properties.≡ᵇ⇒≡ (toℕ c) (toℕ c))
  (Data.Nat.Properties.≡⇒≡ᵇ (toℕ c) (toℕ c)) (T? (toℕ c ≡ᵇ toℕ c))))
!= true of type Bool
when checking that the expression refl has type (c == c) ≡ true

So, what is the right way to prove my foo-eq⇒123 theorem?

Solution

Agda's built-in Char type is a little weird. Let's contrast it with a non-weird built-in type, ℕ. The equality test for ℕ looks as follows.

_≡ᵇ_ : Nat → Nat → Bool
zero  ≡ᵇ zero  = true
suc n ≡ᵇ suc m = n ≡ᵇ m
_     ≡ᵇ _     = false

Note that n ≡ᵇ n doesn't reduce to true, either. After all, Agda doesn't know whether n is zero or suc, i.e., which of the two clauses to apply for the reduction. So, this has the same problem as your Char example. But for ℕ there is an easy way out.

Let's look at your example again and let's also add a ℕ-based version of foo, bar.

open import Data.Char using (Char ; _==_ ; _≟_)
open import Data.Nat using (ℕ ; zero ; suc ; _≡ᵇ_)
open import Data.Bool using (true ; false)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary using (yes ; no)
open import Relation.Nullary.Negation using (contradiction)

foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true  = 123
... | false = 456

bar : ℕ → ℕ → ℕ
bar n1 n2 with n1 ≡ᵇ n2
... | true  = 123
... | false = 456

So, what's the easy way out for ℕ? We pattern match / do a case split on n to reduce n ≡ᵇ n just enough to do our proof. I.e., either to the base case zero or to the next recursive step suc n.

bar-eq⇒123 : ∀ n → bar n n ≡ 123
bar-eq⇒123 zero    = refl
bar-eq⇒123 (suc n) = bar-eq⇒123 n

ℕ just has two constructors and we know what ≡ᵇ looks like, so pattern matching is straight forward.

For Char, things are way more complicated. Long story short, the equality test for Char is defined in terms of a function toℕ that Agda doesn't give us a definition for. Also, the Char data type is postulated and doesn't come with any constructors. So a proof like bar-eq⇒123 is not an option for Char. We don't have clauses and we don't have constructors. (I wouldn't call, say, 'a' a constructor for Char. Similarly to how 1234 is not a constructor for ℕ.)

So, what could we do? Note that c == c in the error message that you quoted reduces to something pretty complicated that involves isYes. If we reduced c == c only a tiny little bit (instead of as much as possible), we'd get isYes (c ≟ c) (instead of the complicated thing from the error message).

_≟_ is the decidable equality for Char (i.e., a combination of an "Equal or not?" Boolean and a proof). isYes strips away the proof and gives us the Boolean.

My idea for a proof would then be to not do a case split on c (as we did for ℕ), but on c ≟ c. This would yield two cases and reduce the isYes to true or false, respectively. The true case would be obvious. The false case could be dicharged by contradiction with the proof from the decidable equality.

foo-eq⇒123 : ∀ c → foo c c ≡ 123
foo-eq⇒123 c with c ≟ c
... | yes p = refl
... | no ¬p = contradiction refl ¬p

Note that, in turn, this proof doesn't easily translate to ℕ, as _≡ᵇ_ isn't based on decidable equality and isYes. It's a primitive instead.

Maybe an even better idea would be to consistently stick to decidable equality, for Char as well as ℕ instead of using _==_ or _≡ᵇ_. foo would then look as follows.

baz : Char → Char → ℕ
baz c1 c2 with c1 ≟ c2
... | yes p = 123
... | no ¬p = 456

And the foo-eq⇒123 proof would apply to it unchanged.