The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

> 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)... 
> 

When I look at the proof, I see you do a proof by induction
on your input rank i.  Because you use an inductive hypothesis to
describe the search for the ith element, I think it is more clever to
use induction on the inductive property.  So I suggest you actually
start your proof by changing slightly the statement (reordering the
quantifications and implications) and then doing
the induction on the inductive property (I prefer to keep the
variables l2 and res2 on the right, an old habit that I may explain
before the end of the message).

     Lemma ith_of_listn_bin_op :
     forall i n l1 res1,
     (ith n l1 i res1) -> forall l2 res2, (ith n l2 i res2) ->
     (ith n (listn_bin_op (S n) l1 l2) i (bin_op res1 res2)).
     Proof.   
       induction 1.
       
You see that this also provides a base case on i, and we don't
have to perform an inversion on the first statement.

       intros l2 res2 H; inversion H.

Now, why is it that inversion does not work nicely?  It is because 
ith has a dependent type and the argument l2 has its type depending
on the argument n.   In the general case for inversion, this leads
to equalities between terms that may not have the same type.  These
equalities are usually encoded as equalities between "existS" terms.

  ...
  H2 : existS (fun x : nat => listn (S x)) nn (consn nn elt0 tl0) =
       existS (fun x : nat => listn (S x)) nn l2
  H3 : elt0 = res
  ============================
   ith nn (listn_bin_op (S nn) (consn nn elt tl) l2) 0 (bin_op elt res)

You can actually rewrite with such an equality, using a tactic
that is called "dependent rewrite".  In our case we will use
"dependent rewrite <-".  It tries to rewrite simultaneously
l2 into "consn nn elt0 tl0" and nn into nn.

I did try "dependent rewrite <- H2", but this failed.  I suppose
this is because nn is also used as type index for tl, so I suggest
we generalize over tl before this rewriting step:

       generalize tl; dependent rewrite <- H2.

       intros tl1; rewrite H3; constructor.

This solves the base case.   For the recursive case, I also did
an inversion to get to this point:

  ...
  H : ith nn tl i res
  IHith : forall (l2 : listn (S nn)) (res2 : nat),
          ith nn l2 i res2 ->
          ith nn (listn_bin_op (S nn) tl l2) i (bin_op res res2)
  ...
  H' : ith (S nn) l2 (S i) res2
  ...
  H3 : ith nn tl0 i res2
  H0 : nn0 = nn
  H1 : existS (fun x : nat => listn (S x)) (S nn) (consn (S nn) elt0 tl0) =
       existS (fun x : nat => listn (S x)) (S nn) l2
  H2 : i0 = i
  H4 : res0 = res2
  ============================
   ith (S nn) (listn_bin_op (S (S nn)) (consn (S nn) elt tl) l2) 
     (S i) (bin_op res res2)

I tried a few things without making any progress.  Here the problem is
that if replace (S nn) by an arbitrary p and l2 by an arbitrary t
of type listn (S p), then the goal is not well typed, because nn
is also used for the type of of other objects in the goal.

I then decided that Iwanted to use the fact that "consn (S nn) elt tl=l2".
With this fact, the proof finishes nicely.

Now the intermediary fact is a simple consequence from H1 and a theorem
provided in the libraries : "Eqdep.inj_pair2".  Unfortunately, this
theorem is not loaded by default in the system.  The reason I found it, is
that I tried to do the proof using the "heterogeneous" equality JMeq.

This message may be redundant with Pierre Castéran's answers, but I did
try to stay very close to your development so that it may still be useful.

Yves


(* 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) .

(* .... removed the case where it worked (Yves) *)

(* 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.

 Require Export JMeq.

     Lemma ith_of_listn_bin_op :
     forall i n l1 res1,
     (ith n l1 i res1) -> forall l2 res2, (ith n l2 i res2) ->
     (ith n (listn_bin_op (S n) l1 l2) i (bin_op res1 res2)).
     Proof.   
       induction 1.
       intros l2 res H; inversion H.
       generalize tl.
       dependent rewrite <- H2; rewrite H3;intros; simpl;constructor. 

       intros l2 res2 H'; inversion H'.

       assert (H'':consn (S nn) elt0 tl0=l2).
       apply Eqdep.inj_pair2 with (1:= H1).

       rewrite <- H''.
       change (ith (S nn) (consn (S nn) (bin_op elt elt0)
                    (listn_bin_op (S nn) tl tl0)) (S i)(bin_op res res2)).

       constructor;auto.
      Qed.