The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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