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