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!

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.

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).
```

It would clearly be nicer to write

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

but it is not implemented

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

was implemented :)

Last updated: Jul 25 2024 at 17:02 UTC