The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Matthew,

Thank you very, very much for the low-level proof; it was incredibly helpful. Without wishing to push my luck too far, I wonder if you'd mind clarifying a few points regarding the proof. Please see below.

Coq < Record Process : Set := {PID : nat}.
...

Coq < Record Package : Set := {AID : nat}.
...

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 < induction l.
2 subgoals

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

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

Is it possible to configure Coq so that the assumptions underlying all goals are displayed at each step? For example, the assumptions underlying subgoal 2 do appear later, but only when subgoal 2 becomes the current goal.

T < exists nil.
2 subgoals

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

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

Interestingly, any list of packages would work, not only nil. Given that the specification defines a transformation between lists of processes and lists of packages, one would intuitively expect an empty list of processes to be mapped to an empty list of packages. However, there's nothing in the specification to enforce this, which suggests that the specification lacks precision. I presume the alternative method of proof (using the map function) accounts for this.

T < unfold In.
2 subgoals

  ============================
   forall p : Process, False -> exists a : Package, False /\ PID p = AID a

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

T < intros.
2 subgoals

  p : Process
  H : False
  ============================
   exists a : Package, False /\ PID p = AID a

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

T < elim H.
1 subgoal

  a : 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
  ============================
   exists m : list Package,
     forall p : Process,
     In p (a :: l) -> exists a0 : Package, In a0 m /\ PID p = AID a0

Is it possible to specify the name 'a' above (which appears to have come from the induction step at the beginning of the proof) and the name 'x' below (which is a witness of the existential quantification above)?

T < destruct IHl.
1 subgoal

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

T < exists (Build_Package (PID a) :: x).
1 subgoal

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

T < simpl.
1 subgoal

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

Could you explain the difference between simpl and (a possible alternative) unfold In in this context. Both appear to do a similar sort of thing (although one is more concise than the other), and both work.

That's it. Thanks once again.

Regards,
Jeff.

T < intros.
1 subgoal

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : a = p \/ In p l
  ============================
   exists a0 : Package,
     (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < destruct H0.
2 subgoals

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : a = p
  ============================
   exists a0 : Package,
     (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

subgoal 2 is:
 exists a0 : Package,
   (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

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

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : a = p
  ============================
   (Build_Package (PID a) = Build_Package (PID a) \/
    In (Build_Package (PID a)) x) /\ PID p = AID (Build_Package (PID a))

subgoal 2 is:
 exists a0 : Package,
   (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < split.
3 subgoals

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : a = p
  ============================
   Build_Package (PID a) = Build_Package (PID a) \/
   In (Build_Package (PID a)) x

subgoal 2 is:
 PID p = AID (Build_Package (PID a))
subgoal 3 is:
 exists a0 : Package,
   (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < left.
3 subgoals

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : a = p
  ============================
   Build_Package (PID a) = Build_Package (PID a)

subgoal 2 is:
 PID p = AID (Build_Package (PID a))
subgoal 3 is:
 exists a0 : Package,
   (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < reflexivity.
2 subgoals

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : a = p
  ============================
   PID p = AID (Build_Package (PID a))

subgoal 2 is:
 exists a0 : Package,
   (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < rewrite H0.
2 subgoals

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : a = p
  ============================
   PID p = AID (Build_Package (PID p))

subgoal 2 is:
 exists a0 : Package,
   (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < reflexivity.
1 subgoal

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : In p l
  ============================
   exists a0 : Package,
     (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < destruct (H p H0).
1 subgoal

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : In p l
  x0 : Package
  H1 : In x0 x /\ PID p = AID x0
  ============================
   exists a0 : Package,
     (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < destruct H1.
1 subgoal

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : In p l
  x0 : Package
  H1 : In x0 x
  H2 : PID p = AID x0
  ============================
   exists a0 : Package,
     (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0

T < exists x0.
1 subgoal

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : In p l
  x0 : Package
  H1 : In x0 x
  H2 : PID p = AID x0
  ============================
   (Build_Package (PID a) = x0 \/ In x0 x) /\ PID p = AID x0

T < split.
2 subgoals

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : In p l
  x0 : Package
  H1 : In x0 x
  H2 : PID p = AID x0
  ============================
   Build_Package (PID a) = x0 \/ In x0 x

subgoal 2 is:
 PID p = AID x0

T < right.
2 subgoals

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : In p l
  x0 : Package
  H1 : In x0 x
  H2 : PID p = AID x0
  ============================
   In x0 x

subgoal 2 is:
 PID p = AID x0

T < assumption.
1 subgoal

  a : Process
  l : list Process
  x : list Package
  H : forall p : Process,
      In p l -> exists a : Package, In a x /\ PID p = AID a
  p : Process
  H0 : In p l
  x0 : Package
  H1 : In x0 x
  H2 : PID p = AID x0
  ============================
   PID p = AID x0

T < assumption.
Proof completed.

T < Qed.
induction l.
 exists nil.
 unfold In in |- *.
 intros.
 elim H.

 destruct IHl.
 exists (Build_Package (PID a) :: x).
 simpl in |- *.
 intros.
 destruct H0.
  exists (Build_Package (PID a)).
  split.
   left.
   reflexivity.

   rewrite H0 in |- *.
   reflexivity.

  destruct (H p H0).
  destruct H1.
  exists x0.
  split.
   right.
   assumption.

   assumption.

T is defined

Coq < Print T.
T =
fun l : list Process =>
list_ind
  (fun l0 : list Process =>
   exists m : list Package,
     forall p : Process,
     In p l0 -> exists a : Package, In a m /\ PID p = AID a)
  (ex_intro
     (fun m : list Package =>
      forall p : Process,
      In p nil -> exists a : Package, In a m /\ PID p = AID a) nil
     (fun (p : Process) (H : False) =>
      False_ind (exists a : Package, False /\ PID p = AID a) H))
  (fun (a : Process) (l0 : list Process)
     (IHl : exists m : list Package,
              forall p : Process,
              In p l0 -> exists a0 : Package, In a0 m /\ PID p = AID a0) =>
   match IHl with
   | ex_intro x H =>
       ex_intro
         (fun m : list Package =>
          forall p : Process,
          In p (a :: l0) -> exists a0 : Package, In a0 m /\ PID p = AID a0)
         (Build_Package (PID a) :: x)
         (fun (p : Process) (H0 : a = p \/ In p l0) =>
          match H0 with
          | or_introl H1 =>
              ex_intro
                (fun a0 : Package =>
                 (Build_Package (PID a) = a0 \/ In a0 x) /\ PID p = AID a0)
                (Build_Package (PID a))
                (conj
                   (or_introl (In (Build_Package (PID a)) x)
                      (refl_equal (Build_Package (PID a))))
                   (eq_ind_r
                      (fun a0 : Process =>
                       PID p = AID (Build_Package (PID a0)))
                      (refl_equal (AID (Build_Package (PID p)))) H1))
          | or_intror H1 =>
              let e := H p H1 in
              match e with
              | ex_intro x0 (conj H3 H4) =>
                  ex_intro
                    (fun a0 : Package =>
                     (Build_Package (PID a) = a0 \/ In a0 x) /\
                     PID p = AID a0) x0
                    (conj (or_intror (Build_Package (PID a) = x0) H3) H4)
              end
          end)
   end) l
     : forall l : list Process,
       exists m : list Package,
         forall p : Process,
         In p l -> exists a : Package, In a m /\ PID p = AID a

Argument scope is [list_scope]

Coq <


 

Matthew Brecknell wrote:

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


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