Rewriting Tactic

[TOTBWF]

Patch Description

This PR adds a new tacticrw, which is a simple equality rewriting tactic, intended to be used in equational reasoning blocks.

Motivation

When performing large equational reasoning proofs, it's extremely common to find yourself constructing sophisticated lambdas to pass into cong. This is extremely tedious, and can bog down large proofs in piles of verbose boilerplate. Normally one would use rewrite to avoid having to write out these complicated cong expressions, but this can obscure the proof, and is often impossible (IE: when using Relation.Binary.Reasoning.Preorder).

Implementation

We solve this problem by introducing a new tactic, rw, that gives us a similar level succinctness as rewrite, but without it's restrictions. It operates by inferring the type of the goal, anti-unifying both ends of the equality, and then using that to construct the lambda argument to cong. This allows us to drastically reduce boilerplate; for instance

example : ∀ (m n : ℕ) → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
example m n eq = begin
    suc (suc (m + 0)) + m
  ≡⟨ cong (λ ϕ → suc (suc (ϕ + m))) (+-identityʳ m) ⟩
    suc (suc m) + m
  ≡⟨ cong (λ ϕ → suc (suc (ϕ + ϕ))) eq ⟩
    suc (suc n) + n
  ≡˘⟨ cong (λ ϕ → suc (suc (n + ϕ))) (+-identityʳ n) ⟩
    suc (suc n) + (n + 0)
  ∎

becomes

example : ∀ (m n : ℕ) → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
example m n eq = begin
    suc (suc (m + 0)) + m
  ≡⟨ rw (+-identityʳ m) ⟩
    suc (suc m) + m
  ≡⟨ rw eq ⟩
    suc (suc n) + n
  ≡˘⟨ rw (+-identityʳ n) ⟩
    suc (suc n) + (n + 0)
  ∎

This also plays nicely with C-c C-m, which allows for the quick generation of boilerplate for those who are hesitant of having tactics in the final source.

Notes

When the rw tactic is used in a hole, it doesn't report it's type properly when C-c C-. is used, and instead reports a metavariable. C-c C-r works fine though, so it's a minor quirk at worst.

[MatthewDaggitt]

This looks awesome, thank you so much @TOTBWF! Added some comments.

I would be interested to see how it stacks up against #1158 which appears to be a bit dead in the water. In theory your solution is much nicer as it doesn't require you to manually point out where to apply cong. It would be great if you could try it out on the test cases in #1158 (comment). Not all of them are relevant though, as they assume the tactic automatically applies sym as well.

So the big thing that is missing is a README file, under README.Tactic.Rewrite explaining how to use it. It also doubles as a test file, to prevent regressions. You could add the test cases there?

[MatthewDaggitt]

Also I'm wondering slightly about the name, rw isn't terrible meaningful. In the past when we have a name that clashes with a builtin keyword, we usually surround it with angle brackets, e.g. ⟨rewrite⟩. Welcome to alternative suggestions as well!

[JacquesCarette]

The level of commenting in this code is exemplary. I need to up my own game to match this!

[gallais]

Welcome to alternative suggestions as well!

Given that it's applying cong, I'd suggest a cong-based name. Perhaps cong- as we are already using -
to denote an argument that is not passed explicitly in e.g. -,_

That being said the missing argument in -,_ is filled by unification (- is a textual representation of _) so
we could maybe use a different character to signal that it's a tactics. cong! maybe?

[MatthewDaggitt]

I like cong!

[TOTBWF]

Working through some of the test cases, I've stumbled across some really weird behaviour:
Consider this test case:

lit-test₁ : 40 + 2 ≡ 42
lit-test₁ = cong! refl

This produces unsolved metas: refl can't determine any of the implicits. This is odd though, as if we expand our the macro using C-u C-c C-m, there are no unsolved metas in sight.

lit-test₁ : 40 + 2 ≡ 42
lit-test₁ = cong (λ ϕ → ϕ) refl

It appears that Agda is checking the types of the arguments before quoting them and passing them into the macro. This can be confirmed by adding a dummy argument to refl, like so:

lit-test₁ : 40 + 2 ≡ 42
lit-test₁ = cong! (refl {x = "uh-oh"})

Trying this out with the quoteTerm primitive, we can see the same behaviour: the term to be quoted is checked, then quoted. To me, this seems pretty bizarre: macros will often provide enough context to make these unsolved metas disappear. Maybe there's some trick I'm missing that allows us to suppress these unsolved metas, but after a bit of experimentation I wasn't able to find one.

EDIT: Of course immediately after posting this I figured it out. The trick is to not quote the equality proof in question.

[jespercockx]

EDIT: Of course immediately after posting this I figured it out. The trick is to not quote the equality proof in question.

You mean you intend to change the type of cong! from Term → Term → TC ⊤ to x ≡ y → Term → TC ⊤? Because that's what I would've suggested. Not quoting things unless it's really needed is a good principle to follow when implementing (Agda) macros.

[TOTBWF]

So naive anti-unification is a bit too naive in a couple of cases. For instance, consider rewriting with +-comm: all subexpressions of the form n + m will get turned into ? + ?. The original cong! tactic still seems useful because of its relative simplicity, but it probably makes sense to add a more sophisticated version that does some sort of subexpression search.

[isovector]

This tactic is clearly very valuable as it stands, and I think it would be a shame to let perfection be the enemy of the good here. I'm exceptionally excited to start using it in my proofs.

[MatthewDaggitt]

Agreed! @TOTBWF if you add the README and the CHANGELOG entries I'll merge it in and then afterwards we can work on improving it if people are still keen.

[TOTBWF]

Cool! I've added the README file and fixed some minor issues. I'll stew a bit over what the best strategy for a more advanced version would be; I have some rough ideas, but nothing too concrete yet.

[JacquesCarette]

Meant to comment on this earlier. Of course I agree with others that it is already valuable as it stands. What I would like to see is a bit of documentation about its limitations -- roughly so that people don't continually report known limitations and/or try to use it for what it is known not to work on.

I'm unsurprised that just anti-unification has limits. There's a reason things like AC and ACI-unification exist as separate items from just unification. You probably want to do a sort of anti-unification-modulo-theory. [No, this doesn't exist yet. I'm just giving it an obvious name.]

[TOTBWF]

There's a short blurb in the README file that describes the situations it is likely to fail in, but ideally someone can come up with a smarter algorithm :)