证明两个字符串在 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.

Answer 1

dec_trivial

对我来说很快就有用了。

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