1
$\begingroup$

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?

$\endgroup$

1 Answer 1

4
$\begingroup$

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.

$\endgroup$
3
  • 4
    $\begingroup$ 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. $\endgroup$ Commented Jul 5 at 21:57
  • $\begingroup$ @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? $\endgroup$ Commented Jul 6 at 22:43
  • 1
    $\begingroup$ 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? $\endgroup$ Commented Jul 8 at 9:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.