The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

I'm probably doing something that isn't allowed, but here goes:
somewhere in a proof, I get the following subgoal (this is a reduced,
self-contained example):

1 subgoal
list : Set
P : list -> Prop
Q : list -> Prop
x0 : list
p0 : P x0 /\ Q x0
H : P x0
H1 : Qc (exist (fun l : list => P l) x0 H)
______________________________________(1/1)
Qc
  (and_rec (fun (H0 : P x0) (_ : Q x0) => exist (fun l : list => P l) x0 H0)
     p0)

I should think that this should be trivial to prove, since I should think that
the and_rec can be reduced to its result (in which case the proof can be
completed by assumption H1); but calling simpl doesn't do anything.  

The problem is (I think) is that and_rec can only be reduced if the
argument has the form (conj _ _). Now, p0 does not have that form, but
the type of p0 is (P x0 /\ Q x0). Given the definition of /\:

Inductive and (A : Prop) (B : Prop) : Prop :=  conj : A -> B -> A /\ B

I would think if if I have a proof of type A /\ B, I must be able to
show that the structure of that proof must be conj _ _; and hence, I
should be able to simplify my and_rec, above. But I don't seem to be
able to prove the following lemma:

Lemma and_conj : forall (A B:Prop) (pf : A /\ B), 
  exists pa : A, exists pb : B, pf = conj pa pb.

Is there a good reason why I can't prove that, other than the fact that
I'm still very much a beginner with Coq?

Thanks!

Edsko