Ssreflect Users Discussion List

[bertot <>]

Here are two examples that provoke errors that could be perfected.

Require Import ssreflect eqtype ssrbool.

Lemma toto : forall (a b c : bool), a -> (b, a) = (b, c) -> true.
move => a b c; case q: a => [[bb ac] | [bb ac]].

The mistake is on the user's side, but the error message is an anomaly, 
assert failure.

This has been verified with ssreflect-1.3pl1, coq8.3pl2, ocaml-3.12.0, 
camlp5-6.02.0

and with the version 3124 of coqfinitgroup (with modifications in Make 
and ssreflect.v to avoid using a ssrcoq binary), coq-8.3pl2, etc.

The following example also does not work, but this time I think the 
behavior of "injection patterns" is debatable.

Require Import ssreflect eqtype ssrbool.

Lemma toto : forall (a b c : bool), a -> (b, a) = (b, c) -> true.
move => a b c; case q: a => [_ [_ ac] | _ [_ ac]].

The two equalities generated by an injection command would be:

b = b
and
true = c
or
false = c

Because the first equation is essentially useless, it is not generated, 
but I am not sure this what most users will expect, because it is not 
what I expected.

Yves