The Coq mailing list

[june andronick <jandronick AT axalto.com>]

Hello,

I have some difficulties while using dependant types, more precisely when 
defining inductive predicate and doing inversion on them. An hypothesis of 
the form:
      H : existS (fun x : T1 => T2) y v1 = existS (fun x : T1 => T2) y v2
appears and sometimes v2 as been changed into v1 in my goal (after 
simplification of projs2(existS ...)), but sometimes no and I cannot deduce 
anything like v1=v2 (injection doesn't work...). And in my goal I have a 
"match...in...return...with...end" form that I don't really understand (I 
don't really understand the "in..." part)... 

Since I'm not very familiar with dependant types, I cannot say whether it 
comes from my definitions or if it's a theoretical problem ... I would be 
grateful if someone can give me some indications.
Hereafter is the whole problem (sorry if it's a bit long, I didn't manage to 
explain it in a shorter manner)

Thanks in advance
June Andronick
--------------------------------------------------------------
(* I have the following definition of lists of size n : *)
     Inductive listn : nat -> Set :=
       | niln : listn 0
       | consn : forall n:nat, nat -> listn n -> listn (S n).

(* I defined a predicate for the ith element of the list : *)
     Inductive ith : 
        forall (n:nat), listn (S n) -> nat ->  nat -> Prop :=
        | IthBitFirst : forall (nn:nat) (elt:nat) (tl:listn nn),
                        (ith nn (consn nn elt tl) 0 elt) 
        | IthBitNotFirst : 
            forall (nn:nat) (elt:nat) (tl:listn (S nn)) (i:nat) (res:nat),
            (ith nn tl i res) -> 
            (ith (S nn) (consn (S nn) elt tl) (S i) res) .

(* The case where it works : *)
     Parameter un_op : nat -> nat.
     Fixpoint listn_un_op (n:nat)(l:listn n){struct l}: listn n :=
       match l in listn n return listn n with
        | niln => niln
        | consn n' a y => consn n' (un_op a) (listn_un_op n' y)
        end.
        
     Lemma ith_of_listn_un_op :
     forall i n l res,
     (ith n l i res) ->
     (ith n (listn_un_op (S n) l) i (un_op res)).
     Proof.   
       induction i; intros; inversion H; simpl; subst; constructor. 
       apply (IHi nn tl res); auto.
     Qed.

(* The case where it doesn't work *)
(* (by the way, I didn't manage to define listn_bin_op with Fixpoint and 
"match ... in..." like the listn_un_op definition ..........) *)

     Parameter bin_op : nat -> nat -> nat.
     Definition listn_bin_op : 
          forall (n:nat), listn n -> listn n -> listn n.
     Proof.
       induction n as [|n hyp_rec_n]; intros l1 l2. exact niln.
       inversion l1 as [|nn a1 tl1]; inversion l2 as [|nnn a2 tl2]; subst.
       exact (consn n (bin_op a1 a2) (hyp_rec_n tl1 tl2)).
     Defined.

     Lemma ith_of_listn_bin_op :
     forall i n l1 l2 res1 res2,
     (ith n l1 i res1) -> (ith n l2 i res2) ->
     (ith n (listn_bin_op (S n) l1 l2) i (bin_op res1 res2)).
     Proof.   
       induction i; intros. 
       inversion H; inversion H0; simpl; subst.  
        ???? ..........