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

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