Making Agda reduce an expression in a goal type

Question

Using ℕ and _≟_ from the standard library, I have

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

foo : ℕ -> ℕ -> ℕ
foo x y with x ≟ y
foo x .x | yes refl = x
foo x y  | no contra = y

data Bar : ℕ -> Set where
  bar : (x : ℕ) -> Bar (foo x x)

I want to implement

mkBar : (x : ℕ) -> Bar x
mkBar x = bar x

Agda complains,

Type mismatch:
expected: x
  actual: foo x x | x ≟ x
when checking that the expression bar x
has type Bar x

This makes sense to me: Agda doesn't know a priori that x ≟ x always evaluates to yes refl, so it's not going to evaluate foo x x until it knows a bit more about x.

So I tried rewriting the goal to force x ≟ x to resolve to yes refl,

eq-refl : forall x -> (x ≟ x) ≡ yes refl
eq-refl x with x ≟ x
eq-refl x | yes refl = refl
eq-refl x | no contra = ⊥-elim (contra refl)

mkBar : (x : ℕ) -> Bar x
mkBar x rewrite eq-refl x = bar x

but to no avail. Same error message. I also tried rewriting by foo x x ≡ x:

foo-eq : forall x -> foo x x ≡ x
foo-eq x rewrite eq-refl x = refl

mkBar : (x : ℕ) -> Bar x
mkBar x rewrite foo-eq x = bar x

This answer suggests pattern matching on x ≟ x on the left hand side of mkBar, but it also seems to have no effect:

mkBar : (x : ℕ) -> Bar x
mkBar x with x ≟ x
mkBar x | yes refl = bar x
mkBar x | no contra = ⊥-elim (contra refl)

I must be missing a trick here. How do I get rid of the | in the goal type and make foo x x reduce to x? (I'd prefer not to examine x directly in the LHS of mkBar.)

gallais gallais · Accepted Answer · 2017-05-15T22:00:51

You were almost there: the important thing to notice is that rewrite takes an x ≡ y and replaces x by y in the goal. foo-eq x has type foo x x ≡ x but there is no foo x x to replace in the goal!

What you need to do is rewrite by sym (foo-eq x) like so:

mkBar : (x : ℕ) → Bar x
mkBar x rewrite sym (foo-eq x) = bar x

Bar x then becomes Bar (foo x x) meaning you can apply your constructor.

Making Agda reduce an expression in a goal type

1 Answers