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 H或rewrite 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 回答