coq - 是什么阻止 Coq 执行简单的重写？

Question

在清除所有多余的假设之后，我在 Coq 中实现了以下目标:

1 focused subgoals (unfocused: 1-1-1-0-0)
, subgoal 1 (ID 14043)

  in_contents : list byte
  H0 : Zlength in_contents = 1
  ============================
   0 <= 0 < Zlength in_contents

并且，对于上下文:

Print byte.
byte = {b : Z | 0 <= b < 256}
     : Set

但是，重写 H0 给出:

Error: Found no subterm matching "Zlength in_contents" in the current goal.

但是，我可以做这个荒谬的证明:

split; try omega.
change ((1-1) < Zlength in_contents); rewrite <- H0; omega.

我确信我在这里错过了一些基本的东西。

(更奇怪的是，这工作正常:)

Example what : forall (in_contents:list byte), Zlength in_contents = 1 -> 0 <= 0 < Zlength in_contents.
Proof.
  intros in_contents H0.
  rewrite H0.
  omega.
Qed.

Answer 1

正如其他人所提到的，重写可能会受到目标或假设中某些隐藏术语的阻碍。此类问题有两个常见来源:

强制:

Coq pretty-print 默认隐藏强制转换(自动类型转换)。说明该问题的示例是:

Section CRew.
Variable (A B : Type) (f : A -> B).

Coercion f : A >-> B.

Variable (x y : A).
Hypothesis H : @eq B x y.

Print H.

Lemma L1 : x = y.
(* rewrite H. fail *) Abort.

Set Printing Coercions.
Print H. (* H : f x = f y *)

End CRew.

在这种情况下，H 实际上指定了 f x 和 f 之间的相等性 y 但显示为 x = y。

隐式参数

另一个常见的混淆来源是隐式参数功能。再次看一下这段代码。

Section IARew.

Definition U := fun (_ : nat) => nat.
Variable (f : forall x, U x -> B).
Arguments f [x] y.

Hypothesis H : eq (@f 1 2) (@f 2 3).
Print H.

Lemma L2 : (@f 2 2) = (@f 2 3).
(* rewrite H. Fail. *) Abort.

Set Printing Implicit.
Print H.

End IARew.

此处，@f 1 2 和 @f 2 2 显示为 f 2，导致困惑。

我希望它有帮助，您可以在以下位置运行示例: https://x80.org/collacoq/eqosecuzar.coq