The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Hello all,

I stumbled upon a strange (to me) problem with dependent destruction (or
dependent induction for that matter) where it gets stuck in a cycle.

I tracked down the problem to the repeated invocation of
simplify_one_dep_elim, which keeps generating the same simple equality.

The context is pretty involved, so I will try to simplify what happens
here and provide more details if they are asked for. For lack of
creativity, I will simply use _ wherever I leave out details.

We start with a hypothesis H on a inductive predicate E and a goal G:

  H : E _ _
  ============================
   G

After 'generalize_eqs H' we get

  H : E _ _
  ============================
   _ = _ -> _ = _ -> _ ~= _ -> G

where H is now simplified, as expected. Now 'destruct H' gives us three
cases, of which we are interested in the second one. The first
invocation of simplify_one_dep_elim adds two dependent pair equalities
to the goal, I will show the first:

  ============================
   existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
   ... -> G

All two subsequent simplify_one_dep_elim invocations will generate the
simple equality p = q and introduce it to the context, so we get

  ============================
   p = q ->
   existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
   ... -> G

and then

  x : p = q
  ============================
   existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
   ... -> G

and after another two invocations

  x0 : p = q
  x : p = q
  ============================
   existT _ p (existT _ a x) = existT _ q (existT _ a y) ->
   ... -> G

and so on, each time introducing the same equality as x1, x2, etc.

Now I know close to nothing about how this all works, but I'm guessing
that the problem is in the nested use of existT.

Is this something simplify_one_dep_elim cannot handle? Could I adjust
the tactic simplify_one_dep_elim_term in some way?

Or is this a sign there is something wrong with my development?

Thanks for any help,
Martijn