Existential quantifier in coq impredicative logic (System F)

Question

I was trying to code into Coq logical connectives encoded in lambda calculus with type à la System F. Here is the bunch of code I wrote (standard things, I think)

Definition True := forall X: Prop, X -> X.

Lemma I: True.
Proof.
  unfold True. intros. apply H.
Qed.

Section s.
Variables A B: Prop.


(* conjunction *)

Definition and := forall X: Prop, (A -> B -> X) -> X.
Infix "/\" := and.

Lemma and_intro: A -> B -> A/\B.
Proof.
  intros HA HB. split.
  apply HA.
  apply HB.
Qed.

Lemma and_elim_l: A/\B -> A.
Proof.
  intros H. destruct H as [HA HB]. apply HA.
Qed.

Lemma and_elim_r: A/\B -> B.
Proof.
  intros H. destruct H as [HA HB]. apply HB.
Qed.



(* disjunction *)

Definition or := forall X:Prop, (A -> X) -> (B -> X) -> X.
Infix "\/" := or.

Lemma or_intro_l: A -> A\/B.
  intros HA. left. apply HA.
Qed.

Lemma or_elim: forall C:Prop, A \/ B -> (A -> C) -> (B -> C) -> C.
Proof.
  intros C HOR HAC HBC. destruct HOR.
    apply (HAC H).
    apply (HBC H).
Qed.


(* falsity *)

Definition False := forall Y:Prop, Y.

Lemma false_elim: False -> A.
Proof.
  unfold False. intros. apply (H A).
Qed.

End s.

Basically, I wrote down the elimination and introduction laws for conjunction, disjunction, true and false. I am not sure of having done thing correctly, but I think that things should work that way. Now I would like to define the existential quantification, but I have no idea of how to proceed. Does anyone have a suggestion?

Answer 1

Existential quantification is just a generalization of conjunction, where the type of the second component of the pair depends on the value of the first component. When there's no dependency they're equivalent:

Goal forall P1 P2 : Prop, (exists _ : P1, P2) <-> P1 /\ P2.
Proof. split. intros [H1 H2]. eauto. intros [H1 H2]. eauto. Qed.

Coq'Art has a section on impredicativity starting at page 130.

Definition ex (T1 : Type) (P1 : T1 -> Prop) : Prop :=
  forall P2 : Prop, (forall x1, P1 x1 -> P2) -> P2.

Notation "'exists' x1 .. x2 , P1" :=
  (ex (fun x1 => .. (ex (fun x2 => P1)) ..))
  (at level 200, x1 binder, right associativity,
  format "'[' 'exists' '/ ' x1 .. x2 , '/ ' P1 ']'") : type_scope.

The problem with impredicative definitions (unless I'm mistaken) is that there's no dependent elimination. It's possible prove

forall (A : Type) (P : A -> Prop) (Q : Prop),
  (forall x : A, P x -> Q) -> (exists x, P x) -> Q,

but not

 forall (A : Type) (P : A -> Prop) (Q : (exists x, P x) -> Prop),
   (forall (x : A) (H : P x), Q (ex_intro P x H)) ->
   forall H : exists x, P x, Q H