Are constructors in the plain calculus of constructions disjoint and injective?
Based on this answer , it looks like the inductive calculus used in Coq has disjoint injective constructors for inductive types.
In simple construct calculus (i.e. no primitive inductive types) that uses non-specific encodings for types (e.g. ∏(Nat: *).∏(Succ: Nat → Nat).∏(Zero: Nat).Nat
), is this still true? May I know which "constructor" was used? Also, is injectivity (as in ∀a b.I a = I b → a = b
) provable in Coq with Prop or an invalid set?
source to share
(I'm not sure about all the questions you asked, so I'm making this an answer on the community wiki for others to add to it.)
Just for completeness, let's use an example boolean coding. I have also included the encodings of some of the base bindings.
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.
We cannot prove that true
and false
do not intersect in CoC; that is, the following statement is not provable:
eq false true -> False.
This is because if this statement was proved in CoC, we could prove true <> false
in Coq, and it would contradict the proof of inconsistency , which is a valid axiom to add. Here's the proof:
Section injectivity_is_not_provable.
Variable Hneq : eq false true -> False. (* suppose it 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.
source to share