Ltac：在包含用户定义符号的假设上与 ltac 匹配

Question

我有以下关于 ordType 的定义及其布尔比较运算符 ==、<b 和 <=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.

Definition eqb  := Order.eqb.
Definition ltb := Order.ltb. 
Definition leb (T:ordType) := fun (x y:T) => (ltb x y || eqb x y).  


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

现在考虑 show_H 的以下 Ltac 定义，它打印类型为 x == y.

形式的假设

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

但是，当我使用此定义在以下引理中显示假设的名称时，它失败并显示以下消息。

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

 (Error: No matching clauses for match)

为什么解析器无法检测假设中的符号 ==？

Answer 1

发生这种情况是因为强制转换 is_true -- H 假设实际上是 H : is_true (x == y)。

如果像这样启用打印强制转换就可以看到它：

Set Printing Coercions.

Ltac：在包含用户定义符号的假设上与 ltac 匹配

Ltac: Matching with ltac on hypothesis which contains user defined notations

coq

coq-tactic

ltac