The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

A few months ago I asked about decidable equality on nested structures. As usual, Cedric Auger came to the rescue :)

Here's the log about the thread in question: https://sympa.inria.fr/sympa/arc/coq-club/2012-08/msg00122.html

Anyway, I believe i have a similar problem now, but I'm not sure how I could adapt the approach to solve my particular situation.

Say you have an inductive like so:

Inductive box : Type :=
  Cons : nat -> list box -> box.

And now I want to prove

Lemma p_dec:
  forall b:box, p b \/ ~ p b.

where p is some predicate of the following shape:

Inductive p (b:box) : Prop :=
 | Xyz : forall n lb, b = Cons n lb ->
                             (forall b', In b' lb -> p b') ->
                             q n.


So, in order to prove p_dec I would need decidability on predicate q (which you can assume I have), but also decidability on all b' for p....So you see my problem here :-)

I believe the solution will be something similar to the one on decidable equality shown on the link above...but how can I adapt it to my case?

Cheers!


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