The Coq mailing list

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

Jeff Terrell wrote:
> So, at the risk of making myself unpopular, how would you prove the theorem 
> using tactics like intro, exists, elim, split and so on. I think if I can 
> see 
> how to solve this simple problem by these means, it will help me to solve 
> the 
> more complex problem.

Since you insist, here is a monolithic proof of your conjecture using
low-level tactics. :-)

Theorem foo:
  forall l : list Process, exists m : list Package,
  forall p : Process, In p l -> exists a : Package,
  In a m /\ PID p = AID a.
Proof.
  induction l.
    exists nil. unfold In. intros. elim H.
    destruct IHl. exists (Build_Package (PID a) :: x). simpl. intros.
    destruct H0.
      exists (Build_Package (PID a)). split.
        left. reflexivity.
        rewrite H0. reflexivity.
      destruct (H p H0). destruct H1. exists x0. split.
        right. assumption.
        assumption.
Qed.

The above is likely to be quite fragile, so you'll probably want to
replay it in the same version I used to check it: version 8.2-1,
released a few days ago.

Now contrast that with the following approach, which makes use of
auxiliary definitions and lemmas provided in the List library:

Definition p2p p := Build_Package (PID p).

Theorem bar:
  forall l : list Process, exists m : list Package,
  forall p : Process, In p l -> exists a : Package,
  In a m /\ PID p = AID a.
Proof.
  Hint Resolve in_map.
  intro l; exists (map p2p l); intro p; exists (p2p p); auto.
Qed.

You can look up the definitions of "map" and "in_map" in the library
sources to decide which approach results in a more robust and
understandable proof script. :-)

Regards,
Matthew