```
Inductive even : nat -> Type := EZ : even 0 | ES n : odd n -> even (S n)
with odd : nat -> Type := OS n : even n -> odd (S n).
Definition even_comm_cast n m : even (n + m) -> even (m + n).
by rewrite addnC.
Defined.
Theorem esumC n m (p : even (n + m)) (q : even (m + n)) :
p = even_comm_cast _ _ q.
Proof.
rewrite /even_comm_cast.
case: (n + m) / addnC p.
Admitted.
```

There is a theorem esumC in code above that postulates the sum of two even numbers commutes.

I have 2 questions here.

1) What is going on in line `case: (n + m) / addnC p.`

? I think I understand what is a `/`

(view) in the simplest cases. I think I also understand the view hints a bit. I think I also understand that this line is a way to perform kind of `case: (addnC n m)`

. But I'm not sure I understand the syntax of expression `(n + m) / addnC p`

.

2) Is there a way to and why I'm not able to perform case analysis in the next theorem?

```
Theorem example a : a = 3 -> True.
Proof. case.
```

Coq says:

```
SSReflect: cannot obtain new equations out of
(a = 3)
Did you write an extra [] in the intro pattern? [spurious-ssr-injection,ssr]
```

I expected to see all occurences of `a`

to be replaced by `3`

. But nothing happened (expect the warning).

// Great thanks to @Arthur Azevedo de Amorim for the code sample.

SSReflect's `case`

has a specialized behavior in case of equalities. Instead of behaving like `rewrite <-`

, it behaves like `injection`

.

As for `: foo /bar qux`

(irrespective of `case`

), it means that `qux`

is first generalized, then `bar`

is applied to this generalization, and finally `foo`

is generalized.

IIUC, `case: _ / _`

is the the ssreflect syntax for the regular behavior of case/destruct on equalities (i.e., `rewrite <-`

and replace occurences of the equality proof by `erefl`

). The part before the / is the pattern to be replaced and allows for occurrence switches. Consider:

```
Lemma exmaple a : 3 = a -> a * a = 9.
move => E.
```

and then compare the behavior of `case: a / E`

and `case {1}a / E`

. Note that most of the time the pattern can be inferred and thus be replaced by `_`

.

Here, `/`

is not the view switch, but the type family switch (https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#type-families). `case: a b / c d`

is basically equivalent to `move: c d; case: a b /`

.

@Guillaume Melquiond, @Christian Doczkal thank you for explanation.

@YAMAMOTO Mitsuharu thank you for explanation and documentation link.

I think I understand it a bit better now.

Andrey Klaus has marked this topic as resolved.

Last updated: Jun 25 2024 at 18:02 UTC