The Coq mailing list

[Matthew Brecknell <coq-club AT brecknell.org>]

Jeff Terrell wrote:
> Unless the specification is wrong, the intention was for Y to contain a 
> subset 
> of the numbers in X, so that (X p') *wouldn't* be a valid witness for Y. 
> What am 
> I missing?

Reading between the lines, I'm wondering if you might actually have
meant to write this:

Theorem T :
forall l : list Process, exists m : list Package,
  forall p : Process, In p l -> exists a : Package,
    In a m /\
    PID p = AID a /\
    forall n : nat,
      In n (X p) /\ n > 0 <-> In n (Y a).

That is, a number is in Y if *and only if* it is in the corresponding X
and it is greater than 0. Note the double-headed arrow.

With regard to your original question about "partial witnesses": since
you're providing the proof, you must know what constraints the witness
will ultimately need to satisfy, so just construct and provide an
appropriate witness. You don't need to wait until the constraints come
to the front of the goal. However, assuming you have provided an
appropriate witness, then when those constraints do come to the front of
the goal, they should be easy to satisfy.

Here's the proof:

Require Import List Compare_dec Omega.

Record Process : Set := {PID : nat; X : list nat}.
Record Package : Set := {AID : nat; Y : list nat}.

Fixpoint gt0_filter (ns: list nat) : list nat :=
  match ns with
    | n :: r => if zerop n then gt0_filter r else n :: gt0_filter r
    | nil => nil
  end.

Definition p2p proc := Build_Package (PID proc) (gt0_filter (X proc)).

Lemma gt0_filter_In_fwd:
  forall (ns: list nat) (n: nat),
  In n ns /\ n > 0 -> In n (gt0_filter ns).
Proof.
  induction ns; simpl; intuition;
  match goal with
    | [ |- context [ if zerop ?X then ?Y else ?Z ] ]
      => destruct (zerop X)
  end;
  try (apply False_ind; omega);
  try (apply IHns);
  simpl; auto.
Qed.

Lemma gt0_filter_In_rev:
  forall (ns: list nat) (n: nat),
  In n (gt0_filter ns) -> In n ns /\ n > 0.
Proof.
  induction ns; simpl; intuition;
  match goal with
    | [ H: context [ if zerop ?X then ?Y else ?Z ] |- _ ]
      => destruct (zerop X)
  end; simpl in *; intuition;
  match goal with
    | [ H: In ?N (gt0_filter ?NS) |- _ ]
      => generalize (IHns N H); intuition
  end.
Qed.

Theorem T :
  forall l : list Process, exists m : list Package,
    forall p : Process, In p l -> exists a : Package,
      In a m /\
      PID p = AID a /\
      forall n : nat,
        In n (X p) /\ n > 0 <-> In n (Y a).
Proof.
  Hint Resolve gt0_filter_In_fwd gt0_filter_In_rev in_map.
  intro l; exists (map p2p l); intro p; exists (p2p p);
  repeat (split; simpl; auto).
Qed.