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

Question

Based on this answer, it looks like the calculus of inductive constructions, as used in Coq, has disjoint, injective constructors for inductive types.

In the plain calculus of constructions (i.e., without primitive inductive types), which uses impredicative encodings for types (e.g., ∏(Nat: *).∏(Succ: Nat → Nat).∏(Zero: Nat).Nat), is this still true? Can I always find out which "constructor" was used? Also, is injectivity (as in ∀a b.I a = I b → a = b) provable in Coq with Prop or impredicative Set?

This seems to cause trouble in Idris.

score 4 · Accepted Answer · edited May 03 '17 at 19:09

4

(I am not sure about all the points that you asked, so I am making this answer a community wiki, so that others can add to it.)

Just for completeness, let's use an impredicative encoding of the Booleans as an example. I also included the encodings of some basic connectives.

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 are disjoint in CoC; that is, the following statement is not provable:

eq false true -> False.

This is because, if this statement were provable in CoC, we would be able to prove true <> false in Coq, and this would contradict proof irrelevance, which is a valid axiom to add. Here is a proof:

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.

edited May 03 '17 at 19:09

Anton Trunov

15,074
2
23
43

answered May 03 '17 at 15:49

Arthur Azevedo De Amorim

23,012
3
33
39

Did you mean `eq false true`? Also, could you elaborate a little further on how that statement would lead to `true <> false`? – paulotorrens May 03 '17 at 16:06
1

@paulotorrens Just added a proof. – Arthur Azevedo De Amorim May 03 '17 at 16:40
2

I think the Church bool should rather use impredicative Set. – András Kovács May 03 '17 at 16:47
2

The reference I see cited for `0 != 1` in CoC is "A Normalization Proof for an Impredicative Type System with Large Elimination over Integers, B. Werner" but I don't have lib access now. – ejgallego May 03 '17 at 17:01
1

That paper is [here](http://www.cse.chalmers.se/research/group/logic/Types/proc92.ps), p. 341. – Anton Trunov May 03 '17 at 17:23

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

1 Answers1

Linked