The Coq mailing list

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

Your proof essentially shows that Erasable_inj implies proof relevance of Foo, and is thus inconsistent with assuming proof irrelevance of Foo :

(No was a Yes? Sorry if I am misunderstanding something.)

Inductive Erasable(A : Set) : Prop :=

  erasable: A -> Erasable A.

Arguments erasable [A] _.

Axiom Erasable_inj : forall {A : Set}{a b : A}, erasable a=erasable b -> a=b.

Inductive Foo : Prop :=

  foo: nat -> Foo.

Definition foo2erasable(f : Foo) : Erasable nat :=

  match f with

    | foo x => erasable x

  end.

Lemma FooRelevant : foo 1 <> foo 2. 

Proof.

  intros H.  apply f_equal with (f := foo2erasable) in H.

  simpl in H.

  apply Erasable_inj in H.

  discriminate H.

Qed.

Do you need to assume Erasable_inj in its full generality? or just some specific instances for some sets?

If only certain instances suffice, and if there was a way to easily understand the implications of such instances, it may still be possible to safely have some instances of proof irrelevance.

More formally, if we assume  @Erasable_inj A for some set A, is there are a simple characterization of the Props (members of sort Prop) whose proof relevance become implied?

-- Abhishek

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

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

On 04/23/2016 10:35 PM, Abhishek Anand wrote:

Do you need to have proof irrelevance and proof relevance for the same
Prop? If so, I would like to understand your use case.

No.  The proof-relevance I have is limited to injectivity of a single Prop constructor with a single Set arg.  Other than that one, I'd like to have proof irrelevance elsewhere, however...

I guess it is safe to assume instances of proof relevance for some Props,
and to simultaneously assume instances of proof irrelevance of some *other*
Props.

I have a proof that injectivity of any Prop constructor over a non-Prop arg combined with irrelevance of any other Prop constructor that has a non-Prop arg is inconsistent.  See : https://github.com/jonleivent/mindless-coding/blob/master/erasable_relevance.v

Anyway, I fear that the trick you used in your proof - of a non-Prop constructor with a single Prop arg, combined with the a-proiri injectivity in Coq of all constructors over all args, means that there isn't a very useful weakening of proof irrelevance, since the constructor use cases for proof irrelevance are probably the most important.

Or, to say this differently, Coq could only support a useful weakened version of proof irrelevance if it didn't have a-priori injectivity over Prop fields in non-Prop constructors.

Thanks anyway,
-- Jonathan.

Also, if the Props for which you want to assume proof irrelevance are
decidable, you can use them in a proof irrelevant way:
Definition makeIrrelevant (P:Prop) `{Decidable
<http://www.cs.cornell.edu/~aa755/ROSCoq/coqdocnew/MathClasses.misc.decision.html#Decision>
P} := if (decide P) then True else False.
(I originally learnt about this trick from
http://cstheory.stackexchange.com/questions/18962/formalizing-the-theory-of-finite-sets-in-type-theory/18967#18967
)


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