In non-ssreflect style, `destruct`

tactic can be used while also remembering something about what was destructed upon (something like that, right?) by adding `eqn: H`

at the end.

Is there something similar in ssreflect's `case`

tactic?

Oh... just saw that we can just do `case x eqn:H.`

just like in `destruct`

.

Sorry for the noise. :grimacing:

Julin Shaji has marked this topic as resolved.

I think the ssreflect standard way to keep the equation is `case H: x`

.

I had been trying this:

```
Lemma eqbP : forall (n m: nat),
reflect (n = m) (Nat.eqb n m).
Proof.
move => n m.
case (Nat.eqb n m) eqn:H.
(* case (Nat.eqb n m): H. *) (* Gave error *)
```

It gave error when the `eqn`

wasn't there. Didn't I do it right?

Error was: `Syntax error: [ltac_use_default] expected after [tactic] (in [tactic_command]).`

Enrico Tassi has marked this topic as unresolved.

You should write `case H: (Nat.eqb n m)`

, but note that this is not the preferred way to prove a reflect.

See section 5.1.2 of https://zenodo.org/records/7118596

Last updated: Jun 22 2024 at 16:02 UTC