lean - 在精益中证明两个字符串是不同的

Question

当我执行我的精益定理证明的正常过程时，我意识到我当前的文件需要很长时间才能编译。然后我将问题缩小到我试图证明两个字符串是不同的部分：

lemma L0 : "x" ≠ "y" :=
begin
  intros H, cases H
end

仅这个小引理就需要 15 秒才能在我的（尽管）慢机器上编译。事情严重错误。

我不是一个流利的精益用户，所以猜测我不应该使用这种cases策略 string。我还可以做些什么？

Coq 中相应的引理可以正常工作，没有任何时间问题：

Require Import String.

Open Scope string_scope.

Lemma L0 : "x" <> "y".
Proof.
    intros H. inversion H.
Qed.

score 3 · Accepted Answer

3

dec_trivial对我来说工作得很快。

lemma L0 : "x" ≠ "y" := dec_trivial

于 2020-06-23T17:49:00.523 回答

1 回答 1