data _∈_ {X : Set} (x : X) : (xs : List X) → Set where
here! : {xs : List X} → x ∈ x ∷ xs
there : {xs : List X} {y : X} (pr : x ∈ xs) → x ∈ y ∷ xs
remove : {X : Set} {x : X} (xs : List X) (pr : x ∈ xs) → List X
remove (_ ∷ xs) here! = xs
remove (y ∷ xs) (there pr) = y ∷ remove xs pr
我正在尝试将上述定义从 Agda 翻译成 Coq，但遇到了困难。
Inductive Any {A : Type} (P : A -> Type) : list A -> Prop :=
| here : forall {x : A} {xs : list A}, P x -> Any P (x :: xs)
| there : forall {x : A} {xs : list A}, Any P xs -> Any P (x :: xs).
Definition In' {A : Type} (x : A) xs := Any (fun x' => x = x') xs.
Fixpoint remove {A : Type} {x : A} {l : list A} (pr : In' x l) : list A :=
match l, pr with
| [], _ => []
| _ :: ls, here _ _ => ls
| x :: ls, there _ pr => x :: remove pr
end.
Incorrect elimination of "pr0" in the inductive type "@Any":
the return type has sort "Type" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.
除了这个错误之外，如果我离开[]的情况，Coq 会要求我提供它，尽管它很荒谬。
到目前为止，我一直认为Agda和Coq是相同的语言，但前端不同，但现在我开始认为它们在引擎盖下是不同的。有没有办法在Coq中复制删除功能，如果没有，你会推荐什么替代方案？
编辑：我还想将证明保留在In和In'之间。最初我In'Type而不是Prop，但这会使以下证明因类型错误而失败。
Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
match l with
| [] ⇒ False
| x' :: l' ⇒ x' = x ∨ In x l'
end.
Theorem In_iff_In' :
forall {A : Type} (x : A) (l : list A),
In x l <-> In' x l.
Proof.
intros.
split.
- intros.
induction l.
+ inversion H.
+ simpl in H.
destruct H; subst.
* apply here. reflexivity.
* apply there. apply IHl. assumption.
- intros.
induction H.
+ left. subst. reflexivity.
+ right. assumption.
Qed.
In environment
A : Type
x : A
l : list A
The term "In' x l" has type "Type" while it is expected to have type
"Prop" (universe inconsistency).
这里的In来自SF的逻辑章节。我在阿格达中有一个鸽子洞原理的解决方案，所以我想要这个双射，以便转换为练习要求的形式。
编辑2：
Theorem remove_lemma :
forall {A} {x} {y} {l : list A} (pr : In' x l) (pr' : In' y l),
x = y / In' y (remove pr).
即使在定义In'时使用Type，我也在这个定义中完全遇到了宇宙不一致。
您需要使用信息丰富的会员证明。现在，您的Any采用Prop中的值，由于其消除的限制(请参阅您得到的错误消息)，这与公理forall (P: Prop) (x y: P), x = y一致。这意味着，如果您有一些术语依赖于类型为Prop的术语(就像remove一样)，它只需要使用这样一个术语存在的事实，而不是它具体是什么术语。通常，您不能在Prop上使用消除(通常是模式匹配)来生成除也是Prop之外的任何内容。
有三种本质上不同的In' 1 [1; 2; 1; 3; 1; 4]证明，并且，根据使用哪个证明，remove p可能是[2; 1; 4; 1; 4]、[1; 2; 3; 1; 4]或[1; 2; 1; 3; 4]。因此，输出在很大程度上取决于特定的证明。
要解决此问题，您只需将Inductive Any {A : Type} (P : A -> Type) : list A -> Prop中的Prop替换为Type.1现在我们可以消除非Prop类型，以及您对remove作品的定义。
为了回答你的编辑，我认为最大的问题是你的一些定理/定义需要In'成为一个Prop(因为它们依赖于无信息的证明)，而另一些则需要信息证明。
我认为你最好的选择是保留In'作为Type，但随后证明定理的无信息版本。在标准库中，在Coq.Init.Logic中，有一个电感型inhabited。
Inductive inhabited (A: Type): Prop :=
| inhabits: A -> inhabited A.
这需要一个类型，基本上忘记了关于其术语的任何具体内容，只记住它是否有人居住。我认为如果你简单地用inhabited (In' x l)替换In' x l，你的定理和引理是可以证明的.我能够证明你的定理的一个变体，其结论很简单In x l <-> inhabited (In' x l).您的证明大部分有效，但我不得不一步使用以下简单的引理：
Lemma inhabited_there {A: Type} {P: A -> Type} {x: A} {xs: list A}:
inhabited (Any P xs) -> inhabited (Any P (x :: xs)).
注意：即使inhabited A基本上只是A的Prop版本并且我们有A -> inhabited A，我们也不能证明一般inhabited A -> A，因为这将涉及选择任意的A元素。阿拉伯数字
我之前也建议
Set这里，但这不起作用，因为感应类型取决于A，这是Type。事实上，我相信证明助手 Lean 使用与此非常相似的东西作为其选择公理。