The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Hello Everyone,

I was in contact with the Coq club recently to ask for help in finding the 
proof
of a simple transformation. Being a Coq novice, I was very grateful for the help 
that I received. The solution to which I could most easily relate, was the one 
by Matthew Brecknell, i.e.

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

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.

I've successfully enhanced the specification (and the proof) on the input side, 
by adding a list field to the Process record, and I'd like to do the same on the 
output side with the Package record.

I've created a rather contrived example below to show you what I mean, by adding 
a list of numbers to each record, and a conjunct to assert the relationship 
between X and Y.

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

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

The problem is that at the stage in the proof where a witness is required for m 
(see proof below), I'm unable to fully specify one, because of the dependency of 
Y on X. I'm not sure whether this makes sense, but what I appear to need is a 
way of partially specifying a witness. Is this possible?

Any help would be gratefully appreciated.

Regards,
Jeff.

Welcome to Coq 8.2 (February 2009)

Coq < Require Import List.

Coq < Record Process : Set := {PID : nat; X : list nat}.
Process is defined
Process_rect is defined
Process_ind is defined
Process_rec is defined
PID is defined
X is defined

Coq < Record Package : Set := {AID : nat; Y : list nat}.
Package is defined
Package_rect is defined
Package_ind is defined
Package_rec is defined
AID is defined
Y is defined

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

T < induction l as [| p'].
2 subgoals

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

subgoal 2 is:
 exists m : list Package,
   forall p : Process,
   In p (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))

T < exists nil.
2 subgoals

  ============================
   forall p : Process,
   In p nil ->
   exists a : Package,
     In a nil /\
     PID p = AID a /\ (forall n : nat, In n (X p) -> n > 0 -> In n (Y a))

subgoal 2 is:
 exists m : list Package,
   forall p : Process,
   In p (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))

T < intros.
2 subgoals

  p : Process
  H : In p nil
  ============================
   exists a : Package,
     In a nil /\
     PID p = AID a /\ (forall n : nat, In n (X p) -> n > 0 -> In n (Y a))

subgoal 2 is:
 exists m : list Package,
   forall p : Process,
   In p (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))

T < elim H.
1 subgoal

  p' : Process
  l : list Process
  IHl : 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))
  ============================
   exists m : list Package,
     forall p : Process,
     In p (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))

T < destruct IHl as [mw].
1 subgoal

  p' : Process
  l : list Process
  mw : list Package
  H : forall p : Process,
      In p l ->
      exists a : Package,
        In a mw /\
        PID p = AID a /\ (forall n : nat, In n (X p) -> n > 0 -> In n (Y a))
  ============================
   exists m : list Package,
     forall p : Process,
     In p (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))

T < exists (Build_Package (PID p') ??????? :: mw).