在类型级别重写 [英] Rewriting at the type level

问题描述

我有以下证明状态：

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 。我说重写H 或在pF中重写H 导致匹配失败，我认为是因为 pF 是指值而不是类型。

and then use proof irrelevance to prove that. Unfortunately, pF = pG is not valid because they have different types, even though I know the types to be the same because H. saying rewrite H or rewrite H in pF leads to a match failure, I assume because in pF refers to the value not the type.

是否有等同于 rewrite 的值

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

Here's the theorem I'm trying to complete (with all necessary definitions).

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.

推荐答案

这不是一般问题的答案，但在这里 subst 完成了工作。证明可以如下完成：

This is not an answer to the general question, but here subst does the work. The proof can be finished as follows:

subst f.
apply f_equal. apply proof_irrelevance.

这篇关于在类型级别重写的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！