Stream: Coq users

Topic: Rewriting pattern not allowed for inversion equations.


view this post on Zulip Pierre Rousselin (Nov 04 2023 at 15:30):

Everything is in the title. Why is that so? Is there a good reason why one cannot use inversion H as [->]?

Edit: it also doesn't accept a discarding pattern.

view this post on Zulip Paolo Giarrusso (Nov 04 2023 at 15:53):

good question. A reproducer:

Require Import List Utf8.
Import Notations.

Lemma inversion_name {A : Type} (x y : A) (xs ys : list A) :
  x :: xs = y :: ys -> x = y  xs = ys.
Proof.
  intros Ha.
  inversion Ha as [Hb].
  Fail inversion Ha as [->].
  Fail inversion Ha as [_].

Last updated: Jun 23 2024 at 04:03 UTC