Syntax of the case tactic in coq

Question

Can someone explain to me what the following coq tactic is doing? case x : fun H => [|[]] // _. How would I rewrite this using destruct?

Even better, can anyone point me to somewhere in the coq documentation where the above syntax is explained?

Answer 1

The example given in the initial posting does not parse, so here is an attempt to produce a similar case command, but without the syntax error.

case : is part of the ssreflect idiom. case name : value . does approximately the same thing as destruct value eqn: name. The => is about making intro patterns in each case.

Here, I will explain the behavior of the following line:

case name : x H => [|[]] // _.

This does a destruct on x (we expect x to be in a type with two constructors, the second constructor having an argument which is itself in an inductive type; if x is in type nat this will work).

Now there is a subtlety from the fact that H appears between x and =>. This means that the H hypothesis will be reverted to the conclusion of the goal before the case command is performed.

revert H; destruct x as [ | [ | temporary_name]] eqn:name; try easy; intros _" 

The try easy is here to represent the // used in the ssreflect idiom. The intros _ is here to represent the _ present at the end of the ssreflect line: it gets rid of the corresponding instance of H in the remaining case, probably because this contains a useless truth.

This explanation is not an exact match, because case ... : ... performs no modifications in the goal hypotheses (except the one that was reverted), while destruct modifies any hypothesis where x occurs.

Here is an example of session where both tactics behave the same:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section sandbox.

Variable P : nat -> Prop.


Lemma toto (x : nat) (H : x == 1) : P x.
Proof.
revert H; destruct x as [| [| temporary]] eqn: name; try easy; intros _.
Abort.

Lemma titi (x : nat) (H : x == 1) : P x.
Proof.
case name : x H => [|[]] // _.
Abort.