Stream: Coq users

Topic: Coq can't recognize a strictly positive occurrence


view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Feb 25 2023 at 21:06):

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

view this post on Zulip Paolo Giarrusso (Feb 25 2023 at 21:11):

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

view this post on Zulip Paolo Giarrusso (Feb 25 2023 at 21:18):

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

view this post on Zulip Matthieu Sozeau (Mar 06 2023 at 07:37):

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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 06 2023 at 07:48):

(That's basically @Paolo Giarrusso 's solution above.)


Last updated: Jun 24 2024 at 00:02 UTC