Generating depth-indexed variant of an inductive

Using Coq
1

Hello,

Is there an already existing plugin to automatically derive, from an Inductive type or predicate, a version of it enriched with the depth/size of the tree? For example, if I have

Inductive Has0 A : list A -> Prop :=
  | Has0_head : forall L,
      Has0 (0 :: L)
  | Has0_tail : forall x L,
      Has0 L -> Has0 (x :: L).

Then I would like to automatically derive another Inductive looking like

Inductive Has0_sized A : list A -> nat -> Prop :=
  | Has0_head_sized : forall L,
      Has0_sized (0 :: L) 0
  | Has0_tail_sized : forall x L n,
      Has0_sized L n -> Has0_sized (x :: L) (S n).

As well as a lemma of the form

Lemma Has0_sized_of_unsized : forall A (L: list A),
  Has0 L -> exists n, Has0_sized L n.

If no such plugin exists but someone knows of some code achieving something similar I could take a look at and maybe adapt, it would also be of great help to me.

Thank you

2

As far as I know, there is no plugin doing this. If you want to try and create such code yourself, I would advise looking at either Coq-Elpi (Enrico Tassi has a few papers on how to use it to do various manipulations on inductive type declarations), or MetaCoq (see this paper for an example). Both tools let you do meta-programming for Coq without having to directly fight in OCaml with the internals of the system.