Another tweak to cong!

[uncle-betty]

Hello there.

I do a lot of equational reasoning with _/_ and _%_. This means NonZero instance arguments on both sides of my equalities. Sometimes, when cong! runs, the metas for the instance arguments are already resolved. But sometimes they aren't. Or one of them is, but the other isn't. It depends on how things fall into place during type-checking.

When there are such unresolved metas, cong! fails. For example, even an identical instance argument gets a different meta on the LHS vs. the RHS. So, anti-unification considers them a difference and places a phi. Same for an unresolved meta on one side and a resolved meta on the other.

The solution that I would like to propose is to wait for the meta variables to be resolved, before doing anti-unification. However, checking the goal for the existence of metas comes with a cost: the goal needs to be traversed, which impacts cong! performance.

This proposal thus only checks for metas once unification failed. The idea is to avoid burdening other people with the meta check, who might not use _/_ and _%_ as much as I do, and who thus might not have this problem.

In addition to the meta check, this proposal tries to make the error message issued by a failing cong! more meaningful to the user. cong! now tells them which term it tried, so that the user can troubleshoot the situation. Consider the following:

lemma : ∀ m n o → m + n + o ≡ n + m + o
lemma m n o = begin-equality
  m + n + o ≡⟨ cong! (+-comm m n) ⟩
  n + m + o ∎
  where open ≤-Reasoning

This now yields the following error:

cong! failed, tried:
cong (λ ϕ → ϕ + ϕ + o) (+-comm m n)

Previously the error was the following, which I've always found confusing:

m != m + n of type ℕ

[uncle-betty]

Thank you for your reviews!

I think I might need some guidance regarding the blockOnMetas (see my response to the comment), but I made the other changes.

The idea behind the test₂ unit test, which may not be completely obvious:

• Anecdotally, I seem to have encountered issues mostly with reasoning chains that were a little longer. Hence the redundant steps.
• It tests explicitly given instances in addition to instances from instance arguments.

[uncle-betty]

Thanks for taking another look. I made the changes.

[jamesmckinna]

Coming to this PR quite late... ... if you find yourself doing a lot of equational reasoning with _/_ and _%_ then is there a higher level (as opposed to low-level cong reasoning) collection of DivMod abstractions which might streamline your work?

[uncle-betty]

Excellent question. I don't know yet. I've only started toying around.

I'm curious about modeling machine integers in Agda: convert integers modulo 2^64 to Vec Bool 64 and vice versa, prove that division by 2 of an integer corresponds to a right shift of the corresponding bit vector - this kind of thing.

Yes, there may be a much better way than what I'm currently doing. But I still think that there's benefit in making cong! deal properly with meta variables in goals.

[jamesmckinna]

@uncle-betty you wrote:

I'm curious about modeling machine integers in Agda: convert integers modulo 2^64 to Vec Bool 64 and vice versa, prove that division by 2 of an integer corresponds to a right shift of the corresponding bit vector - this kind of thing.

Makes good sense, but then I would (be tempted to) avoid _/_ and _%_ in favour of using the Data.Nat.Base.⌊_/2⌋ and Data.Nat.Base.⌈_/2⌉ functions and their properties, and perhaps consider iterates of them for m-ary shifts? If you're only considering base-2^n arithmetic, I think full 'div-mod' is overkill?

Yes, there may be a much better way than what I'm currently doing. But I still think that there's benefit in making cong! deal properly with meta variables in goals.

Absolutely fair point.

[uncle-betty]

Oh, nice! Thanks, @jamesmckinna, for pointing me to these functions. I appreciate the guidance.

[MatthewDaggitt]

Apologies for the delay. Merging in now. Thanks for another great PR!

[uncle-betty]

Oh, that's exciting! Great! Thank you for the merge and for your assistance.