在 Coq 中展开一个不透明的固定点

Question

我目前正在解决软件基础问题，并在 IndProp 章节中进行练习“filter_challenge”。我在 merge_filter 定理中遇到了以下问题。当我尝试展开 All 固定点并说它不透明时，Coq 出错。我不知道为什么它是不透明的。 我曾尝试使用 cbv 来计算 Fixpoint 一次，但它不起作用（而且我不确定如何使用它，或者它是否是适合这项工作的工具）。

这是我对合并的定义：

Inductive merge {X:Type} : list X -> list X -> list X -> Prop :=
(* FILL IN HERE *)
| merge_nil : merge [] [] [] 
| merge_head l1 l2 l (x: X) (H: merge l1 l2 l) : merge (x::l1) l2 (x::l)
| merge_comm l1 l2 l (H: merge l1 l2 l) : merge l2 l1 l
.

我在本书前面的 Logic.v 中对 All 的定义：

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop
:= match l with
| [] => True
| x::l' => P x /\ All P l'
end.

所讨论的定理：

Theorem merge_filter : forall (X : Set) (test: X->bool) (l l1 l2 : list X),
  merge l1 l2 l ->
  All (fun n => test n = true) l1 ->
  All (fun n => test n = false) l2 ->
  filter test l = l1.
Proof.
  intros. 
  induction H.
  - reflexivity.
  - simpl. unfold All in H0. 
  Admitted.

我想展开 H0 以获得关于列表头部的假设。

Answer 1

有一个白话关键字

Transparent

可以使不透明的定义变得透明（还有一个

Opaque

可以使定义变得不透明。因此，您可以执行

Transparent All.

来使

All

unfold

的定义变得可用。

不透明意味着你无法看到它的内部，因为你不应该依赖它的具体定义。

用

Qed.

定义的事物设置为不透明，用

Defined.

定义的事物是透明的，因此简化等可以在必要时扩展它们。

但是你应该知道为什么要让不透明的东西变得透明。
它被宣布为不透明是有原因的。