[Coq-Club] Ltac: Matching on hypothesis which contains user defined notations

[Abhishek Kr Singh]

Hi,

I have the following definition for an ordType and infix notations for its
boolean comparison operators ==, <b and <=b

Module Order. Structure type: Type:= Pack { sort: Type; eqb: sort-> sort ->
bool; ltb: sort-> sort -> bool; eq_P: forall x y, reflect (eq x y)(eqb x
y); ltb_irefl: forall x, ltb x x=false; ltb_antisym: forall x y, x<>y ->
ltb x y = negb (ltb y x); ltb_trans: forall x y z, ltb x y -> ltb y z ->
ltb x z }. Module Exports. Coercion sort : type >-> Sortclass. Notation
ordType:= type. End Exports. End Order. Export Order.Exports.

Definition sort:= Order.sort. Definition eqb := Order.eqb. Definition ltb
:= Order.ltb.

Notation "x == y":= (@eqb _ x y)(at level 50, no associativity):
bool_scope. Notation "x <b y":= (@ltb _ x y)(at level 0, no associativity):
bool_scope. Notation " x <=b y" := (@leb _ x y)(at level 70, no
associativity): bool_scope.

Now consider the following Ltac definition for show_H which should print
the hypothesis whose type is of the form x == y.

Ltac show_H:=
match goal with
| H: ?x == ?y |- _ => idtac H
end.

However, when I use this definition to show the name of hypothesis in the
following Lemma it fails with the following error message.

Lemma triv (T:ordType)(x y:T): x == y -> y <b x -> 2=3.
Proof. intros. show_H.

(Error: No matching clauses for match.)

Why is the parser unable to match the notation == in the hypothesis ?

[Soegtrop, Michael]

Dear Abishek,

I guess you have a coercion defined from bool to Prop, otherwise eqb x y cannot be on the left side of -> .

Ltac doesn’t know about this coercion, so I think you have to put in the coercion from bool to Prop explicitly in your Ltac match. Enable “Display Coercions” to see what your goal really is.

I also would use an explicit type scope (?x == ?y)%bool for clarity.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Abhishek Kr Singh]

Dear Michael,

Thanks for pointing out.

Indeed, there is a Coercion is_true which maps bool to Prop. I have
changed the Ltac definition as

Ltac show_H:=
match goal with
| H: is_true (?x == ?y)%bool |- _ => idtac H
end.

and it worked correctly. Thanks again.

On Thu, Aug 16, 2018 at 4:10 PM, Soegtrop, Michael <

Post by Soegtrop, Michael
Dear Abishek,
I guess you have a coercion defined from bool to Prop, otherwise eqb x y
cannot be on the left side of -> .
Ltac doesn’t know about this coercion, so I think you have to put in the
coercion from bool to Prop explicitly in your Ltac match. Enable “Display
Coercions” to see what your goal really is.
I also would use an explicit type scope (?x == ?y)%bool for clarity.
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10
<https://maps.google.com/?q=Am+Campeon+10&entry=gmail&source=g>-12, 85579
Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928