Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: decidability and all that

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: decidability and all that


Chronological Thread 
  • From: Nuno Gaspar <nmpgaspar AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Re: decidability and all that
  • Date: Wed, 29 Aug 2012 16:02:42 +0200

Ok, scratch that repeat inversion; subst - I should never use that :x

2012/8/29 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.



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



Archive powered by MHonArc 2.6.18.

Top of Page