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: Apr 18 2024 at 07:02 UTC