The Coq mailing list

[Fr�d�ric Gava <frederic.gava AT wanadoo.fr>]

Dear Coq's wizards,

 

I have two problems in my development. I give here the code and the two questions.

 

Thanks very much.
Best regards,
  Frédéric Gava.

 

Require Export Arith.
Require ZArith.
Require PolyList.
Require Omega.

 

(* number of processes = p  *)
Parameter bsp_p:unit->Z.

 

(* Good number of processes *)
Parameter good_bsp_p:`0 < (bsp_p tt)`.

 

Hints Resolve good_bsp_p.
Hints Resolve good_bsp_p : zarith.

 

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

 

(* My parallel vectors as list with the proof that the length is p *)
Record Vector [T:Set]: Set := mkVect  {
  val: (list T);
  Vect_val_cond: `(Zlength T val)=(bsp_p tt)` }.

 

(* nth elements of a list *)
Definition at_tmp: (T:Set) (l:(list T)) (pos:Z) `0<=pos<(Zlength T l)` -> T.
Intros T l. 
NewInduction l;Simpl;Intros.
Absurd `0 <= pos < 0`;Auto.
Auto with zarith.
Case (Z_eq_dec pos `0`);Intros.
Assumption.
Assert `0 <= pos-1 < (Zlength T l)`.
Auto with zarith.
Apply (IHl `pos-1` H0);Auto.
Defined.

 

(* For the vectors *)
Definition at: (T:Set) (Vector T) -> (i:Z) `0<=i<(bsp_p tt)` -> T.
Intros.
Generalize (Vect_val_cond T H);Intro.
Assert `0<=i<(Zlength T (val T H))`.
Rewrite H1;Auto.
Apply (at_tmp T (val T H) i H2).
Defined.

 

(* Discriminate a number with the length of a list *)
Definition within_bound_list: (T:Set) (l:(list T)) (i:Z) {`0<=i<(Zlength T l)`}+{~`0<=i<(Zlength T l)`}.
Intros; Case (Z_le_dec `0` i); Intros; Intuition.
Intros; Case (Z_lt_dec i (Zlength T l)); Intros; Intuition.
Defined.

 

(* Now for parallel vectors *)
Definition within_bound: (i:Z) {`0<=i<(bsp_p tt)`}+{~`0<=i<(bsp_p tt)`}.
Intros; Case (Z_le_dec `0` i); Intros; Intuition.
Intros; Case (Z_lt_dec i (bsp_p tt)); Intros; Intuition.
Defined.

 

(* My first function *)
(* It is clear and easy to see that the function do not change the length of the list l *)

 

Fixpoint put_tmp [T:Set;l1:(list Z->(option T));i:Z;l:(list Z->(option T))]: (list (Z->(option T))) :=
 Cases l of
    nil => (nil Z->(option T))
 | (cons hd tl) => (cons ([j:Z]
                            if (within_bound_list (Z->(option T)) l j) then [H1]((at_tmp (Z-> (option T)) l j H1) i)
                              else [H2](None T))
    (put_tmp T l1 `i+1` tl)) end.

 

(* But the proof ????? *)
(* i.e. for all i,j,l1,l2  the function does not change the length of the list *)

 

Lemma put_tmp2: (T:Set)(l1,l2:(list Z->(option T)))(l:(list Z->(option T)))(i,j:Z)
                (Zlength (Z->(option T)) (put_tmp T l1 i l))=(Zlength (Z->(option T)) (put_tmp T l2 j l)).
Intros.

 

?????????????

 

 

 

(* My second function *)
(* She takes two lists, and make an application components by components for
the elements of the list *)

 

Fixpoint apply_tmp [T1,T2:Set; l1:(list T1->T2); l2:(list T1)]: (list T2) :=
 Cases l1 l2 of
    nil _ => (nil T2)
 |    _ nil => (nil T2)
 | (cons hd1 tl1) (cons hd2 tl2) => (cons (hd1 hd2) (apply_tmp T1 T2 tl1 tl2)) end.

 

(* Now proof that the length of the result of the function is the length of one of the arguments *)

 

Lemma apply_tmp_tmp: (A,B:Set) (l1:(list A->B)) (l2:(list A))
    {`(Zlength B (apply_tmp A B l1 l2))=(Zlength A l2)`}+{`(Zlength B (apply_tmp A B l1 l2))=(Zlength [(A->B)] l1)`}.
Intros.

 

Double Induction l1 l2.
Error: No hypothesis l1 in current goal even after head-reduction

 

How prove it ????

 

 

 

Thanks.

 

Frédéric Gava.