The Coq mailing list

[Boris Yakobowski <ml AT yakobowski.org>]

On Wed, Nov 10, 2004 at 02:52:39PM +0100, june andronick wrote:
> 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...). 

The following tactic simplifies this kind of equations, using results from
the Eqdep modules. From there, it is easy to finish the proof.

Require Eqdep.

(* Simplify an hypothesis (existS P p v1=existS P p v2) into v1=v2 *)
Ltac eq_existS  :=
match goal with H:(existS ?P ?p ?v1 = existS ?P ?p ?v2), p:?t |- _ =>
assert (v1=v2) ; 
 [ apply Eqdep.eq_dep_eq with (P:=P) ;
     elim (Eqdep.equiv_eqex_eqdep t P p p v1 v2) ; intros ; auto
 | clear H ; first [subst v1 | subst v2 | idtac] ]
end.

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 ; clear H H0 ; subst.
do 2 eq_existS ; simpl ; constructor.
injection H8 ; clear H1 H7 H8 ; intro ; subst nn0 ; do 2 eq_existS.
simpl ; constructor ; exact (IHi _ _ _ _ _ H6 H12).


> (* (by the way, I didn't manage to define listn_bin_op with Fixpoint and
> "match ... in..." like the listn_un_op definition ..........) *)

This is really difficult to do "by hand" in a fixpoint definition. In fact,
I don't think it's possible if you decompose outright one of the lists;
instead you need to recurse on the length of the lists. The problem is that
you then have to keep track of the fact that both lists have the same
length, and introducing proofs inside fixpoints is always messy.

-- 
Boris