agda
Reasoning Combinators for Congruence?
In a reasoning like the following:
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
structure type3 ≈⟨ congruence_for_structure equiv3 ⟩
structure type4 ≈⟨ congruence_for_structure equiv4 ⟩
structure type5 ≈⟨ congruence_for_structure equiv5 ⟩
structure type6 ≈⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
i.e., a reasoning with multiple consecutive steps using a congruence, it is tedious to repeat the congruence. This is especially more burdensome if the congruence is fairly long. One can try to resolve this using a nested reasoning like
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
structure type3 ≈⟨ congruence_for_structure
(begin type3 ≈⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩
type6 ∎) ⟩
structure type6 ≈⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
However, note that we need to repeat type3 and type6 twice. If they are also long/complex, this option does not help much either. It would be nice if there is some combinators with-cong⟨_⟩_ and _after-cong⟨_⟩_ (there would be better names, but for sake of giving the next example) that allows us to write the following:
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
with-cong⟨ congruence_for_structure ⟩
type3 ≈⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩
type6
after-cong⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
or depending on the relation, even better:
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
with-cong⟨ structure ⟩
type3 ≈⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩
type6
after-cong⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
Should after-cong⟨ equiv ⟩ be a distinct step,... or a continuation as part of your hypothetical with-cong⟨_⟩ notation? Ie. something like
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
with-cong⟨ congruence_for_structure ⟩then⟨ equiv6 ⟩
type3 ≈⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩
type6
type7 ≈⟨ equiv7 ⟩
type8 ∎
@jamesmckinna Thanks for the suggestion. I proposed _after-cong⟨_⟩_ as a separate step so that the order of equivalences stays the same. However, if this approach seems too verbose, what you suggested seems a good approach as well.
So as the author of much of the current reasoning-based code, this is going to be quite complicated to implement and I think there are better ways to do it.
Firstly, have you seen the cong! tactic? I feel that if its only a few lines then cong! should suffice.
If the sub-reasoning has many lines then you really should be splitting out the sub-equality into a where block or even a different proof.
Thanks @MatthewDaggitt ! Good to have the balance between expertise and enthusiasm when it comes to suggestions for new functionality.
@MatthewDaggitt Thank you for the valuable comment! That tactic seems indeed very useful. However, I want to argue that the reasoning step I suggest is still useful separately. The tactic supports only equalities, not other equivalences, so we still have the problem in general case.
Yes, that is a fair point. However, I think it's still clearer and more modular to split reasonable to split these subequalities out into a where block. Is there a problem with that approach?
That approach shares the issue in the second approach of the original post, i.e. one needs to duplicate the initial and final types. If they are fairly complex, extracting a sub reasoning into a separate definition does not save much time/(textual) proof size.
Hmmm, thinking about this a bit more: if type3 and type6 are duplicated and/or sufficiently complicated (whatever that may mean in any context), then I'd be tempted to abstract those out as named subterms in a where block as well... in support of @MatthewDaggitt 's thesis...
Sure, that works. It is just more cumbersome in my opinion. I think the question is really how difficult to implement a combinator like this.
Okay so:
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
with-cong⟨ congruence_for_structure ⟩
type3 ≈⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩
type6
after-cong⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
vs
begin
type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
structure type3 ≈⟨ cong structure equiv ⟩
structure type6 ≈⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
where
equiv = begin
type3 ≈⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩
type6 ∎
I agree that your syntax is a little bit shorter, but however it does break the crucial point of the reasoning combinators, namely that they make all the intermediate types available at each step of the reasoning. Currently even though the intermediate types structure type3 and structure type6 are crucial to the proof, in your syntax they don't explicitly appear anywhere? In fact structure doesn't appear anywhere...
I feel this is a downgrade in readability of the proof no?
Hm, that's a fair point. However, I think that can be adjusted in the combinator, e.g. so that it explicitly mentioned structure type3 before the combinator and skipping type3 or just to mention structure before.
How about the following syntax?
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
structure type3 under⟨ cong structure ⟩≈⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩then
structure type6 ≈⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
- Advantage: keeping the structure at the beginning and the end so that each step is clearly shown
- Disadvantage: the beginning type of equiv3 and the ending type of equiv5 are less clear
Minor: I personally prefer to put the begin on the line above, to use less horizontal space. But that's pure style.
As to the syntax, an alternate suggestion would be
begin type1 ≈⟨ equiv1 ⟩
type2 ≈⟨ equiv2 ⟩
structure type3 ≈cong[ structure ]⟨ equiv3 ⟩
type4 ≈⟨ equiv4 ⟩
type5 ≈⟨ equiv5 ⟩∎
structure type6 ≈⟨ equiv6 ⟩
type7 ≈⟨ equiv7 ⟩
type8 ∎
