The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

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