I would like to do something like this:

```
Inductive ExprZ :=
| EZ_Variable : nat -> ExprZ
| EZ_Literal : Z -> ExprZ
| EZ_Unary : Expr_UnaryOp -> ExprZ -> ExprZ
| EZ_Binary : Expr_BinaryOp -> ExprZ -> ExprZ -> ExprZ
| EZ_Int : forall (size : Expr_IntSize) (signed : Expr_IntSignedness) (e : ExprInt size signed), ExprZ
with ExprInt (size : Expr_IntSize) (signed : Expr_IntSignedness) :=
| EI_Unary : Expr_UnaryOp -> ExprInt size signed -> ExprInt size signed
| EI_Binary : Expr_BinaryOp -> ExprInt size signed -> ExprInt size signed -> ExprInt size signed
| EI_Z : ExprZ -> ExprInt size signed
.
```

but get a `Parameters should be syntactically the same for each inductive type.`

.

Any idea how I could define something with equivalent semantics?

I can't make the parameters arguments to the individual constructors because my proofs rely on that an int expression is in itself type consistent (casts got to Z and back). Also I obviously can't give Z the same parameters since it might involve different int types.

Also is there a good reason for this restriction? I find quite unnatural.

I found a work around - not terribly elegant but OK (or at least I guess so - tbd):

```
Inductive ExprInt (exprZ : Set) (size : Expr_IntSize) (signed : Expr_IntSignedness) : Set :=
| EI_Unary : Expr_UnaryOp -> ExprInt exprZ size signed -> ExprInt exprZ size signed
| EI_Binary : Expr_BinaryOp -> ExprInt exprZ size signed -> ExprInt exprZ size signed -> ExprInt exprZ size signed
| EI_Z : exprZ -> ExprInt exprZ size signed
.
Inductive ExprZ : Set :=
| EZ_Variable : nat -> ExprZ
| EZ_Literal : Z -> ExprZ
| EZ_Unary : Expr_UnaryOp -> ExprZ -> ExprZ
| EZ_Binary : Expr_BinaryOp -> ExprZ -> ExprZ -> ExprZ
| EZ_Int : forall (size : Expr_IntSize) (signed : Expr_IntSignedness) (e : ExprInt ExprZ size signed), ExprZ
.
```

Still I find this restriction unnatural and would appreciate some comments on why it exists.

Hmm - as it looks it is impossible to define a combined mutually recursive function on such a split mutually recursive type.

Are there other suggestions?

Could it work to turn all the parameters into indices?

One alternative would probably be defining your mutually recursive function using a measure.

As @Janno wrote, turning parameters into indices is a good workaround. (But obviously, you would then suffer from universe shenanigans.) As to why there is this restriction on parameters of mutually recursive types, I think it is just because people do not understand what the theory would look like in presence of non-uniform parameters. (Again, because of universes and the like.)

In the Set model, parameters are just bona fide λ-abstractions. I don't see why we wouldn't be able to allow weakening of parameters on a per-block basis just as we allow weakening of variables.

See also https://github.com/coq/coq/issues/5293

We must have a different set model in mind. Because in mine, mutually inductive types are modeled by the smallest set (unbounded intersection) stable by the constructors. But the ability to define this smallest set depends on the parameters being uniform. If they are not, I don't see any simple way of taking their intersection.

`Expr_IntSize`

and `Expr_IntSignedness`

seem small enough to avoid universe problems — you must turn large parameters into indices to get a universe bump.

I also don't expect universe issues - both types are explicitly in Set above.

Let me try your suggestions of using indices.

Re `Set`

models, would that be enough to justify all interesting Coq axioms? It seems you need a model for univalence and one for impredicative Set?

lifting this restriction seems among the topics of https://github.com/coq/ceps/pull/60:

claims such that not all inductive types of a block of mutual inductive types need to have exactly the same parameters are seriously quite frightening.

This *frightening* remark was more about non-uniform parameters. Parameters are just an encoding detail, if we had local inductive types then they'd just be transparent abstractions. Conversely, I cannot claim I understand non-uniform parameters.

Oh! Did you originally mean that, in @Michael Soegtrop 's example, we could just implicitly add the missing parameters to make all the types uniform? If so, I agree.

