Stream: Coq users

Topic: ✔ Mutual inductives with different parameters

Michael Soegtrop (Apr 19 2022 at 09:10):

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.

Michael Soegtrop (Apr 19 2022 at 09:32):

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.

Michael Soegtrop (Apr 19 2022 at 10:33):

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?

Janno (Apr 19 2022 at 10:35):

Could it work to turn all the parameters into indices?

Janno (Apr 19 2022 at 10:38):

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

Guillaume Melquiond (Apr 19 2022 at 11:59):

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.)

Pierre-Marie Pédrot (Apr 19 2022 at 12:05):

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.

Pierre-Marie Pédrot (Apr 19 2022 at 12:09):

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

Guillaume Melquiond (Apr 19 2022 at 12:23):

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.

Paolo Giarrusso (Apr 19 2022 at 12:40):

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

Michael Soegtrop (Apr 19 2022 at 12:42):

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

Let me try your suggestions of using indices.

Paolo Giarrusso (Apr 19 2022 at 12:53):

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?

Paolo Giarrusso (Apr 19 2022 at 12:59):

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.

Pierre-Marie Pédrot (Apr 19 2022 at 13:06):

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.

Guillaume Melquiond (Apr 19 2022 at 13:09):

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.

Guillaume Melquiond (Apr 19 2022 at 13:11):

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

Pierre-Marie Pédrot (Apr 19 2022 at 14:21):

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

Pierre-Marie Pédrot (Apr 19 2022 at 14:22):

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.

Pierre-Marie Pédrot (Apr 19 2022 at 14:24):

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.

Pierre-Marie Pédrot (Apr 19 2022 at 14:25):

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

Pierre-Marie Pédrot (Apr 19 2022 at 14:26):

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.

Pierre-Marie Pédrot (Apr 19 2022 at 14:26):

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.

Michael Soegtrop (Apr 19 2022 at 15:31):

@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.

Michael Soegtrop (Apr 19 2022 at 15:33):

@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.

Michael Soegtrop (Apr 19 2022 at 15:35):

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.

Paolo Giarrusso (Apr 19 2022 at 16:32):

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.

Michael Soegtrop (Apr 20 2022 at 09:13):

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.

Janno (Apr 20 2022 at 09:17):

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?

Janno (Apr 20 2022 at 09:18):

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

Janno (Apr 20 2022 at 09:22):

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

Michael Soegtrop (Apr 20 2022 at 09:22):

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.

James Wood (Apr 20 2022 at 09:28):

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
.

Janno (Apr 20 2022 at 09:28):

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.

Michael Soegtrop (Apr 20 2022 at 09:30):

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.

Michael Soegtrop (Apr 20 2022 at 09:31):

Let me look into what @James Wood wrote.

James Wood (Apr 20 2022 at 09:33):

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).

Gaëtan Gilbert (Apr 20 2022 at 09:34):

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.

Michael Soegtrop (Apr 20 2022 at 09:40):

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

Janno (Apr 20 2022 at 09:41):

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.

Michael Soegtrop (Apr 20 2022 at 09:46):

@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.

Michael Soegtrop (Apr 20 2022 at 09:47):

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

Gaëtan Gilbert (Apr 20 2022 at 09:48):

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

Gaëtan Gilbert (Apr 20 2022 at 09:50):

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

Janno (Apr 20 2022 at 09:53):

Oh, indeed! Fully annotating both types worked.

Michael Soegtrop (Apr 20 2022 at 09:58):

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!

Notification Bot (Apr 20 2022 at 09:58):

Michael Soegtrop has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC