Stream: math-comp users

Topic: Inference difference between `destruct`, `case:` and `case`.


view this post on Zulip DArends (May 03 2024 at 11:42):

Hi, I'm wondering what the difference is for the inference of implicit parameters for the destruct, case: and case tactics.
For example:

From mathcomp Require Import eqtype ssrbool ssreflect.

Parameter T : eqType.
Parameters x y : T.

Goal x = y \/ x != y.
Proof.
    (* This fails with "Cannot infer the implicit parameter T of eqVneq whose type is "eqType" " *)
    destruct (eqVneq).
Abort.

Goal x = y \/ x != y.
Proof.
    (* This succeeds *)
    case (eqVneq).
Abort.

Where can I find information regarding this process for related questions?

view this post on Zulip Reynald Affeldt (May 03 2024 at 14:40):

I am sure you have already looked at the Coq manual (destruct tactics and the ssreflect documentation).
Maybe there are relevant comments in the source code of the ssreflect plugin (file coq/plugins/ssr/ssrelim.ml ?).

view this post on Zulip Pierre Roux (May 04 2024 at 11:50):

In any case, eqVneq has been developped and tested to be used with ssreflect case:, using it with ltac case or destruct might or might not work, that's pure luck.


Last updated: Oct 13 2024 at 01:02 UTC