Potential for a cong helper macro in Tactic module

[dylanede]

agda-holes is a library that makes working with cong more convenient and succinct. This issue is for discussing the possibility of adding some similar functionality inside the Tactic module alongside the ring and monoid solvers.

agda-holes is not usable as-is. It has bit-rotted from the current stable Agda, and it also relies on uses of the TERMINATING pragma, which would presumably need to be removed and the corresponding functions refactored. It would also need to be made properly agnostic over cong implementations (e.g. from cubical Agda). I might be interested in undertaking the work to make it suitable for inclusion when I get some time, so I'm interested in whether this sounds like a good idea.

[gallais]

This would be a very nice addition. :)

[dylanede]

agda-holes auto-applies sym if necessary. I'm not sold on that idea myself as I prefer explicit yet DRY code. Thoughts?

Also, the exact syntax is up for bikeshedding. One possibility is that it becomes an alternative form of _≡⟨_⟩_, instead of a separate call, or both forms could be available.

[dylanede]

I quite like the idea of using _≡⌞⟨_⟩⌟_, to stress that you are operating inside the "hole". A line of a proof might then look like this:

⌞ (b + c) + a * b ⌟ + a * c     ≡⌞⟨ +-assoc b c (a * b) ⟩⌟

[JacquesCarette]

That would be a very nice addition.

Opinions:

1. I would prefer _≡⌞⌟⟨_⟩_ over _≡⌞⟨_⟩⌟_
2. I also prefer to be explicit in my uses of sym.

[dylanede]

OK, I think I prefer that too, so how does this sound?

1. _≡⌞⌟⟨_⟩_ for use in equational reasoning
   2.⌞⌟ as a standalone function-like macro, e.g. ⌞⌟ $ +-assoc b c (a * b)

This second form would be convenient for use in single line proofs, where the ⌞_⌟ wrapped part is part of the signature of the proof. It could be a prefix operator instead to remove the common need for $, but that might make readability suffer.

If we had a defaultTo tactic as alluded to in an example in the Agda documentation, importing the cong macros could be done as follows:

open import Tactic.Holes

would use cong from the standard library, but

open import Tactic.Holes {{mycong}}

would use a different, user-specified implementation.

[ajrouvoet]

Although visually the proposed syntax is fine, I am a little worried about how much effort it takes to input, and that comes from someone who is completely sold on the unicode front :)

Why not either _≡⌞_⌟_ or _≡⌊_⌋_ if you want to or have to distinguish them from the usual infix reasoning combinators?

[JacquesCarette]

Oh, I like those suggestions! Especially the first one. [Sometimes it takes a bad syntax suggestion to prod someone else to have a better one... yeah, I'll go with that! ;) ]

[gallais]

@ajrouvoet's suggestion would make it nicely compatible with the ˘ symbol to
combine sym & automation.

[ajrouvoet]

the ˘ symbol

Talking about syntax, the categories library had the much nicer IMO _↑≡⟨_⟩_ and _↓≡⟨_⟩_ to indicate the direction of the equality. But perhaps that ship has sailed :)

[MatthewDaggitt]

Just to add my voice that this would be a great idea! I like the _≡⌊_⌋_ syntax best myself, but _≡⌞_⌟_ is also good (it's just the brackets are a little low compared to all the other brackets we use).

Talking about syntax, the categories library had the much nicer IMO ↑≡⟨⟩_ and ↓≡⟨⟩_ to indicate the direction of the equality. But perhaps that ship has sailed :)

@ajrouvoet I too would like to do something about the ˘ syntax, even though I introduced it (@JacquesCarette I can definitely relate!). I really hate it: it's difficult to type, it ruins the alignment of proofs and doesn't clearly convey symmetry to me. Perhaps you could open a separate issue in which we could come up with an alternative?

[JacquesCarette]

And now issue #1138 seems to have been introduced for discussing just that. We should keep the discussion here about cong-helper.

[dylanede]

Just a heads up: I'm writing my own implementation, not based on agda-holes. I have the implementation of ⌊_⌋ with ⌊⌋ working, i.e. code like this works:

foo : (a b c : ℤ) → ⌊ a + b ⌋ + c ≡ b + a + c
foo a b c = ⌊⌋ (+-comm a b)

This should also work with the ⌊_⌋ nested deep within lambdas, though it needs more testing to be sure.

It is currently proving a bit tricky to write the _≡⌊_⌋_ form, due to a combination of quote ⌊⌋ not being able to find ⌊⌋ (quote: not a defined name) for some reason, and the type checker being a bit too eager to normalise terms. I am making progress however.

The code is sitting at 139 lines in a single file. It is being tested against cong from the standard library at the moment. I expect that in order to make it cope with cong from, say, agda/cubical, I will need something like an application routine (see agda/agda#3821 for some relevant discussion). This will make the code a bit larger, but I do not see it becoming as complex as agda-holes. It is also fully --safe.