(Or maybe I don't. It still seems a bit fragile, because the parameters would come out of nothingness.)

@Guillaume Melquiond if we handled parameters as abstractions in inductive types, yes, that would be a trivial solution.

Unfortunately that's not the case so you'd get into conversion issues. There are good reasons to consider parameters "rigid" (mainly performance) but it should be allowed to treat parameters as being only sugar for toplevel lambdas.

A simple cooked-up example: `Inductive foo (n : nat) := Foo.`

. Currently `foo 0`

is not convertible to `foo 1`

but there is no fundamental reason for that. This is true in the Set model for instance, and in any model that implements local inductive blocks.

With such inductive types you could just take the union of all contexts of the blocks of your mutual and feed dummy values.

I'd be very happy personally to have parameters-as-abstractions, even on an opt-in basis, but it'd really be terrible for performance.

Every time you check the conversion between two such inductive types you have to unfold the block and check that the type of the constructors match.

@Guillaume Melquiond : I don't understand how this is supposed to work. Of course I could add the same parameters to ExprZ, but my assumption is that then I can't change the parameters, which I definitely want to do. Say a single term can easily contain both INT32S and INT64U arithmetic. My assumption is that if the bitsize and signedness are common parameters to the mutual inductive, one term can have only one value of these parameters.

@Janno : I looked into changing this into parameters, but I have issues with the proofs then, because then the signdness and bitsize are properties of actual terms and not the type. But I need it in the type for my proofs to work. Or I would have to guard my lemmas with a validity function, which excludes terms which mix types in inappropriate ways.

I guess I will simply merge the ExprZ and ExprInt type into one by introducing a "bounded" parameter in my arithmetic definition records. This way my proofs might even get shorter, although the conversion between Z and int types gets more messy. On the other hand I could then easily add support for other unbounded integer types.

Guillaume Melquiond said:

(Or maybe I don't. It still seems a bit fragile, because the parameters would come out of nothingness.)

concretely, weakening would not seem enough in this artificial example — or anytime the parameter type isn't obviously inhabited (say `m <= n`

where `m`

and `n`

are also parameters):

```
Inductive Foo := | mkFoo : Foo | mkBarFoo x : Bar x -> Foo.
with Bar (x : False) := mkBar : Bar x.
Eval cbv in mkFoo.
```

Here, it's not clear how to translate `mkFoo`

into a closed term if `Foo`

gets `x : False`

as parameter.

IOW, weakening is not enough, you need some "strengthening" at the call site.

After pondering over this for a day, I still find this highly unsatisfactory. I usually have no difficulties to express my ideas in Gallina, but I find this quite hard in this case.

I can use indices instead of parameters, but the meaning is quite different. With indices one could mix and match expressions of different int types arbitrarily - essentially it would convert the typed expression language to an untyped one. I could probably live with this, but I don't really want to live with this.

I can also unify the Z and INT type, but it also expands the term language quite a bit, e.g. I don't have int literals or variables (there are always converted from Z). If I deviate with the structure too much from the terms CompCert / Clightgen produces, I gets tricky to ensure that the interpretation of the term matches the original CompCert expression.

The workaround with passing one type as argument to another works to define the type, but it results in very substantial additional effort in defining fixpoints on this type (see https://github.com/coq/coq/issues/15932).

So does someone have a suggestion on how I could express the expression data structure as above with a Z and a parameterized INT type?

This type I have in mind is really quite simple (it lives in Set) and I find it unsatisfactory that there shall be no way to express it in Coq.

I think I am beginning to understand what you are trying to do but it leaves me more confused. How can the types fix the parameters if one of your constructors contains a universal quantification over the parameters?

I think it would help to have a mathematical formulation of what values you would like to be contained within your types

It could also really help if you could give a bit more context and maybe a "benchmark" function that should be definable with a proposed formulation of the mutual inductive types

I have an expression in Z and it contains a conversion operator for an expression in say INT32. This conversion operator is given the type (INT32) and the expression below the conversion operator shall be an INT32 expression - until it comes to a conversion operator which brings it back to Z.

So this way I have ExprZ, ExprInt32S, ExprInt32U, ExprInt64S, ExprInt64U and conversion operators between ExprZ and any of the int types and any of the int types and ExprZ.

Wait, so what's wrong with...? (modulo typos)

```
Inductive ExprZ : Set :=
| EZ_Variable : nat -> ExprZ
| EZ_Literal : Z -> ExprZ
| EZ_Unary : Expr_UnaryOp -> ExprZ -> ExprZ
| EZ_Binary : Expr_BinaryOp -> ExprZ -> ExprZ -> ExprZ
| EZ_Int : forall (size : Expr_IntSize) (signed : Expr_IntSignedness) (e : ExprInt size signed), ExprZ
with ExprInt : Expr_IntSize -> Expr_IntSignedness -> Set :=
| EI_Unary : forall {size signed}, Expr_UnaryOp -> ExprInt size signed -> ExprInt size signed
| EI_Binary : forall {size signed}, Expr_BinaryOp -> ExprInt size signed -> ExprInt size signed -> ExprInt size signed
| EI_Z : forall {size signed}, ExprZ -> ExprInt size signed
.
```

Okay, I see. So `ExprZ`

really shouldn't be restricted in any way to any particular `size`

or `signedness`

, right? In that case, I do not understand what is wrong with the approach of using indices. I wonder if your proofs simply ran into one of the usual problems with dependent types in Coq.

With indices (as far as I understand this) the type becomes and argument of the individual constructors and and really can't distinguish the types of different kinds of integer expressions.

Let me look into what @James Wood wrote.

They are arguments of the constructors, but also the actual constructors are constrained such that any contiguous subtree of them will maintain the same indices. It should be equivalent to the version with parameters, except for universe levels (which anyway shouldn't be relevant here).

I can use indices instead of parameters, but the meaning is quite different. With indices one could mix and match expressions of different int types arbitrarily

I don't get it, shouldn't

```
with ExprInt : forall (size : Expr_IntSize) (signed : Expr_IntSignedness), Set :=
| EI_Unary size signed : Expr_UnaryOp -> ExprInt size signed -> ExprInt size signed
| EI_Binary size signed : Expr_BinaryOp -> ExprInt size signed -> ExprInt size signed -> ExprInt size signed
| EI_Z size signed : ExprZ -> ExprInt size signed
```

produce the same semantics as the parameter version? the only difference is that matches are harder to write so you probably want to use a helper

```
Definition destruct_ExprInt size signed (P:ExprInt size signed -> Type)
(vUnary : forall op e, P (EI_Unary size signed op e))
(vBinary : forall op e e', P (EI_Binary size signed op e e'))
(vZ : forall z, P (EI_Z size signed z))
: forall e, P e.
Proof.
destruct e;auto.
Defined.
```

@Janno , @James Wood , @Gaëtan Gilbert : yes sorry, you are right. I just had some sort of knot in my brains on this.

One thing that might still be different is that your type might not end up in `Set`

but in `Type`

. At least it does so for me. I axiomatized all the unknown terms to live in `Set`

and as a consequence `ExprInt`

must be a `Type`

.

@Janno : This works in `Set`

(I coerced the bitsize and signedness into one here for convenience in some other definitions):

```
Require Import ZArith.
Inductive Expr_UnaryOp :=
| EU_Neg
.
Inductive Expr_BinaryOp :=
| EB_Add
| EB_Sub
| EB_Mul
| EB_Div
| EB_Shift
.
Inductive Expr_IntType :=
| EIT_32S
| EIT_32U
| EIT_64S
| EIT_64U
.
Inductive ExprZ : Set :=
| EZ_Variable : nat -> ExprZ
| EZ_Literal : Z -> ExprZ
| EZ_Unary : Expr_UnaryOp -> ExprZ -> ExprZ
| EZ_Binary : Expr_BinaryOp -> ExprZ -> ExprZ -> ExprZ
| EZ_Int : forall (type : Expr_IntType) (e : ExprInt type), ExprZ
with ExprInt : Expr_IntType -> Set :=
| EI_Unary : forall {type}, Expr_UnaryOp -> ExprInt type -> ExprInt type
| EI_Binary : forall {type}, Expr_BinaryOp -> ExprInt type -> ExprInt type -> ExprInt type
| EI_Z : forall {type}, ExprZ -> ExprInt type.
```

Let me work this through - with the suggestion by @Gaëtan Gilbert it should be quite smooth.

Janno said:

One thing that might still be different is that your type might not end up in

`Set`

but in`Type`

. At least it does so for me. I axiomatized all the unknown terms to live in`Set`

and as a consequence`ExprInt`

must be a`Type`

.

if it's the same error as I got it's a bug

```
Inductive foo := A | B
with bar : Set :=
C : foo -> bar.
```

says `Error: Large non-propositional inductive types must be in Type.`

but annotating `foo : Set`

makes it work as it should

https://github.com/coq/coq/issues/15934

Oh, indeed! Fully annotating both types worked.

All my fixpoints went through with the suggestion by @James Wood / @Gaëtan Gilbert.

Sorry for the fuzz and thanks a lot for the help!

Michael Soegtrop has marked this topic as resolved.

Last updated: Jun 15 2024 at 08:01 UTC