3
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

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).

Improve this answer
$\endgroup$
4
  • $\begingroup$ Thank you! So in Agda, the contextual information (say, which terms are equivalent) doesn't hold across functions. Is that correct? $\endgroup$ Commented Oct 13, 2018 at 20:18
  • $\begingroup$ I'm not sure what you mean. Can you give an example? $\endgroup$ Commented Oct 13, 2018 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$ Commented Oct 13, 2018 at 23:48
  • 2
    $\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$ Commented Oct 14, 2018 at 0:03

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.