简单的结构演算中的构造函数是不相交和单射的吗？

Question

，看起来像 Coq 中使用的归纳结构的演算，具有用于归纳类型的不相交的内射构造子。

在简单的结构演算中（即没有原始归纳类型），它对类型使用非谓语编码（例如，∏(Nat: *).∏(Succ: Nat → Nat).∏(Zero: Nat).Nat），这仍然是正确的吗？我总能找出使用了哪个 "constructor" 吗？此外，单射性（如 ∀a b.I a = I b → a = b）是否可以在 Coq 中用 Prop 或 impredicative Set 证明？

This seems to cause trouble in Idris.

Answer 1

（我不确定你问的所有要点，所以我把这个答案做成一个社区维基，以便其他人可以添加到它。）

为了完整起见，我们以布尔值的谓词编码为例。我还包括了一些基本连接词的编码。

Definition bool : Prop := forall (A : Prop), A -> A -> A.

Definition false : bool := fun A _ Hf => Hf.

Definition true : bool := fun A Ht _ => Ht. 

Definition eq (n m : bool) : Prop :=
  forall (P : bool -> Prop), P n -> P m.

Definition False : Prop := forall (A : Prop), A.

我们无法证明true和false在CoC中是不相交的；也就是说，以下陈述不可证明：

eq false true -> False.

这是因为，如果这个陈述在 CoC 中是可证明的，我们将能够在 Coq 中证明 true <> false，而这将与 proof irrelevance 相矛盾，这是要添加的有效公理。这是一个证明：

Section injectivity_is_not_provable.

  Variable Hneq : eq false true -> False.   (* suppose it's provable in CoC *)

  Lemma injectivity : false <> true.
  Proof.
  intros Heq.
  rewrite Heq in Hneq.
  now apply (Hneq (fun P x => x)).
  Qed.

  Require Import Coq.Logic.ProofIrrelevance.
  Fact contradiction : Logic.False.
  Proof.
  pose proof (proof_irrelevance bool false true) as H.
  apply (injectivity H).
  Qed.

End injectivity_is_not_provable.

简单的结构演算中的构造函数是不相交和单射的吗？

Are constructors in the plain calculus of constructions disjoint and injective?

functional-programming

coq

dependent-type