Andrew Appel (Feb 25 2023 at 14:21): Andrew Appel (Feb 25 2023 at 14:21):Consider the following Inductive definitions. The first one is simply a generalization of the second one, but Coq complains that the first one does not have "strictly positive" occurrences. As you can see from the demonstration in the second version, semantically it's strictly positive, but Coq somehow can't see that. And also as you can see, the second one is less general than the first one (works only for n=1,2 instead of any natural-number length), so I would really like to use the first one. Does anyone have a suggestion?
Require Import List.
Axiom type: Type.
Axiom ftype: type -> Type.
Fail Inductive expr (ty: type): Type :=
| Const (c: ftype ty)
| Func (argt: list type) (args: fold_right (fun t => prod (expr t)) unit argt).
(*The command has indeed failed with message:
Non strictly positive occurrence of "expr" in
"forall argt : list type,
fold_right (fun t : type => prod (expr t)) unit argt ->
expr ty". *)
Inductive expr (ty: type): Type :=
| Const (c: ftype ty)
| Func1 (argt: type) (arg: expr argt)
| Func2 (argt1 argt2: type) (arg1: expr argt1) (arg2: expr argt2).
what about using something hlist-like?
Require Import List.
Import ListNotations.
Axiom type: Type.
Axiom ftype: type -> Type.
Inductive klist (k : type -> Type) : list type -> Type :=
| Nil : klist k []
| Cons {ty tys} : k ty -> klist k tys -> klist k (ty :: tys).
Inductive expr (ty : type): Type :=
| Const (c: ftype ty)
| Func {tys : list type} (x : klist expr tys).
I've also tried an hlist indexed by a list Type directly, which seems more standard, but that gave a universe inconsistency — possibly because packing types makes hlist a "large" datatype, but I try to stay away from universes whenever I can:
Inductive hlist : list Type -> Type :=
| Nil : hlist []
| Cons {ty tys} : ty -> hlist tys -> hlist (ty :: tys).
Inductive expr (ty : type): Type :=
| Const (c: ftype ty)
| Func {tys : list type} (x : hlist (map expr tys)).
(*
Error: Universe inconsistency. Cannot enforce hlist.u0 =
max(Set, type.u0, ftype.u0, hlist.u0+1, hlist.u1+1).
*)
I wanted to double-check I didn't fool myself somehow and my proposal makes sense, so here's a possible development:
Require Import List.
Import ListNotations.
Inductive type :=
| Bool
| Fun (dom cod : type).
Fixpoint ftype (ty : type) : Type :=
match ty with
| Bool => bool
| Fun dom cod => ftype dom -> ftype cod
end.
Inductive klist {k : type -> Type} : list type -> Type :=
| Nil : klist []
| Cons {ty tys} : k ty -> klist tys -> klist (ty :: tys).
Arguments klist : clear implicits.
Inductive expr {ty : type}: Type :=
| Const (c: ftype ty)
| Func {tys : list type} (x : klist (@expr) tys).
Arguments expr : clear implicits.
Definition test : expr (Fun Bool Bool) :=
Func (Cons (@Const Bool false) (Cons (@Const Bool true) Nil)).
@Pierre-Marie Pédrot I think you had ideas how to extend positivity to match, maybe fix is also possible in some cases ? I wonder what the generated induction principle would look like here.
Pierre-Marie Pédrot (Mar 06 2023 at 07:47):My plan was to allow at least the stuff we know how to encode via a nested indirection.
Pierre-Marie Pédrot (Mar 06 2023 at 07:48):(That's basically @Paolo Giarrusso 's solution above.)
Last updated: Oct 13 2024 at 01:02 UTC