Also, one specific point I haven’t seen discussed “philosophically” anywhere is the reasonableness of assuming the existence of inaccessible cardinals. There may be some papers somewhere, but likely not readable by (accessible to) regular Coq users.

I think it’s worth pointing out that while the kernel discussion in this post is in some sense distinct from the topic here, it also overlaps quite a lot.

I think the argument regarding the features that are used should be removed entirely. Furthermore, something should be added about the reinforced need to trust the OCaml compiler when using native compute. I don’t feel confident enough to write it, so I’d encourage anyone who does to do so.

You meant to ping @mattam82 in your previous message. BTW, he shared this paper yesterday, where it is again assumed that pCuIC is strongly normalizing.

I don’t know if this is documented anywhere, and I didn’t find any issue about it. Feel free to create one.

Indeed, for a calculus based on eliminators of inductive types which is only a subset of the definitions that are accepted by Coq’s guardness check. Fixing the guard w.r.t. it’s unfolding behavior to ensure any definition can indeed be translated to eliminators is on my list One fix could be to ensure that the reductions the guard does are safe: they never make a recursive call disappear (a kind of linearity condition).

Thanks. For the record, Coq is supposed to implement PCuIC and is therefore expected to be SN?
So, this should be considered a “bug” ? Would it help if we opened an issue?

I think the guard issue is already reported (in any case it’s always been on my mind )

Other than that, indeed it is supposed to implement PCuIC and be consistent and SN. For the SN proof the closest we have is Barras’ work in his habilitation for a model where the guard is represented using sized types instead of a syntactic check IIRC. No such bad examples would typecheck in this system.

About the (categorical) semantics of Coq. Inductive families can be reduced to W-types; see here. These are claimed to be similar to the inductive families of Coq. However, I am not sure I’ve ever seen a precise result along these lines. Voevodsky has made a similar reduction for Coq’s inductive types, but I am not sure it’s entirely up to date, or complete.

But IIUC, the reduction to W-types doesn’t work in standard ITT, because of the lack of functional extensionality; this is explained, for instance in http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf.

@mattam82, if I understand your new equations paper correctly, it addresses this issue by compiling to eliminators, (and a similar thing is done in lean).

Yes, Equations can define functions using the eliminators for accessibility and case analysis, so relies only on eliminators and their defining equations. However by default it still compiles down functions using the struct fix primitives. Adding a mode where we instead try to define it with the standard eliminator instead is a relatively easy TODO

Speaking of compiling to eliminators, I would expect that the specification

0 + y = y
S x + y = S (x + y)

compiles to

Definition add : nat -> nat -> nat :=
nat_rect _ (fun y => y) (fun x a y => S (a y)).

Equations, on the other hand, compiles the above specification to

Definition Add : nat -> nat -> nat :=
fix F x y := match x with
| 0 => fun y0 => y0
| S x' => fun y0 => S (F x' y0)
end y.

which is not definitionally equal to a formulation with the eliminator nat_rect. Is there a reason that Equations produces this unnecessarily complicated code? Why not compile to ``add```? Or, to the definitionally equal

Definition ADD : nat -> nat -> nat :=
fix F x := match x with
| 0 => fun y => y
| S x' => fun y => S (F x' y)
end.

in case the compiler doesn’t distinguish between primitive recursion and structural recursion?