Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proof uninformativeness vs. proof irrelevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof uninformativeness vs. proof irrelevance


Chronological Thread 
  • From: Gabriel Scherer <gabriel.scherer AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] proof uninformativeness vs. proof irrelevance
  • Date: Sat, 23 Apr 2016 22:39:23 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-ig0-f180.google.com
  • Ironport-phdr: 9a23:jLjdKRKBcg/qIHB799mcpTZWNBhigK39O0sv0rFitYgULfXxwZ3uMQTl6Ol3ixeRBMOAu6IC1LCd6fmwEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35TxiLr5ocSDKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgyWrlAYT29exhFPGk3O6Azwdpb3qCrz8ORnjnq0J8rzGJ89Uy6j4qMjcxTohT0KLXZt/2jdkM19iORAqxKsvRFl64HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==

f is injective iff (f p = f q) implies (p = q). This is compatible with proof-irrelevance. In particular, all functions whose domain is in a proof-irrelevant Prop are injective.

On Sat, Apr 23, 2016 at 10:10 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:
Sigh... there's got to be a version that "works" - that captures Coq's uninformative Prop concept, yet is weaker than proof irrelevance.  Is it enough to restrict T to bool? :

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

What I'm trying to do is to work in a context where proof irrelevance is inconsistent (because I need injectivity of some props), yet one can still have its benefits.  So, I would like to keep proofs relevant to other proofs, but not to non-Prop types somehow...

-- Jonathan


On 04/23/2016 09:55 PM, Abhishek Anand wrote:
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








Archive powered by MHonArc 2.6.18.

Top of Page