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

问题描述 投票:0回答:2

我目前正在解决软件基础问题,并在 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 以获得关于列表头部的假设。

coq
2个回答
0
投票

有一个白话关键字

Transparent
可以使不透明的定义变得透明(还有一个
Opaque
可以使定义变得不透明。因此,您可以执行
Transparent All.
来使
All
unfold
的定义变得可用。

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

Qed.
定义的事物设置为不透明,用
Defined.
定义的事物是透明的,因此简化等可以在必要时扩展它们。

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


0
投票

这是构建过程中的问题。重建项目修复了它。

© www.soinside.com 2019 - 2024. All rights reserved.