2

我定义了一个简单的结构：

Require Import Ensembles.

Record ConfigStructure {T:Type} : Type := mkCS {
  E: Ensemble T;
  C: Ensemble (Ensemble T);
  CS_wf : forall x y, In _ C x -> In _ x y -> In _ E y;
  rooted := In (Ensemble T) C (Empty_set T)
}.

CS_wf基于这两个参数，在构造时强制执行语义格式良好的属性。现在稍后，我需要比较两条记录是否相等——我用证明组件做什么？

我从以下内容开始---我猜这两个良构也应该出现在 lhs 上？

Lemma CS_split: forall T e1 c1 wf1 e2 c2 wf2,
e1 = e2 /\ c1 = c2 -> mkCS T e1 c1 wf1 = mkCS T e2 c2 wf2.
Proof.
intros.
destruct H as [He Hc].
destruct He; destruct Hc.
f_equal.
Abort.

这需要我：

T : Type
e1 : Ensemble T
c1 : Ensemble (Ensemble T)
wf1 : forall (x : Ensemble T) (y : T),
      In (Ensemble T) c1 x -> In T x y -> In T e1 y
wf2 : forall (x : Ensemble T) (y : T),
      In (Ensemble T) c1 x -> In T x y -> In T e1 y
============================
 wf1 = wf2

我想证明无关性也起作用了？

4

1 回答 1

1

当然，“apply proof_irrelevance”起到了作用——它只是在我的情况下不起作用，因为我的Require Import ClassicalFacts脚本中有一个 up ，而我本来需要Coq.Logic.ProofIrrelevance，正如 Coq-Club 成员指出的那样。

于 2013-10-22T07:55:25.957 回答