2

私は次の証明状態を持っています:

1 subgoals
U : Type
X : Ensemble U
Y : Ensemble U
f : U -> U
g : U -> U
pF : proof_dom_cod U X Y f
pG : proof_dom_cod U X Y g
fg : f = g
H : proof_dom_cod U X Y g = proof_dom_cod U X Y f
______________________________________(1/1)
createarrow U X Y f pF = createarrow U X Y g pG

だから私はしたいです

assert (pF = pG)

そして、それを証明するために証拠の無関連性を使用します。残念ながら、pF = pG型が同じであることはわかっていますが、型が異なるため有効ではありませんH。rewrite Horrewrite H in pFが一致の失敗につながると言ってin pFいるのは、型ではなく値を参照しているためだと思います。

rewritefor タイプに相当するものはありますか？

これが私が完成させようとしている定理です（必要なすべての定義を含む）。

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Logic.Classical_Prop.


Definition proof_dom_cod 
(U : Type) (X Y : Ensemble U) (f : U -> U) : Prop
    := forall x : U, In U X x -> In U Y (f x).

Inductive setarrow (U : Type) (X Y : Ensemble U) : Type
        :=
    | createarrow (f : U -> U) (proof : proof_dom_cod U X Y f).

Lemma eq_setarrow
    (U : Type) (X Y : Ensemble U) (f g : U -> U) (pF : proof_dom_cod U X Y f) (pG : proof_dom_cod U X Y g)
        : (f = g -> (createarrow U X Y f pF = createarrow U X Y g pG)).
    intros fg.
    assert (proof_dom_cod U X Y g = proof_dom_cod U X Y f).
        rewrite fg.
        trivial.
Qed.
4

1 に答える 1

3

これは一般的な質問に対する回答ではありませんが、ここsubstで作業を行います。証明は次のように終了できます。

subst f.
apply f_equal. apply proof_irrelevance.
于 2016-05-22T19:31:06.803 に答える