Stream: math-comp users

Topic: case on a type family with 2 indices


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Enrico Tassi (Apr 27 2021 at 20:16):

It would clearly be nicer to write

case E1 E2 : _ _ /.

but it is not implemented

view this post on Zulip Anton Trunov (Apr 27 2021 at 20:48):

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


Last updated: Feb 08 2023 at 08:02 UTC