# Prove that a function's result cannot dependent on Prop-valued parameters in Coq

Consider the following function elem and the lemma that the result of elem does not depend on the proof of l <> nil.

Program Definition elem {A: Type} (l: list A) (nn: l <> nil): A :=
match l with
| nil => _
| (a::_) => a
end.

Lemma elem_proof_irrelevant: forall A (l: list A) nn1 nn2, elem l nn1 = elem l nn2.
Proof.
intros. destruct l; [congruence | now unfold elem].
Qed.


My understanding of universes is very limited, but I believe that, in Coq, you cannot define something in Set whose value depends on something in Prop. At least, I believe that the result of elem cannot depend on nn for universe-related reasons.

So is there a more general way to prove elem_proof_irrelevant - i.e. that elem only depends on its first parameter - that does not inspect elem and would work on arbitrary functions, without assuming proof_irrelevance or other axioms?

Short answer: no. More precisely, if you assume that any function from a proposition to a type does not depend on its arguments, then you can prove proof irrelevance:

Axiom fun_irrel : forall (P : Prop) (A : Type) (f : P -> A) (p q : P), f p = f q.

Lemma proof_irrel (P : Prop) (p q : P) : p = q.
Proof.
apply (fun_irrel P P (fun x => x)). (* uses cumulativity Prop <= Type *)
Qed.

(* Let's start again, without using cumulativity this time *)

Inductive Box (P : Prop) : Type := | box : P -> Box P.

Arguments box {_} _.

Definition unbox {P} : Box P -> P := fun b => match b with box p => p end.

Lemma proof_irrel' (P : Prop) (p q : P) : p = q.
Proof.
assert (box p = box q) as e by apply fun_irrel.
change (unbox (box p) = unbox (box q)).
now rewrite e.
Qed.


And conversely, proof irrelevance entails fun_irrel. Obviously, just like you can prove proof irrelevance for certain propositions, you can prove instances of fun_irrel for specific functions, as in your case. But it will not, in general, be possible.

• If you're willing to drop the condition that the proof cannot inspect the term, then I believe you can prove by parametricity that a Coq term cannot depend on an argument living in Prop in a systematic way. This proof would be non-uniform, i.e. the process assigning to a given term its parametricity proof would not be a Coq function but a meta-theoretical translation. The resulting proof would be internal nonetheless, i.e. a vanilla Coq term. The notion of "to depend on" would be defined by the parametricity translation itself. I have to define this properly to check it actually works. Commented Jul 5 at 21:57
• @Pierre-MariePédrot I would be very keen on seeing such a systematic way of carrying out this proof. Maybe you can post it as an answer once you come up with something? Commented Jul 6 at 22:43
• I would be surprised if you managed to do this, as I don't think you can internally prove that the result of cast : bool = bool -> bool -> bool does not depend on its argument, since the HoTT models disprove it? Commented Jul 8 at 9:04