## Stream: math-comp users

### Topic: case on a type family with 2 indices

#### Anton Trunov (Apr 27 2021 at 18:09):

Suppose I have a type family with two indices:

``````Inductive foo : nat -> nat -> Prop :=
| A : foo 1 0
| B : foo 0 2.
``````

Now, what would be the SSReflect way to have two equations generated for the two indices in the following case:

``````Goal foo 0 0 -> False.
case E: _ _ /.
- done.
(* unprovable *)
``````

The manual says

The equation name generation feature combined with a type family / switch generates an equation for the first dependent d_item specified by the user.

The equation always refers to the first d_item in the actual tactic call, before any padding with initial _. Thus, if an inductive type has two family parameters, it is possible to have SSReflect generate an equation for the second one by omitting the pattern for the first; note however that this will fail if the type of the second parameter depends on the value of the first parameter.

which makes me think `case: /` cannot handle this. Thanks in advance!

#### Emilio Jesús Gallego Arias (Apr 27 2021 at 18:35):

What I'd do here is to introudce `foo_spec` and `fooP` so `case: fooP` does indeed solve the goal. It is cumbersome due to boilerplate but has never failed me once to produce good proofs and replace inversion.

#### Enrico Tassi (Apr 27 2021 at 20:13):

I think the only way around it (without a spec lemma, which is recommended), is to do something along the lines of

``````move=> H; case E: _ {-1}_ / H (erefl 0).
``````

#### Enrico Tassi (Apr 27 2021 at 20:16):

It would clearly be nicer to write

``````case E1 E2 : _ _ /.
``````

but it is not implemented

#### Anton Trunov (Apr 27 2021 at 20:48):

Thanks for your very helpful answers! I wish `case E1 E2 : _ _ /.` was implemented :)

Last updated: Jul 25 2024 at 17:02 UTC