我对 ordType
有以下定义及其 bool 比较运算符的中缀符号 ==
, <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)
为什么解析器无法检测符号==
在假设中?
最佳答案
发生这种情况是因为强制 is_true
- H
假设实际上是 H : is_true (x == y)
。
如果您启用打印强制,您可以看到它,如下所示:
Set Printing Coercions.
关于coq - Ltac:根据包含用户定义符号的假设与 ltac 进行匹配,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/51873274/