Stream: Coq users

Topic: Inductive predicate definiton causes Anomaly


view this post on Zulip Xavier Denis (Mar 16 2021 at 14:33):

Hey! I'm trying to define an inductive predicate over hlists, but it causes coq to raise Anomaly Not_found, with no further informaton. Are common pitfalls that I might have walked into?

Coq version 8.13
Here's a minimal-ish test case:

Class ElemOf A B := elem_of: A -> B -> Prop.
Infix "∈" := elem_of (at level 70) .
Inductive Types := tnil: Types | tcons: Type -> Types -> Types.
Implicit Type As: Types.
Infix "^::" := tcons (at level 60, right associativity).
Notation "^[ ]" := tnil (at level 5, format "^[ ]").

Inductive hlist F : Types -> Type :=
| hnil: hlist F ^[]
| hcons {A As} : F A -> hlist F As -> hlist F (A ^:: As).
Infix "+::" := (hcons _) (at level 60, right associativity).

Inductive elem_of_hlist {F A As} : ElemOf (F A) (hlist F As) :=
  | elem_of_hlist_here (x : F A) l : x ∈ (x +:: l)
  | elem_of_list_further (x y : F A) l : x ∈ l -> x ∈ (y +:: l).

view this post on Zulip Xavier Denis (Mar 16 2021 at 14:41):

Well I've partially answered my own question, it seems to be caused by the implicits in definition, moving them to the right of : and explicitly quantifying solves the error, though I still think this should be considered a bug

view this post on Zulip Théo Zimmermann (Mar 16 2021 at 14:41):

Hi Xavier :wave:
When you hit an anomaly, this is always worth reporting. There are already a number of "Anomaly Not_found" issues in the bug tracker, but it's hard to tell whether this one would be a duplicate or not given how non-specific this anomaly is. So the thing to do is to post the minimal test case in the bug tracker and let the experts close it if this is a duplicate.

view this post on Zulip Xavier Denis (Mar 16 2021 at 14:43):

Sounds good, thanks for the response Théo

view this post on Zulip Xavier Denis (Mar 16 2021 at 15:01):

oh wow they're fast.. already reduced it down to a single line


Last updated: Jan 31 2023 at 14:03 UTC