1

我很困惑为什么 assert 和 cut 在这种情况下表现不同。我试图用 ssreflect seq 库来证明这个引理。

Lemma subseq_add_both: forall{A: eqType} (L1 L2: seq A) (a: A),
    subseq L1 L2 -> subseq (a:: L1) (a :: L2).
Proof. intros.
       assert (subseq [:: a] (a:: L2)).

以上工作正常。然而，

Lemma subseq_add_both: forall{A: eqType} (L1 L2: seq A) (a: A),
    subseq L1 L2 -> subseq (a:: L1) (a :: L2).
Proof. intros.
       cut (subseq [:: a] (a:: L2)).

产生错误 Error: Not a proposition or a type.

为什么会这样？我认为 assert 和 cut 都会将任意目标作为参数，但显然情况并非如此。这两种策略在其工作目标方面有何不同？

谢谢你。

4

1 回答 1

2

这可能是一个错误。问题是subseq返回一个布尔值。您可以将其结果用作命题，因为 ssreflect 声明为从tois_true b := b = true的强制转换。我的猜测是，它不适用这种强制，并且会因为它得到一个布尔值而不是一个命题而感到困惑。boolPropcut

您可以通过显式强制转换来解决问题：

cut (is_true (subseq [:: a] (a:: L2))).

但是，由于您已经在使用 ssreflect，我建议您使用haveandsuffices策略而不是assertand cut。例如，

suffices : subseq [:: a] (a :: L2).

给你

2 subgoals (ID 279)
  
  A : eqType
  L1, L2 : seq A
  a : A
  H : subseq L1 L2
  ============================
  subseq [:: a] (a :: L2) -> subseq (a :: L1) (a :: L2)

subgoal 2 (ID 280) is:
 subseq [:: a] (a :: L2)
于 2020-06-29T01:48:06.667 回答