Stream: Coq users

Topic: Non supported pattern with ssreflect's if

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.)

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)

Théo Winterhalter (Apr 30 2022 at 12:40):

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

Last updated: Apr 19 2024 at 12:02 UTC