Consider function wa'' (need natural number definition, either in stdlib or Agda.Builtin.Nat):

postulate comm : ∀ m n -> m + n ≡ n + m

wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m)
wa'' m n with comm n m
...        | refl = { }0

The pattern matching on comm n m with refl fails. But if I add one more match:

wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m)
wa'' m n with (n + m) | comm n m
...        | .(m + n) | refl = { }0

This code works. Is there any semantics-level difference between these two code snippets?


First, let's desugar the withs.

First definition:

wa''-aux : ∀ m n -> n + m ≡ m + n -> wa (m + n) ≡ wa (n + m)
wa''-aux m n refl = ?  -- cannot unify n + m with m + n

wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m)
wa'' m n = wa''-aux m n (comm n m)

Second definition:

wa''-aux : ∀ m n w -> w ≡ m + n -> wa (m + n) ≡ wa w
wa''-aux m n .(m + n) refl = ?

wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m)
wa'' m n = wa''-aux m n (n + m) (comm n m)

When checking that refl is a valid case, we must unify the two sides of the equation it is supposed to be a proof of. Remember that refl : {x : ℕ} → x ≡ x, so we must find a single value x that is βη-equal to both the left-hand side and right-hand side.

In the first case, this means unifying n + m with m + n, and in the second case, this means unifying w with m + n. The latter is obviously possible, where we assign w ↦ m + n and note that we have done this with the dot pattern .(m + n) in w's place. The former is not obvious. How should we unify n + m with m + n? n ↦ m would be wrong: note, for example, that 2 + 3 ≡ 3 + 2, but 2 does not unify with 3.

In general, things are made difficult by the fact that Agda can't show that _+_ is injective. This is for the good reason that it isn't (as our example showed). Agda can show that constructors are injective, justified by the fact that Agda has no quotient types or the like. This is why suc m and suc n will unify. Agda does not try to show that any defined functions are injective, though it in principle could (by getting the user to supply a proof, for example).

  • $\begingroup$ Thank you! So in Agda, the contextual information (say, which terms are equivalent) doesn't hold across functions. Is that correct? $\endgroup$
    – ice1000
    Oct 13 '18 at 20:18
  • $\begingroup$ I'm not sure what you mean. Can you give an example? $\endgroup$
    – mudri
    Oct 13 '18 at 21:21
  • $\begingroup$ Like, if a parameter of type $a \equiv b$ is matched as $refl$, $a$ and $b$ will be treated as equivalent in the context. We have to bring this information out of the generated helper function (by introducing an explicit argument whose value is trivially $a$) so that we can make use of it in the proofs. $\endgroup$
    – ice1000
    Oct 13 '18 at 23:48
  • 1
    $\begingroup$ From the outside, we only learn about the behaviour of wa''-aux when the proof we pass to it is judgmentally refl, matching the definition clause. comm n m is not judgmentally refl – it is an inductive argument. Whenever we do pass in refl, we've already done the same unification on the outside as has been done on the inside, so generally, this unification information doesn't leak. $\endgroup$
    – mudri
    Oct 14 '18 at 0:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.