The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Fri, Feb 10, 2006 at 10:41:01AM +0100, Yves Bertot wrote:
> 
> Axiom
>   dependent_description' :
>     forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
>       (forall x:A,
>           exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
>        sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
> 

Hi Yves,

From my humble opinion, this doesn't look good. From the extraction
point of view, this amounts to say "exists f : A->B" out of nothing. 
Adding additional axioms like Classical, Extensionality,
ProofIrrelevance, doesn't change the point, since those axioms live in
Prop. And my "doesn't-look-good" opinion can probably be formalized a
bit more using realizability. 

In the meantime, another additional transformation gives you something
perfectly provable. But it is probably not what you want...

Lemma dependent_description'' :
    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
      (forall x:A,
          sigT (fun y : B x => R x y /\ (forall y':B x, R x y' -> y =
    y')))->
      sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))).
Proof.
intros.
exists (fun x => let (y,_) := X x in y).
intros.
destruct (X x); intuition.
Qed.

With this one, extraction is just the identity. By the way, in the
above proof, you don't even need the "R x y' -> y =y'" part (but you
would need it to prove that the answered function is the only one that
fits). 

Hope that helps, 

Pierre