Open cangiuli opened 3 years ago
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.
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?
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.
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
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 ordinaryhcom
tactic does. Instead of inserting anhcom
term, it creates and then inserts a fresh global symbolx : [...] → (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 anhcom
, and (2) we may include a mechanism for replacingx
by the correspondinghcom
. It differs from the current treatment ofhcom
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.sym
in terms ofsym/filler
, etc.cubicaltt
indicates that very few proofs rely on the type-specifichcom
equations, soabstract-hcom
is likely to suffice in most circumstances. In essence, this proposal simulates weak cubical type theory incooltt
. Note that the type-specifichcom
equations hold up to a path even in weak cubical type theory.