coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 definitionInductive 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.
- [Coq-Club] decidability and all that, Nuno Gaspar, 08/29/2012
- [Coq-Club] Re: decidability and all that, Nuno Gaspar, 08/29/2012
- Re: [Coq-Club] decidability and all that, AUGER Cédric, 08/29/2012
- Re: [Coq-Club] decidability and all that, Nuno Gaspar, 08/30/2012
Archive powered by MHonArc 2.6.18.