The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Hi Jeff.
If you are not afraid of the lowest level, here is the proof using only 
lambda terms:

Goal 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.
refine (fix rec (l:list Process) := _).
refine (match l as l return exists m, forall p, In p l -> (_:Prop)
        with nil => _ | p0 :: l0 => _ end).
refine (ex_intro _ nil _).
        refine (fun _ f => match f with end).
simpl.
        refine (let rec0 := rec l0 in _).
        refine (match rec0 with ex_intro m0 rec1 => _ end).
        clear rec0.
        refine (ex_intro _ (Build_Package (PID p0) :: m0) _).
        simpl.
        refine (fun p or0 => _).
        refine (match or0 with or_introl eq0 => _
                        | or_intror in0 => _ end).
                refine (ex_intro _ (Build_Package (PID p0)) _).
                refine (conj (or_introl _ (refl_equal _)) _).
                simpl.
                refine (f_equal _ (sym_eq eq0)).
        refine (match rec1 p in0 with ex_intro a1 and1 => _ end).
                refine (ex_intro _ a1 (conj
                        (or_intror _ (proj1 and1)) (proj2 and1))).
Save.


> Date: Sat, 21 Feb 2009 15:46:52 +0000
> From: Jeff Terrell 
> <jeff AT kc.com>
>
> ...how would you prove the theorem 
> using tactics like intro, exists, elim, split and so on.
>   
--
Best regards,
 Roman Beslik.