The Coq mailing list

[Pierre Casteran <casteran AT labri.u-bordeaux.fr>]

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