Why is Coq consistent? What is the intended semantics?

Miscellaneous
22

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?

23

In principle it can be adapted to do that, but that’s still on my TODO list