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