How can I write a proof to match inductive type without using forall in its subterm?

I have a definition:

Inductive type :=
| Bool: type
| Int: type
| Option: type -> type

Then wanna define a proof about property P like this:

Proof type_match_P:
  forall ty ty1,
  (ty = Int \/ ty = Option ty1) -> P ty.

However ty1 does not seem to matter, could I just write something like (Option _) to match it in a proof?

Thank you very much!

Solution

Here are three different ways to represent your assumption, and examples of how to use them:

Inductive type :=
| Bool: type
| Int: type
| Option: type -> type.

Variable P : type -> Prop.

Definition hyp1 (t : type) : Prop :=
  match t with
    | Int | Option _ => True
    | Bool => False
  end.

Inductive hyp2 : type -> Prop :=
  | hypI : hyp2 Int
  | hypO (t : type) : hyp2 (Option t).

Definition hyp3 (t : type) : Prop := t = Int \/ (exists t', t = Option t').

Lemma type_match_P1:
  forall ty, hyp1 ty -> P ty.
Proof.
  intros ty Hty.
  destruct ty, Hty.
Abort.

Lemma type_match_P2:
  forall ty, hyp2 ty -> P ty.
Proof.
  intros ty Hty.
  inversion_clear Hty.
  Undo.
  inversion Hty ; subst ; clear Hty.
Abort.

Lemma type_match_P3:
  forall ty, hyp3 ty -> P ty.
Proof.
  intros ty [-> | [? ->]].
  Undo.
  intros ty Hty.
  destruct Hty as [e | [ty' e]].
  all: subst.
Abort.

The first version computes based on t either the True or False proposition. To use this version, you have to destruct t and then get rid of the either absurd or trivial hypothesis.

The second version represents your assumption as an inductive predicate. To use it, use the inversion tactics and/or its variants such as inversion_clear.

The third is the most similar to yours, except that it uses an existential type rather than a universal quantification. Here you can directly destruct the assumption using intro-patterns, or first introduce it and destruct it later on.

These are just presentation choices: in the end, they all are equivalent. So use the one that fits your needs the most.