## Stream: Coq users

### Topic: ✔ [ssreflect] what is going on in this view

#### Andrey Klaus (Sep 03 2021 at 13:47):

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

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.

#### Guillaume Melquiond (Sep 03 2021 at 14:06):

SSReflect's `case` has a specialized behavior in case of equalities. Instead of behaving like `rewrite <-`, it behaves like `injection`.

#### Guillaume Melquiond (Sep 03 2021 at 14:08):

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.

#### Christian Doczkal (Sep 03 2021 at 14:20):

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

#### YAMAMOTO Mitsuharu (Sep 04 2021 at 08:44):

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

#### Andrey Klaus (Sep 06 2021 at 07:38):

@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.

#### Notification Bot (Sep 06 2021 at 07:38):

Andrey Klaus has marked this topic as resolved.

Last updated: Sep 26 2023 at 12:02 UTC