A tweak for the cong! tactic

[uncle-betty]

Hello there.

It's known that the cong! tactic's anti-unification is a tad too granular for some use cases. In the following, for example, it descends past the application of _+_ in b + c and c + b, so that the following definition doesn't type-check.

proof : ∀ a b c → a + (b + c) ≡ a + (c + b)
proof a b c =
  a + (b + c) ≡⟨ cong! (+-comm b c) ⟩
  a + (c + b) ∎

Note, however, that the following does type-check. (Note the added application of id to b + c.)

proof : ∀ a b c → a + (b + c) ≡ a + (c + b)
proof a b c =
  a + id (b + c) ≡⟨ cong! (+-comm b c) ⟩
  a + (c + b)    ∎

It works, because the cong! tactic inhibits normalisation, the application of id isn't reduced, anti-unification finds that id (b + c) is different from (c + b) (because id is different from _+_) - and doesn't descend further.

Unfortunately, this hack falls apart, when using cong! multiple times in a row. The following, for example, doesn't type-check.

proof : ∀ a b c d → a + b + (c + d) ≡ b + a + (d + c)
proof a b c d =
  a + b + id (c + d)   ≡⟨ cong! (+-comm c d) ⟩
  id (a + b) + (d + c) ≡⟨ cong! (+-comm a b) ⟩
  b + a + (d + c)      ∎

I think that this can be worked around, however, by slightly tweaking the cong! tactic to replace any id x on the right-hand side of the equality with x, i.e., by manually reducing id x to x on the RHS.

The modifications contemplated in this pull request do two things:

