The Coq mailing list

[Marko Doko <m.doko AT hw.ac.uk>]

Hi Mukesh,

take a look at this:

Theorem go_app_stated_nicely:
  ∀ (xs : list A) (z : A),
  let (ys, zs) := go z xs in Permutation (ys ++ zs) xs.
Proof.
  intros xs z; induction xs; intros; simpl; [trivial | ].
  destruct (go z xs) as [ys zs].
  destruct (R a z); simpl; eauto using Permutation_cons, Permutation_sym, 
Permutation_cons_app.
Qed.

Theorem go_app :
    ∀ (xs ys zs : list A) (z : A),
    In z xs ->
    (ys, zs) = go z xs -> Permutation (ys ++ zs) xs.
Proof.
 intros xs ys zs z IN EQ.
 specialize (go_app_stated_nicely xs z).
 rewrite <- EQ.
 trivial.
Qed.




Best,
--
Marko
________________________________

Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With 
campuses and students across the entire globe we span the world, delivering 
innovation and educational excellence in business, engineering, design and 
the physical, social and life sciences. This email is generated from the 
Heriot-Watt University Group, which includes:

 1.  Heriot-Watt University, a Scottish charity registered under number 
SC000278
 2.  Heriot- Watt Services Limited (Oriam), Scotland's national performance 
centre for sport. Heriot-Watt Services Limited is a private limited company 
registered is Scotland with registered number SC271030 and registered office at 
Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, 
EH14 4AS.

The contents (including any attachments) are confidential. If you are not the 
intended recipient of this e-mail, any disclosure, copying, distribution or 
use of its contents is strictly prohibited, and you should please notify the 
sender immediately and then delete it (including any attachments) from your 
system.