The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

It implies proof irrelevance, as shown below.

Definition distinguished(T : Type) := exists (a b : T), a <> b.

Definition proof_uninformativeness : Prop := 

  forall (P : Prop)(T : Type)(f : P -> T)(p1 p2 : P), distinguished T -> f p1 = f p2.

Inductive InjectPT (P:Prop) : Type :=

| injectpt :  P -> InjectPT P

| dummy1 : InjectPT P

| dummy2 : InjectPT P.

Lemma distinguishedInjectPT : forall P, distinguished (InjectPT P).

Proof using.

  intros ?. unfold distinguished. exists (dummy1 P), (dummy2 P).

  discriminate.

Qed.

Definition uninject (P:Prop) (ip: InjectPT P) : option P :=

match ip with

| injectpt _ p => Some p

| _ => None

end.

Lemma invertSome (A:Type) (a b: A) :

  Some a = Some b -> a= b.

Proof using.

  intros H.

  inversion H.

  reflexivity.

Qed.

 

Lemma  proof_uninformativeness_implies_proof_irrelevance:

  proof_uninformativeness

  -> forall (P : Prop) (p q : P), p = q.

Proof using.

  intros H ? ? ?.

  specialize (H P (InjectPT P) (injectpt P) p q (distinguishedInjectPT P)).

  apply (f_equal (uninject P)) in H.

  simpl in H.

  apply invertSome in H.

  assumption.

Qed.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sat, Apr 23, 2016 at 9:00 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 04/23/2016 08:41 PM, darktenaibre wrote:

Ah, that notprop predicate prevents this stupid observation though. You can certainly write something like (fun T => forall P : Prop, ~ (@eq Type P T)) which will easily block the previous proof, but it's probably unusable this way. I do not have any idea for a clever solution to this problem though.
On 04/24/2016 02:32 AM, darktenaibre wrote:

On 04/24/2016 02:21 AM, Jonathan Leivent wrote:

Definition proof_uninformativeness := forall (P : Prop)(S : Set)(f : P -> S)(p1 p2 : P), f p1 = f p2.

Hi,
If you take f:=id, isn't it just proof irrelevance ?


Lemma proof_uninformativeness_irrelevance : proof_uninformativeness -> forall (P : Prop) (p q : P), p = q.
  intros pu P; apply pu.
Qed.

Oops - my (embarrassing) mistake having Prop not be a subtype of Set. :-[

So, there would need to be some usable notprop predicate.
Hmm... maybe types having at least 2 distinguished instances are sufficient? :

Definition distinguished(T : Type) := exists (a b : T), a <> b.

Definition proof_uninformativeness := forall (P : Prop)(T : Type)(f : P -> T)(p1 p2 : P), distinguished T -> f p1 = f p2.

Is this a suitable replacement for all interesting use cases of proof irrelevance?

-- Jonathan