The Coq mailing list

[Frederic GAVA <frederic.gava AT wanadoo.fr>]

Bonsoir,

Voici quelques fonctions sur les listes (avec les entiers Z) et deux lemmes 
que je n'arrive
pas a finir...

Est-ce qu'il existe une bibliothèque de liste sur Z qui a déjà été développée 
?

Merci de votre aide (et des aides précèdentes).
Frédéric Gava.



Require TheoryList.
Require ZArith.
Require Omega.

Fixpoint Zlength [T:Set] [l:(list T)] : Z := Cases l of 
                                     nil => `0` 
                            | (cons _ m) => `(Zlength T m)+1` end.
                            

Lemma Zlength_app : (T:Set) (l1,l2:(list T)) ( (Zlength T (app l1 
l2))=`(Zlength T l1)+(Zlength T l2)`).
Intros T l1.
NewInduction l1;Simpl;Auto.
Intro l2.
Rewrite (IHl1 l2).
Auto with zarith.
Qed.

Lemma Zlength_map : (T1,T2:Set) (l:(list T1)) (f:T1->T2) (Zlength T2 (map f 
l))=(Zlength T1 l).
Intros T1 T2 l.
NewInduction l;Simpl;Intros;Auto.
Rewrite (IHl f);Auto.
Qed.

Lemma Zlength_no_nil: (T:Set) (l:(list T)) (n:Z) `0<n` -> `(Zlength T l) = n` 
-> ~(l=(nil T)).
Intro T.
NewInduction l;Simpl;Intros.
Absurd  `0 = n`;Auto with zarith.
Discriminate.
Qed.


Lemma Zlength_le_0: (T:Set) (l:(list T)) `0<=(Zlength T l)`.
Intros.
NewInduction l;Simpl;Auto with zarith.
Qed.



(* Voici la spécification *)

Inductive Znth_spec [T:Set] : (list T)->Z->T->Prop :=
  Znth_spec_O : (a:T)(l:(list T))(Znth_spec T (cons a l) `1` a)
| Znth_spec_S : (n:Z)(a,b:T)(l:(list T))
           (Znth_spec T l n a)->(Znth_spec T (cons b l) `n+1` a).
           
(* et une fonction que la réalise *)

Definition ZNth : (T:Set) (l:(list T)) (pos:Z) `1<=pos<=(Zlength T l)` 
  -> { res:T | (Znth_spec T l pos res)}.
Intros T l.  
NewInduction l;Simpl;Intros.
Absurd `1 <= pos <= 0`;Auto.
Omega.
Case (Z_eq_dec pos `1`);Intros.
Exists a.
Rewrite e.
Apply (Znth_spec_O T a l).
Assert `1 <= pos-1 <= (Zlength T l)`.
Omega.
Elim (IHl `pos-1` H0);Intros.
Exists x.
Generalize (Znth_spec_S T `pos-1` x a l p).
Assert `pos-1+1`=`pos`.
Omega.
Rewrite H1;Auto.
Defined.


(* et une fonction qu'alors j'utilise dans certaines de me spécifications *)

Definition Znth2: (T:Set) (l:(list T)) (pos:Z) `1<=pos<=(Zlength T l)` -> T.
Intros.
Generalize (ZNth T l pos H);Intro.
Inversion H0;Auto.
Defined.

(* Et voici le lemma que j'arrive pas a faire *)

Lemma Znth2_Znth_spec: (T:Set) (l:(list T)) (a:T) (n:Z) (Hyp_n:`1 <= n <= 
(Zlength T l)`) (a=(Znth2 T l n Hyp_n)) -> (Znth_spec T l n a).   


(* Et son opposée ??? (moins important, plus par curiosité) *)

Lemma Znth2_Znth_spec: (T:Set) (l:(list T)) (n:Z) (a:T) (Znth_spec T l n a) ->
( (`1 <= n <= (Zlength T l)`) /\ ( (Hyp_n:`1 <= n <= (Zlength T l)`) 
(a=(Znth2 T l n Hyp_n)))).