Abstract hcom mechanism

[cangiuli]

The goal of this proposal, developed with @jonsterling, is to make hcom less unwieldy in practice. Comments are very welcome.

The basic idea is to add a new abstract-hcom A r r' φ p tactic that succeeds exactly when the ordinary hcom tactic does. Instead of inserting an hcom term, it creates and then inserts a fresh global symbol x : [...] → (i : I) → sub A {φ ∨ i=r} {p i _} for the corresponding filler parameterized over the current hypotheses. In other words, it creates a special kind of hole differing from ordinary holes in two ways: (1) the development is not considered incomplete, because this hole can be resolved by an hcom, and (2) we may include a mechanism for replacing x by the corresponding hcom. It differs from the current treatment of hcom by (1) not unfolding, and (2) importantly, making sure that the entire filler is always around even if the user only asks for the composite.

The rationale is the following:

• hcom terms can be large and difficult to read in goals. The most relevant information for users is their boundary, which we capture here in the large type of a small term. We conjecture this will be easier to understand, and certainly will result in shorter goals.
• As in the proofs of the groupoid laws via hcom, proving laws about composites often require the associated filler. This essentially automates the pattern of defining sym in terms of sym/filler, etc.
• @mortberg's experiment with weak cubicaltt indicates that very few proofs rely on the type-specific hcom equations, so abstract-hcom is likely to suffice in most circumstances. In essence, this proposal simulates weak cubical type theory in cooltt. Note that the type-specific hcom equations hold up to a path even in weak cubical type theory.

[favonia]

My only question is that it seems we can simulate this with opaque lemmas? That is, it appears that we could define an opaque hcom with all the cubical constraints and then use it whenever we don't want the hcom to compute.

[jonsterling]

I think the one place where we need some special feature it make the coherence with between an abstract hcom and something else. Am I missing something?

[cangiuli]

I think that's right -- it would help future automation if we knew that this particular opaque lemma is hcom. It would also be desirable to allow it to unfold in some circumstances, but maybe that's better deferred to a discussion on controlling unfolding. But I take @favonia's point that we can try out this idea immediately.

[cangiuli]

Actually, there is one really important aspect of this design that I've only just edited into the issue description (sorry about that! lol), and it's that the created symbol should always be the filler even if only the composite is being used. This alleviates the common problem that one defines symm and then realizes that they actually have to define symm/filler if they want to prove a law about symm, etc. /cc @favonia