Stream: Coq users

Topic: ssreflect equivalent of `destruct x eqn:H`


view this post on Zulip Julin Shaji (Jan 04 2024 at 11:45):

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?

view this post on Zulip Julin Shaji (Jan 04 2024 at 12:09):

Oh... just saw that we can just do case x eqn:H. just like in destruct.
Sorry for the noise. :grimacing:

view this post on Zulip Notification Bot (Jan 04 2024 at 12:09):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Kenji Maillard (Jan 04 2024 at 12:38):

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

view this post on Zulip Julin Shaji (Jan 04 2024 at 12:42):

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?

view this post on Zulip Julin Shaji (Jan 04 2024 at 12:42):

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

view this post on Zulip Notification Bot (Jan 04 2024 at 12:49):

Enrico Tassi has marked this topic as unresolved.

view this post on Zulip Enrico Tassi (Jan 04 2024 at 12:51):

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