The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Matthew,

Matthew Brecknell wrote:
> 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.

What I was trying to do was to come up with an example in which a witness 
*couldn't* be constructed from constraints in the current goal, because I was 
keen to understand how to deal with such a situation. Unfortunately, I messed up 
the theorem and that led to some confusion; I'm sorry to everyone for that.

I'm grateful to Adam for pointing out something that just didn't occur to me, 
and that is that as *I'd* defined the theorem, any list of numbers could serve 
as a witness for Y, provided that it included the positive numbers in X. And one 
such witness, of course, is (X p').

Your theorem above tie things down quite nicely - many thanks for that. But I 
was also wondering (for curiosity sake more than anything else) whether <-> 
could be replaced by ->, if the implicand constrained Y to be the smallest 
possible list. If that were possible, (X p') wouldn't then be a witness.

> 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.

This is exactly the sort of example that I was looking for. The problem it 
solves is the one that prompted me to ask about partial witnesses in the first 
place. Many thanks for your help.

Regards,
Jeff.

> 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.
>
>
>
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club