在类型级别重写

Question

我有以下证明状态：

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 指的是值而不是类型。

是否有等同于 rewrite 的类型？

这是我要完成的定理（包含所有必要的定义）。

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.

Answer 1

这不是一般问题的答案，但 subst 可以解决这个问题。证明可以完成如下：

subst f.
apply f_equal. apply proof_irrelevance.

在类型级别重写

Rewriting at the type level

coq

coq-tactic