• They add ⌞_⌟ as an alias for id. (Name choice inspired by #1136.)
• They tweak the anti-unification algorithm to skip past any application of ⌞_⌟ on the right-hand side of the equality.

As a result, the following example type-checks:

module Demo where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Tactic.Cong

proof : ∀ a b c d → a + b + (c + d) ≡ b + a + (d + c)
proof a b c d =
  a + b + ⌞ c + d ⌟   ≡⟨ cong! (+-comm c d) ⟩
  ⌞ a + b ⌟ + (d + c) ≡⟨ cong! (+-comm a b) ⟩
  b + a + (d + c)     ∎
  where open ≡-Reasoning

proof′ : ∀ a b → a + b + (a + b) ≡ b + a + (b + a)
proof′ a b =
  ⌞ a + b ⌟ + ⌞ a + b ⌟   ≡⟨ cong! (+-comm a b) ⟩
  b + a + (b + a)         ∎
  where open ≡-Reasoning

This could be a useful tweak to the cong! tactic, no? Or am I missing something?

[uncle-betty]

Great! Thank you for the review.

I've started to make the requested additions, but now I also have second thoughts: The whole idea breaks, when using ≡˘⟨ ? ⟩. sym swaps the RHS and the LHS, and as the underlying idea is to have special treatment for the RHS, things break.

I'll have to spend more thought on this over the next days.

[shhyou]

This idea seems relevant to the approach in https://github.com/gallais/potpourri/blob/b0b734fb8e768f280bc36519048b977b994d1a5e/agda/cong/Syntax/Focus.agda#L154 which is suggested in #2033.

[uncle-betty]

Thank you, @shhyou, for the pointer! I'll check out #2033.

[uncle-betty]

Alright - catchTC to the rescue! I think that fixed the issue with ≡˘⟨ ? ⟩.

The idea is to use catchTC to detect when anti-unification doesn't yield a correct solution. And then try again, with the RHS and LHS swapped. This incurs additional cost, but only when the first attempt at anti-unification fails. So, there's only a performance penalty in the following two cases:

• The proof is a work in progress and not yet complete/correct. Now it takes a little longer for type-checking to fail, because there are two attempts at anti-unification.
• The proof contains ⌞_⌟ and uses ≡˘⟨ ? ⟩. The first anti-unification attempt always fails, resulting in a second attempt.

Complete/correct proofs that don't contain ⌞_⌟ won't be affected at all.

(I double-checked that let is lazy by adding debug log messages to uni and uni'.)

I'm not sure whether this is good enough for inclusion in the standard library. I guess one could try to find a smarter way to address cong! failures. What I like about this approach, though, is that it's basically a 10-line add-on to existing proven technology. Maybe collect some more feedback from people? I'll go over to #2033 and ask.

[uncle-betty]

Out of curiosity, a quick performance smoke test with --profile=definitions.

README.Tactic.Cong on the master branch:

README.Tactic.Cong.succinct-example                   31ms 
README.Tactic.Cong.EquationalReasoningTests.test₁     30ms 
README.Tactic.Cong.EquationalReasoningTests.test₂     26ms 
README.Tactic.Cong.verbose-example                    24ms 
README.Tactic.Cong.LambdaTests.test₂                  14ms 
README.Tactic.Cong.HigherOrderTests.test₂             12ms 

On the cong-tweak branch:

README.Tactic.Cong.succinct-example                   29ms 
README.Tactic.Cong.EquationalReasoningTests.test₁     36ms                                                                                                                                        
README.Tactic.Cong.EquationalReasoningTests.test₂     25ms 
README.Tactic.Cong.verbose-example                    21ms 
README.Tactic.Cong.LambdaTests.test₂                  10ms 
README.Tactic.Cong.HigherOrderTests.test₂             12ms 
README.Tactic.Cong.marker-example₁                    25ms 
README.Tactic.Cong.marker-example₂                    13ms 

As expected, pretty much the same, within the margin of error, no? Sometimes cong-tweak is faster, sometimes master is. (I don't know why not all top-level definitions show up.)

When I change the two marker-example proofs (which contain ⌞_⌟) to use ≡˘⟨ ? ⟩ instead of ≡⟨ ? ⟩, then they take longer to type-check, as expected. So, the second anti-unification and other extra work does show.

README.Tactic.Cong.marker-example₁                    45ms 
README.Tactic.Cong.marker-example₂                    17ms 

Note that succinct-example also uses a ≡˘⟨ ? ⟩ and doesn't see a slow-down, because it does not contain ⌞_⌟.

So, I'm now cautiously optimistic that the thoughts about performance in my previous comment are reasonable.

[uncle-betty]

Hmmmm. Maybe I'm overthinking the performance angle.

As a comparison, I just ran #2033 on marker-example₁. (It doesn't seem to support multiple markers per proof step, as in marker-example₂.)

Demo.marker-example₁     94ms 

Repeating the original results from above for context. Tweaked cong! with ≡⟨ ? ⟩:

README.Tactic.Cong.marker-example₁                    25ms

Tweaked cong! with ≡˘⟨ ? ⟩:

README.Tactic.Cong.marker-example₁                    45ms

So, even with the overhead of the second anti-unification in ≡˘⟨ ? ⟩, the tweaked cong! seems faster in this specific case.

I'm starting to feel a little more bullish about this tweak.

Sorry about all the comments. I'm just trying to be transparent about my reasoning so that others can chime in, if interested.

[gallais]

Rather than guessing using catchTC, wouldn't it be easier to provide combinators that include the call to the cong! tactic?

E.g.

_≡⟨_⟩_ -- forwards step
_≡⟪_⟫_ -- forwards step with magic cong

_≡⟨_⟨_ -- backwards step
_≡⟪_⟪_ -- backwards step with magic cong

? Never start by forgetting the user's stated intent only to then attempt to guess it via computations...

[uncle-betty]

Oooooh! Cool! I like the idea of having combinators that include the cong!.

Earlier, I tried to come up with something in this vein, but couldn't. I tried to find a way to make cong! figure out somehow, whether it's being used in ≡˘⟨ ? ⟩ vs. ≡⟨ ? ⟩. Which seems impossible.

This proposal would solve that problem elegantly.

Does anyone have any opinions on the user ergonomics of the proposed approach?

[uncle-betty]

I've been thinking about the combinator proposal a little more. Let me make sure that I have this right by breaking it down a little. I think I might need some adult supervision here.

The combinators would be syntax declarations, say:

syntax cong!-≡-⟫ x y≡z x'≡y' = x ≡⟪ x'≡y' ⟫ y≡z
syntax cong!-≡-⟪ x y≡z y'≡x' = x ≡⟪ y'≡x' ⟪ y≡z

The overall proof of x ≡ z would be trans (cong ... x'≡y') y≡z, where ... is the part the tactic has to figure out. cong ... x'≡y' would have type x ≡ y.

The two macros used by the syntax declarations would look like this:

cong!-≡-⟫ : ∀ {a} {A : Set a} (x : A) {x' y' y z : A} → y ≡ z → x' ≡ y' → Term → TC ⊤
cong!-≡-⟫ x y≡z x'≡y' hole = ...

cong!-≡-⟪ : ∀ {a} {A : Set a} (x : A) {x' y' y z : A} → y ≡ z → y' ≡ x' → Term → TC ⊤
cong!-≡-⟪ x y≡z y'≡x' hole = ...

• hole would be the overall goal, x ≡ z. I somehow have to get from there to x ≡ y, because that's what I want to run anti-unification on.
• How would I do that? I guess I would create a new meta variable and construct a term trans <meta> y≡z. I would then unify this constructed term with hole. The meta variable would then have type x ≡ y, which would be my new goal.
• From this point on, it's all basically like the existing cong!: I would run anti-unification on this new goal. Then I would unify the resulting cong ... x'≡y' term with my new meta variable (as opposed to the overall goal, as cong! currently does).

Does this make sense at all? Maybe it would be nice to pull the trans out of the macros, in order to simplify them - but I don't see how this can be done.

[uncle-betty]

OMG! It works! It works, it works, it WORKS! I guess, to a certain extent, one can compensate a lack of experience with enthusiasm and tenacity. :)

I haven't yet changed the documentation. Let's first decide whether these custom combinators are what we really want. And whether my proposed implementation makes sense. If not, I'll roll back the changes. Otherwise, I'll fix the documentation and examples.

[MatthewDaggitt]

This does look very exciting! I guess my main question is do these combinators work with any reasoning module (e.g. preorder, partial order reasoning) as well? It looks like they should, but it would be good to get confirmation!

Minor bikeshedding, but I think it would be good if we could include the tactic symbol ! in the combinator names. Maybe _≡⟨!_⟩_?

[uncle-betty]

Oh, excellent question! I'm glad you asked, because it turns out that the combinators don't work with anything else right now.

Turns out that the ≡-syntax module, for example, is parameterized by the relation and the trans that goes with it. And that the relation isn't necessarily _≡_, but would more typically be _IsRelatedTo_, which differs between the stdlib's different reasoning modules.

Shame. Now a user cannot simply generically import the combinators from Tactic.Cong and use them with any reasoning module, can they?

Instead, we'd have to parameterize the new combinators as well. Then, say, ≤-Reasoning for Data.Nat would have to import the combinators from Tactic.Cong with the parameters filled in appropriately, and re-export the now specialized combinators.

Or is there a better way?

Have a good weekend, everyone.

P. S. Happy to change the name of the combinators. I don't have a preference.

[uncle-betty]

I started sketching the idea of having, say, Relation.Binary.Reasoning.Base.Triple import Tactic.Cong and re-export explicitly parameterized versions of the combinators.

Unfortunately, this causes an import cycle: Tactic.Cong imports Reflection, which imports Data.Nat.Properties, which (via Relation.Binary.Reasoning.Base.Triple) imports Tactic.Cong.

I'll try to understand the dependencies a little better, but I'm a little hesitant to change the structure of stdlib just to suit a relatively small additional feature. But maybe there's another way.

I also double-checked my assumption that the combinators have to be explicitly parameterized. What, if they could take the relation as an implicit parameter instead and figure out the relation (e.g., _≡_ or _IsRelatedTo_) themselves? As I had assumed, this doesn't work. In applications of the following test function, for example, Agda cannot figure out B.

test : ∀ {a b} {A : Set a} {B : REL A A b} {x y : A} → B x y → REL A A b 
test {B = B} Bxy = B

_ = test {B = _≡_} {x = 1} refl -- B  must be explicitly specified

I'll spend some more thought on this. I'd definitely prefer the combinator approach over my original catchTC hack.

[JacquesCarette]

For efficiency of checking and for having minimal dependencies, I doubt we'll ever want to use tactics in the "low level" parts of the library. So I wouldn't spend much time on this.

Using tactics is great for users, and for exploratory development, but some parts of the library will always use explicit proofs.

[uncle-betty]

Thank you for looking into this!

Unfortunately, the cyclic dependencies are a more general issue, as far as I can tell. Suppose that I'd like to use ≤-Reasoning from Data.Nat.Properties in a higher-level proof outside of stdlib.

• Then Data.Nat.Properties would presumably have to import Tactic.Cong, which provides the new cong! combinators to ≤-Reasoning.
• However, conversely, Tactic.Cong imports stdlib's reflection machinery, which imports Data.Nat.Properties.

It looks like this generally precludes combinators from using reflection.

Here's how I ended up where I am:

≡-Reasoning from Relation.Binary.PropositionalEquality is based on Trans _≡_ _≡_ _≡_. That's what the cong! combinators on the cong-tweak branch work with right now. That's solved.

However, other reasoning modules are based on Trans _≡_ R R. (I.e., the current proof step uses _≡_, the rest of the proof down to the _∎ uses R.) So, I'm now trying to generalize the combinators to work with any R.

My first idea was to make R an implicit argument to the cong! combinators. But Agda seems unable to automatically derive this argument in applications of the combinators. (As the test function from my previous comment illustrates.)

That's why the idea I'm currently pursuing is to explicitly parameterize the cong! combinators by way of an explicit relation parameter to the cong! combinators module. (This also seems to be the general pattern followed by stdlib.) Data.Nat.Properties would then import the cong! combinators module providing _IsRelatedTo_ (which is the R for ≤-Reasoning) as the explicit relation parameter.

Currently, I see two ways out:

• The reflection machinery in stdlib imports Data.Nat.Properties solely for _≟_, as a foundation for its own decidable equality on ASTs. So, effectively, it only imports a dozen or so lines of code. Could that simply be duplicated in the reflection machinery? Or factored out into some other place under Data.Nat?

• Abandon the idea of custom combinators and go back to the catchTC construct. (Which I'm not too thrilled about.)

Or am I missing something?

[JacquesCarette]

I've been of the opinion for quite some time that things like _≟_ should be in their own modules -- explicitly because of dependency issues. Data.Nat.Properties pulls in a lot of stuff, legitimately, but one often needs some particular relations, like _≟_ without all that baggage. It was deemed too big a breaking change, even for stdlib-2.0. Sigh.

[uncle-betty]

Oh, well! Luckily I just found other cycles, so now it's not just Data.Nat.Properties that causes me trouble! :)

≡-Reasoning from Relation.Binary.PropositionalEquality would also have to import Tactic.Cong for its combinators, which causes additional cycles via the reflection subsystem.

At this point, I think that combinators and reflection just don't mix well.

But let me take a step back. Maybe I took a wrong turn at an earlier point that led me into this dead-end.

The reason why my combinators use macros and reflection is so that there isn't any need to flip the goal for the macro when doing a backwards step. The cong! macro application is integrated into the combinator, so that the combinator for a backwards step can do, say, cong! (sym (+-comm m n)) instead of what the existing combinators do, sym (cong! (+-comm m n)).

Unfortunately, the hack that my proposal builds upon depends on the goal not getting flipped. Hence the need for custom combinators that avoid the need to flip the goal in a backwards step.

I'll keep pondering this over the next few days. At this point, the only viable solution seems to be catchTC, which seems super hacky.

[uncle-betty]

Alright. Progress!

The combinators now support all reasoning modules that are based on Relation.Binary.Reasoning.Base.Single, [...].Double, and [...].Triple, in addition to ≡-Reasoning from Relation.Binary.PropositionalEquality.

I also renamed the combinators to ≡⟨! ... ⟩ and ≡⟨! ... ⟨.

The updated code is considerably more complex and brittle, though, than the older version that was based on catchTC and that didn't have the custom combinators. I hope that we aren't setting ourselves up for a maintenance nightmare.

The main insight is that I can figure out the relation to be used via reflection:

• As I said earlier, Agda cannot figure out the R in {R : Rel A r} {y z : A} (yRz : R y z) based on the given yRz.
• So, let's instead do this: {R : Set r} (yRz : R). And then use reflection to figure out what R is, by getting the type of yRz and looking at its name.
• Once we have the name of R, we can map it to the corresponding step function. So, Cong.agda now contains a hard-coded list of which relation goes with which step function.
• Previously, I was trying to pass the relation and step function from the individual ...-Reasoning modules into Tactic.Cong. Which caused the cycles. Now this knowledge is hard-coded in Tactic.Cong. Of course this means, that Tactic.Cong may need to be changed if any of the ...-Reasoning modules changes.
• Modules like Relation.Binary.Reasoning.Base.Triple have a lot of parameters. So, how do I construct the complete parameter list for the step functions? I make the following assumptions.
  • The relation and the step function live in the same module.
  • When I strip the last two arguments off the relation's n arguments (e.g., the x and y off x ≡ y) and apply the step function to the remaning (n - 2) arguments, then the remaining arguments to the step function are {x} {y} {z} x≡y yRz.
  • Example: Suppose that the relation is _≡_ {0ℓ} {ℕ} x y. Stripping off x and y yields the argument list {0ℓ} {ℕ}. Thus the step function that goes with _≡_, trans, is expected to take arguments {0ℓ} {ℕ} {x} {y} {z} x≡y yRz.
• Again, this might turn out to be brittle. Should the relationship between a relation's arguments and its step function's arguments ever change, Tactic.Cong will have to be changed.

I'm not quite sure what to make of all of this. The solution still feels a little hackish, because Tactic.Cong now:

• Contains knowledge about other parts of stdlib, namely the mapping of relations to step functions.
• Makes assumptions about how the parameters of relations and step functions relate.
• Has gained quite a bit of complexity.

Maybe the quoteTC-based solution now doesn't look that bad, after all?

[uncle-betty]

After a good night's sleep: Maybe I'm overthinking this. The modules on whose implementation details Tactic.Cong now depends don't seem to see that much change. So, maybe this won't turn into a maintenance nightmare.

On the other hand, I just checked - and, oh boy! The performance is now considerably lower:

README.Tactic.Cong.marker-example₁                    64ms 
README.Tactic.Cong.marker-example₂                    84ms 

Previously: 25 ms and 13 ms, respectively. So the combinators take ~3x and ~6x as much time as the quoteTC solution in this benchmark.

Which makes sense. The combinator approach delegates more responsibility from Agda's built-in type-checking to the macro. The combinators operate "on a larger hole" than cong!.

So, I'm a little torn. If the difference weren't that massive, I'd say: Sure, let's opt for the more principled approach via the combinators. But given that the performance difference is substantial, I'm not so sure any longer.

[uncle-betty]

Alright. Another day, another suggestion. But this one's really cool, I think. I think that it marries the simplicity and robustness of the quoteTC approach to the combinator approach.

Idea: Instead of having cong!-specific combinators, have generic tactic combinators. Say, _≡⟪_⟫_ and _≡⟪_⟪_. They would differ from the existing forward and backward combinators in that they enrich a goal. So, a tactic used with these tactic combinators would operate on an enriched goal. The enrichment would communicate additional context to the tactic. For now, it would just be the direction of the combinator, forward or backward.

Let me sketch some code:

  data Direction : Set where
    forward : Direction
    backward : Direction

  data Goal {a : Level} (d : Direction) (A : Set a) : Set (sucℓ a) where
    proof : A → Goal d A

  makeGoal : ∀ {a} {A : Set a} (d : Direction) → Goal d A → A
  makeGoal _ (proof p) = p

  test : ∀ m n o p → m + n + (o + p) ≡ n + m + (p + o)
  test m n o p = begin
    ⌞ m + n ⌟ + (o + p) ≡⟨ makeGoal forward  (proof (cong (λ ϕ → ϕ + (o + p)) (+-comm m n))) ⟩
    n + m + ⌞ o + p ⌟   ≡⟨ makeGoal backward (proof (cong (λ ϕ → n + m + ϕ)   (+-comm p o))) ⟨
    n + m + (p + o)     ∎

The idea is to have a tactic operate on, say, Goal forward (⌞ m + n ⌟ + (o + p) ≡ n + m + ⌞ o + p ⌟) instead of just ⌞ m + n ⌟ + (o + p) ≡ n + m + ⌞ o + p ⌟. To this end, the forward combinator would apply makeGoal forward to the tactic's result. The backward combinator would apply makeGoal backward. So, the two tactic combinators would automate what I manually did above. The tactic would be responsible for providing the (proof ...) part.

From the enriched goal, the tactic would know which direction we're going and could act accordingly, if it is direction-sensitive.

In order to support the tactic combinators, existing tactics would have to:

• Become able to break down an enriched goal.
• Wrap their generated proof in proof.

Sorry about the back and forth. I thought that this pull request was in pretty good shape, but then I got nerd-sniped with the idea of having new combinators.

But I think that we might finally have gone from primitive, via complicated, to simple. (Story of my life.)

How does such a more generic tactic combinator framework sound? If this is a non-starter, then I'd suggest that we go back to the catchTC approach.

[uncle-betty]

After playing around a little more, here's what I think: For the purpose of this pull request, let's leave it at the original tweak based on catchTC. If that doesn't clear the bar for stdlib, then that's perfectly fine. Then let's close this pull request.

To recap: The disadvantage of this approach is that when ⌞_⌟ is used with cong! in a backward step, then anti-unification is done twice, which results in lower performance of cong!. Other cases are not affected, e.g., using cong! without ⌞_⌟, or using cong! with ⌞_⌟ in a forward step.

My reasoning:

• It's just a few dozen lines. Easy to undo, should we come up with a more principled approach. And while not perfect, I think that it provides pretty good value.
• Custom combinators for cong! are trickier than I thought. I either ended up with import cycles, or I had to build the combinators on implementation details of other parts of stdlib, which was brittle and slow.
• I still like the idea of generic tactic combinators and the idea of enriched goals. But that would change how tactics work in stdlib. That's quite a bit of an overhaul. If at all, then this should be done in a larger context, it should consider the needs of other existing and possible future tactics, and it should consider the use of tactics without combinators. It shouldn't be done in this pull request.

[uncle-betty]

Great! Thank you for the review. I made the changes. I'm excited that this is making it into stdlib!

[MatthewDaggitt]

I'm excited that this is making it into stdlib!

Haha, I'm glad! We'd of course welcome any further similarly high-quality contributions you might be interested in making. :+1: I've hit merge, so it should be in in the next couple of hours.

[uncle-betty]

Thank you for the encouragement!

(It looks like there still is an open change request, which prevents merging.)

[MatthewDaggitt]

Whoops, approved.