Trying to get a parameterized inductive type into induction

Using Coq
1

I have defined the following inductive datatype:

Inductive action : ioh -> Type :=
| inputEvent: nat -> list types -> string -> nat -> nat -> action Input
| outputEvent: nat -> list (nat + bool) -> string -> nat -> nat -> action Output
| matchEvent: nat -> nat -> action Input -> action Output -> action Internal
| dbAccess : nat -> nat -> dbacc -> nat -> action Internal
| guard : nat -> nat -> bool -> action Internal
.

that is parameterized to distinguish input, output and internal actions. I want to have a proof about that if we have some element a:action Input it must be of structure (inputEvent n l s n1 n2). So i assume something like this:

Lemma action_Input_is_inputEvent : forall (n : nat) (ts : list types) (name : string) (tid : nat) (sid : nat) (a : action Input),
  a = inputEvent n ts name tid sid.

I tried to have a proof:

intros n ts name tid sid a.
induction a.

But this give me the error: The 3rd term has type “action Input” which should be coercible to “action i0”.
For me it seems that we cannot apply induction here, because not all cases are well-typed. Is there a way to have this kind of Lemma proven in Coq ? Or is there maybe a smarter way to define my datatype to make it more easy? Thank you!

2

I want to have a proof about that if we have some element a:action Input it must be of structure (inputEvent n l s n1 n2).

To express this, do not use forall but exists:

Lemma action_Input_is_inputEvent : forall (a : action Input), exists (n : nat) (ts : list types) (name : string) (tid : nat) (sid : nat),
  a = inputEvent n ts name tid sid.

Then, dependency makes indeed that induction, or destruct, or inversion, or dependent inversion, or case_eq, … don’t work. However, dependent destruction works:

Inductive ioh := Input | Internal | Output.
Axiom types dbacc : Type.
Require Import String.
Inductive action : ioh -> Type :=
| inputEvent: nat -> list types -> string -> nat -> nat -> action Input
| outputEvent: nat -> list (nat + bool) -> string -> nat -> nat -> action Output
| matchEvent: nat -> nat -> action Input -> action Output -> action Internal
| dbAccess : nat -> nat -> dbacc -> nat -> action Internal
| guard : nat -> nat -> bool -> action Internal.

Require Import Program.
Lemma action_Input_is_inputEvent : forall (a : action Input), exists (n : nat) (ts : list types) (name : string) (tid : nat) (sid : nat) ,
  a = inputEvent n ts name tid sid.
intros.
dependent destruction a.
repeat eexists.
Qed.

Alternatively, dependent destruction a can be replaced by refine (match a with inputEvent n ts name tid sid => _ end).