The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Hello Everyone,

I'm new to Coq and would appreciate some help in finding a proof term for

forall l : list Process,
   exists m : list Package,
      forall p : Process,
         In p l -> exists a : Package,
            In a m /\
            PID p = AID a.

where

Record Process : Set := {PID : nat}.
Record Package : Set := {AID : nat}.

I'm attempting to prove the proposition (which represents a simple 
transformation between processes and packages) by induction over l. I think I've 
proved the base case ok, but I'm not sure how to prove the induction step. I can 
see that a suitable witness for m (see last goal) is a'::mn, where mn is a 
witness for the assumption Mn, and (AID a') = (PID p'), but I'm not sure how to 
exploit Mn. In a hand-crafted proof of the proposition, I've de-constructed Mn 
and built it up with a different value of m, i.e. a'::mn. But I'm not sure how 
to do this in Coq.

Many thanks in anticipation.

Regards,
Jeff.

Coq < Theorem T :
Coq < forall l : list Process,
Coq <    exists m : list Package,
Coq <       forall p : Process,
Coq <          In p l -> exists a : Package,
Coq <             In a m /\
Coq <             PID p = AID a.
1 subgoal

  ============================
   forall l : list Process,
   exists m : list Package,
     forall p : Process,
     In p l -> exists a : Package, In a m /\ PID p = AID a

T < intro.
1 subgoal

  l : list Process
  ============================
   exists m : list Package,
     forall p : Process,
     In p l -> exists a : Package, In a m /\ PID p = AID a

T < elim l.
2 subgoals

  l : list Process
  ============================
   exists m : list Package,
     forall p : Process,
     In p nil -> exists a : Package, In a m /\ PID p = AID a

subgoal 2 is:
 forall (a : Process) (l0 : list Process),
 (exists m : list Package,
    forall p : Process,
    In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) ->
 exists m : list Package,
   forall p : Process,
   In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0

T < exists (nil:list Package).
2 subgoals

  l : list Process
  ============================
   forall p : Process,
   In p nil -> exists a : Package, In a nil /\ PID p = AID a

subgoal 2 is:
 forall (a : Process) (l0 : list Process),
 (exists m : list Package,
    forall p : Process,
    In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) ->
 exists m : list Package,
   forall p : Process,
   In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0

T < intros.
2 subgoals

  l : list Process
  p : Process
  H : In p nil
  ============================
   exists a : Package, In a nil /\ PID p = AID a

subgoal 2 is:
 forall (a : Process) (l0 : list Process),
 (exists m : list Package,
    forall p : Process,
    In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) ->
 exists m : list Package,
   forall p : Process,
   In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0

T < exists (Build_Package (PID p)).
2 subgoals

  l : list Process
  p : Process
  H : In p nil
  ============================
   In (Build_Package (PID p)) nil /\ PID p = AID (Build_Package (PID p))

subgoal 2 is:
 forall (a : Process) (l0 : list Process),
 (exists m : list Package,
    forall p : Process,
    In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) ->
 exists m : list Package,
   forall p : Process,
   In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0

T < split.
3 subgoals

  l : list Process
  p : Process
  H : In p nil
  ============================
   In (Build_Package (PID p)) nil

subgoal 2 is:
 PID p = AID (Build_Package (PID p))
subgoal 3 is:
 forall (a : Process) (l0 : list Process),
 (exists m : list Package,
    forall p : Process,
    In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) ->
 exists m : list Package,
   forall p : Process,
   In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0

T < apply H.
2 subgoals

  l : list Process
  p : Process
  H : In p nil
  ============================
   PID p = AID (Build_Package (PID p))

subgoal 2 is:
 forall (a : Process) (l0 : list Process),
 (exists m : list Package,
    forall p : Process,
    In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) ->
 exists m : list Package,
   forall p : Process,
   In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0

T < trivial.
1 subgoal

  l : list Process
  ============================
   forall (a : Process) (l0 : list Process),
   (exists m : list Package,
      forall p : Process,
      In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) ->
   exists m : list Package,
     forall p : Process,
     In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0

T < intros p' ln.
1 subgoal

  l : list Process
  p' : Process
  ln : list Process
  ============================
   (exists m : list Package,
      forall p : Process,
      In p ln -> exists a : Package, In a m /\ PID p = AID a) ->
   exists m : list Package,
     forall p : Process,
     In p (p' :: ln) -> exists a : Package, In a m /\ PID p = AID a

T < intro Mn.
1 subgoal

  l : list Process
  p' : Process
  ln : list Process
  Mn : exists m : list Package,
         forall p : Process,
         In p ln -> exists a : Package, In a m /\ PID p = AID a
  ============================
   exists m : list Package,
     forall p : Process,
     In p (p' :: ln) -> exists a : Package, In a m /\ PID p = AID a