HITs with rewrite rules

[Alizter]

In Coq 8.20, it is expected that coq/coq#18038 will be merged giving us rewrite rules in Coq. From experimentation, it would seem that we should be able to define HITs using these rewrite rules. As an example:

Axiom Circle : Set.
Symbol base : Circle.
Symbol loop : paths base base.
Symbol Circle_rec : forall (P : Type), P -> (paths base base) -> Circle -> P.

Rewrite Rule loop_rew :=
| Circle_rec _ ?b ?loop base ==> ?b
| match loop with idpath => @idpath (Circle_rec ?B ?b ?loop base) end ==> ?loop
.

The match is just the normal form for ap as the rewrite rule needs to work on a normal pattern.

We can probably write down the dependent eliminators in this way too. (It might have to come after the non-dependent one to be well-typed).

I think we should definitely experiment with these in the library as they have the potential to save us a lot of path algebra. One thing I don't know about is the semantics for HITs with definitional path computation rules. Obviously, there are things like CTT where this holds, but that doesn't give us the right general model IIUC.

The other question is performance, hopefully reducing HITs won't be too costly. But in the end, it means we can get rid of the private inductive types hack.

[Alizter]

FTR I asked about semantics of strict path computation rules on Zulip and it doesn't look good. It doesn't seem to be known to be possible to have strict path computation rules. So there is that to keep in mind.

https://hott.zulipchat.com/#narrow/stream/228519-general/topic/Semantics.20of.20HITs.20with.20judgemental.20path.20eliminators

On the other hand, cubical agda has them, but the semantics of cubical type theory deal with HITs in a way that allows for them. They don't run into the issue of trying to relate Id's J and HIT eliminators. Then again, I have no idea what a model of cubical sets is supposed to correspond to in homotopy theory.

[jdchristensen]

It would be nice to resolve the semantic issue, but until then, I guess we should avoid this.

Symbol Circle_rec : forall (P : Type), P -> (paths base base) -> Circle -> P.

Just a minor point that this doesn't have the right type. paths base base should instead be a loop in P at the chosen point.

[yannl35133]

I didn't notice it the first time, but since Circle_rec ?B ?b ?loop base can reduce, your second rewrite rule would in practice never be triggered and you would be stuck with a term match loop return paths ?b ?b with idpath => idpath end which would not reduce.
I guess the better solution using rewrite rules would be to do what Théo Winterhalter suggested, a symbol for ap and a reduction for ap ?f idpath.

[Alizter]

That also appears to be the suggestion semantically, but this is not a desirable thing to have. ap appears naturally unrelated to the HIT in question, so I think it would be quite awkward to have to translate back and forth, defeating the purpose of the rewrite rule for the path eliminator in the first place.

[mikeshulman]

Is it not possible to have a single symbol ap satisfying rewrite rules for all HITs? Do the rewrite rules for a given symbol have to all be declared at the same time?

[yannl35133]

The rewrite rules don't have to be declared at the same time. Since they are added to the environment as a block, this is necessary to have rewrite rules which have a correct type thanks to previous rewrite rules (and it's also just convenient).

[mikeshulman]

Ok, then we could just declare the symbol ap along with its rewrite rule for refl in Overture, and then whenever we introduce a new HIT we give ap a rewrite rule for the eliminator of that HIT. I very much doubt we ever use the fact that ap is defined by path induction rather than just its rewrite rule for refl.

[jdchristensen]

That also appears to be the suggestion semantically, but this is not a desirable thing to have. ap appears naturally unrelated to the HIT in question, so I think it would be quite awkward to have to translate back and forth, defeating the purpose of the rewrite rule for the path eliminator in the first place.

But it might work if we used the new ap symbol everywhere that we currently use the ap defined by path induction. I think I know one or two places where we use that some other path induction specializes to our current ap definitionally, so a lemma would be needed there, but I think it's fairly rare. (This comment overlapped with Mike's, but I'm still adding it because I do know one or two places where I currently rely on the definition of ap.)

[mikeshulman]

Oh, okay, I'm surprised. But it should be rare and easy to work around, as you say.

[mikeshulman]

I wonder whether one could prove a conservativity result for a type theory with a primitive ap and apd and definitional path-constructor computation over ordinary Book HoTT. It feels kind of like saying we introduce a new thing ap/apd, and then we say how that new thing computes, and so it's almost like a "definitional extension".

[Alizter]

With my logician hat on, I like to think of strict path computation rules as something akin to cut elimination. I would expect that if the two versions of HoTT really do have the same models, then there ought to be some syntactic procedure allowing you to transform proofs in the slightly stricter HoTT to book HoTT. Comparing the size of say the 3x3 lemma for pushouts' proof in cubical type theory vs Brunerie's proof, its easy to see there is quite a large blowup in various metrics for proof size. This is something that reminds me of the size of proofs with cut eliminated in classical logic.

As you put it @mikeshulman (faster than I could write), this would essentially be equivalent to a conservativity result about these two type theories.

The lack of such a result is still something that makes me uncomfortable however. Even if both HoTTs had the same models, the fact that we don't have anything like completeness for HoTT, means that there is still the question of "is this provable in the weaker theory?".

Practically this would mean we would second-guess every result we prove here with respect to book HoTT.

[Alizter]

Here is an implementation of the interval using rewrite rules: #2098. It can prove funext, but there are some universe issues with rewrite rules I've created a bug report for upstream.

[Alizter]

Here is an updated proof of funext, the previous one didn't fail because of funext but because I forgot some rewrite rules (:innocent:):

Require Import Basics.Overture.
Global Set Asymmetric Patterns.

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.

Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

Symbol Interval : Set.
Symbol i0 : Interval.
Symbol i1 : Interval.
Symbol seg : i0 = i1.

Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y
  := match p with idpath => u end.

Unset Universe Polymorphism.
Symbol ap@{u v} : forall {A : Type@{u}}{B : Type@{v}} (f : A -> B) {x y : A}
  (p : x = y), f x = f y.
Rewrite Rule ap_comp :=
| @ap ?A ?P ?f _ _ (@idpath@{u} _ ?a) => @idpath ?P (?f ?a).
Symbol apD@{u v} : forall {A : Type@{u}} {P : A -> Type@{v}}
  (f : forall x, P x) {x y : A} (p : x = y), transport P p (f x) = f y.
Rewrite Rule apD_comp :=
| @apD ?A ?P ?f _ _ (@idpath _ ?a) => @idpath (?P ?a) (?f ?a).
Set Universe Polymorphism.

Symbol Interval_ind
  : forall (P : Interval -> Type)
      (a : P i0) (b : P i1) (p : transport P seg a = b),
      forall x, P x.

Symbol Interval_rec : forall (P : Type) (a b : P) (p : a = b), Interval -> P.

Rewrite Rule interval_rewrite :=
| Interval_ind ?P ?a ?b ?p i0 => ?a
| Interval_ind ?P ?a ?b ?p i1 => ?b
| Interval_rec ?P ?a ?b ?p i0 => ?a
| Interval_rec ?P ?a ?b ?p i1 => ?b
| apD (Interval_ind ?P ?a ?b ?p) seg => ?p
| ap (Interval_rec ?P ?a ?b ?p) seg => ?p
.

Definition funext {A : Type} {P : A -> Type} {f g : forall x, P x}
  : (forall x, f x = g x) -> f = g.
Proof.
  intros p.
  simple refine (let r := _ in _).
  1: exact (Interval -> forall x, P x).
  { intros i x; revert i.
    exact (Interval_rec _ (f x) (g x) (p x)). }
  exact (ap r seg).
Defined.