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_wf2 つの引数に基づいて、構築時にセマンティック整形式プロパティを適用します。後で、2 つのレコードが等しいかどうかを比較する必要があります。

私は次のことから始めました---2つの整形式は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

もちろん、「applyproof_irrelevance」はそのトリックを行いました.Coq -Clubメンバーが指摘したRequire Import ClassicalFactsように、スクリプトにupがあったため、私の場合はうまくいきませんでしたが、.Coq.Logic.ProofIrrelevance

于 2013-10-22T07:55:25.957 に答える