The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

Thank you Frédéric.

That definitely implies my rule, taking `f x n = x`, and `h x n IH = IH`, we have `f x (S n) = x = h x n x = h x n (f x n)`, and thus `\x n. x = R (\x.x) (\x n IH. IH)`, which is what I wanted.

I retain hope that my rule is enough weaker to retain decidability and Church-Rosser, but now I'm looking at the right references in the literature.

Thanks.

- Jasper Hugunin

On Wed, Jan 3, 2018 at 4:02 PM, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

Hi.

About eta for iteration, see for instance "A NOTE ON REWRITING THEORY FOR UNIQUENESS OF ITERATION" of M. Okada and P. Scott, Theory and Applications of Categories, 6, 47-64 in 2000:

The rule is:

f = R a h where f : A x nat -> B, R is the recursor on nat and a = \x.f x 0,

if for all x and y, f x (S n) = h x n (f x n).

"(i) It is undecidable,

(ii) Church-Rosser fails, although ground Church-Rosser holds,

(iii) strong normalization (termination) is still valid.

This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system."

Frédéric.

Le 03/01/2018 à 03:13, Jasper Hugunin a écrit :

Hi Cody,

Thanks for your response.

Neither of the rules you mentioned seem to quite match what I am looking for (though maybe they imply it).

As I understand it, eta for inductives reduces (fix id n := match n with O => O | S m => S (id m) end) to (fun n => n),

or reduces (match n with O => O | S m => S m end) to n.

Neither of these seem to apply when defining a function (nat -> A).

Commutative conversions allow to move the application of a function across a match (into and out of the branches).

But there is no function applied to the match in (fix shift n := match n with O => a | S m => shift m end),

and no shared function that I see applied to the branches (a) and (shift m).

Perhaps you know of a more general meaning for these rules or some tricky set of rewrites to use to derive it?

I'll attach my example below. Modulo this reduction, it is an implementation of coinductive types from nat, pi, and sigma,

with an anamorphism and eliminator such that the eliminator computes on the anamorphism.

Under the univalence axiom, these types should be equivalent to the ones in the paper below,

which were shown to have the correct equality types.

The main ideas are all in

NON-WELLFOUNDED TREES IN HOMOTOPY TYPE THEORY

BY: BENEDIKT AHRENS, PAOLO CAPRIOTTI, AND RÉGIS SPADOTTI

<https://hott.github.io/M-types/m-types.pdf>,

this development just improves the computational behavior.

I don't have much hope for adding this reduction to Coq, since it seems very specific to nat,

but I was thinking it could be interesting to develop a type theory with such a rule,

and then get coinductive types for free.

Best,

- Jasper Hugunin

On Tue, Jan 2, 2018 at 9:47 PM, roux cody <cody.roux AT gmail.com> wrote:

Hi Jasper!

    This rule is sometimes called "eta for inductives" or "commutative conversions". In some versions it may break confluence, and in general is quite difficult to implement in Coq.

See also this discussion:  https://github.com/coq/coq/issues/3119

If you post your complete example, someone may have a workaround which does not require such a powerful conversion rule!

Best,

Cody

On Tue, Jan 2, 2018 at 2:20 AM, Jasper Hugunin <jasperh AT cs.washington.edu> wrote:

Hello,

I ran into the following function:

(fix shift n := match n with O => a | S m => shift m end) : nat -> A

which clearly on any concrete n reduces to a.

It would be very convenient if this was judgmentally equal to (fun _ => a).

Of course, this is not implemented in Coq, but I haven't been able find any references discussing such a reduction. Does anyone know what the cost of adding such a reduction would be?

(does it break decidable type-checking, or introduce unreasonable computational overhead?)

Where this comes from, is that I actually have a family of types A : nat -> Type, along with

forall n, A n = A (S n), and a0 : A 0. My function then looks like (fun n => nat_rect A a0 (coerce) n),

but for some specific instances A is actually independent of n, and the equalities are eq_refl.

In the general case, I don't see how to do a useful reduction, but when given such nice data I would

have liked to return just a, independent of n.

- Jasper Hugunin