The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello friends.

Consider the following definition

Inductive def : Type :=

  | Cons1 : nat -> list nat ->def.

Now, let's say I want to prove decidability of this structure's equality. Trivially, the following does work.

Lemma def_dec:

  forall d d': def, {d = d'} + {d <> d'}.

Proof.

  intros.

  repeat decide equality.

Qed.

Now, say we have this definition instead:

Inductive def :Type :=

  | Cons1 : list def -> def.

The above proof would not work in this case. In fact, since I'm using repeat, it would actually never terminate.

As you've guessed by now :), I would like to know what is the approach you guys use for proving decidable equality of inductive definitions with self-referenced projections.

On a related note: I use CoqIDE and it does not seem to have any way to kill the current applied tactic, meaning that for the above infinite scenario I have no other way besides killing the application and restart it. Right?

Please note that this 'problem' may also arise in situations like 'repeat inversion H; subst', which is something that I use from time to time..

What's your input on that? I should treat using 'repeat' as some kind of "bad practice" or? Yeah, I know some of you could tell me that I should know beforehand what are the effects of the tactic before applying it :), but the thing is that sometimes I forget how I defined the structures and in the case of repeating inversions it was not that easy to predict - consider a respectable number of hypothesis in your context.

Anyway, some thoughts please :)

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.