Stream: Coq users

Topic: Non supported pattern with ssreflect's if


view this post on Zulip Théo Winterhalter (Apr 29 2022 at 13:51):

Consider the following:

Require Import ssreflect.

Goal forall b : bool, (if b then 0 else 1) = 1.
Proof.
  Fail lazymatch goal with
  | |- context [ if _ then _ else ?xx ] =>
    idtac
  end.
  lazymatch goal with
  | |- context [ if _ then ?xx else _ ] =>
    idtac
  end.

Matching on the content of the left branch is fine, but not in the right one. It fails with "Non supported pattern". (At least for 8.14.)

view this post on Zulip Gaëtan Gilbert (Apr 30 2022 at 10:42):

it seems the ssreflect boolean_if_scope if produces something like match _ with true => _ | _ => ?xx end after notation interpretation, and pattern_of_glob_scope can only handle default cases if they produce _ (ie _ => _ not _ => anything else)

view this post on Zulip Théo Winterhalter (Apr 30 2022 at 12:40):

Should I report a bug? Because it's quite annoying I would say.


Last updated: Feb 09 2023 at 00:03 UTC