The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Yes there is a systematic way to do that.
The trick is to replace the fixpoint T with the provably equal term 
  Cases T of c1 => c1 | ... | cn => cn end
then iota reduction applies

In your case:

 Lemma LList_decompose : 
  (l:LList)l = (Cases l of LNil => LNil | (LCons a l) => (LCons a l) end).
Destruct l; Trivial.
Save.

 Lemma repeat_unfold : (a:A)(repeat a)=(LCons a (repeat a)).
 Proof.
  Intro a; Apply trans_equal with 1:=(LList_decompose (repeat a)); Trivial.
 Qed.

This scheme is explained in papers by E. Gimenez on co-inductive type,
see for instance the Tutorial on recursive types

Christine

Pierre Casteran writes:
 > Hello,
 > 
 > 
 > Hello,
 >   
 >  In the framework of potentially infinite lists, I proved the
 > theorem (repeat a)=(LCons a (repeat a)) ; the proof uses some
 > case analysis ; is there a way (reewriting, specialized tactics ...) to
 > do it more simply ?
 > 
 > Pierre
 > 
 > 
 > Section LLists.
 >  Set Implicit Arguments.
 >  Variable A : Set.
 > 
 >  CoInductive Set LList :=
 >     LNil : LList
 >    |LCons : A -> LList -> LList.
 > 
 > 
 >  Definition decompose : LList -> (option (A*LList)) 
 >                       := [l:LList]Case l of (None ?) 
 >                                             [a:A;l':LList]
 >                                            (Some ? (a,l'))
 >                                  end.
 > 
 > 
 >  CoFixpoint repeat : A->LList :=
 >    [a:A](LCons a (repeat a)).
 > 
 >  Lemma repeat_decompose : (a:A)(decompose (repeat a))=
 >                                 (Some ? (a,(repeat a))).
 >  Proof.
 >   Intro;Simpl;Auto.
 >  Qed.
 > 
 >  Lemma decompose_eq_1 : (l : LList)(a:A)(l':LList)
 >                        (decompose l)=(Some ? (a,l')) ->
 >                        l=(LCons a l').
 >  Proof.
 >   Intros l a l';Case l;Simpl.
 >   Intro H;Discriminate H.
 >   Intros a0 l0 H0;Injection H0;Auto.
 >   Intros H1 H2;Rewrite H1;Rewrite H2;Auto.
 >  Qed.
 > 
 >  Lemma repeat_unfold : (a:A)(repeat a)=(LCons a (repeat a)).
 >  Proof.
 >   Intro a;Apply decompose_eq_1.
 >   Apply repeat_decompose.
 >  Qed.
 > 
 > 
 > -- 
 > Pierre Casteran,
 > LaBRI, Universite Bordeaux-I      |   
 > 351 Cours de la Liberation        |   
 > F-33405 TALENCE Cedex             |   
 > France                            |   
 > tel : (+ 33) 5 56 84 69 31
 > fax : (+ 33) 5 56 84 66 69
 > email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white
 > space)
 > www: http://dept-info.labri.u-bordeaux.fr/~casteran

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84