coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeff Terrell <jeff AT kc.com>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Simple Transformation
- Date: Sun, 22 Feb 2009 12:38:27 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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 |
- [Coq-Club] Simple Transformation, Jeff Terrell
- Re: [Coq-Club] Simple Transformation,
Matthew Brecknell
- Re: [Coq-Club] Simple Transformation,
Jeff Terrell
- Re: [Coq-Club] Simple Transformation, Luke Palmer
- Re: [Coq-Club] Simple Transformation,
Matthew Brecknell
- Re: [Coq-Club] Simple Transformation, Jeff Terrell
- Re: [Coq-Club] Simple Transformation, Adam Chlipala
- Re: [Coq-Club] Simple Transformation, Matthew Brecknell
- [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness, Adam Chlipala
- Re: [Coq-Club] Partial Witness, Jeff Terrell
- Re: [Coq-Club] Partial Witness, Adam Chlipala
- Re: [Coq-Club] Partial Witness,
Jeff Terrell
- Re: [Coq-Club] Partial Witness,
Adam Chlipala
- Re: [Coq-Club] Partial Witness, Pierre Castéran
- Re: [Coq-Club] Simple Transformation, Jeff Terrell
- Re: [Coq-Club] Simple Transformation,
Jeff Terrell
- Re: [Coq-Club] Simple Transformation,
Matthew Brecknell
- <Possible follow-ups>
- Re: [Coq-Club] Simple Transformation, Roman Beslik
Archive powered by MhonArc 2.6.16.