The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 17/11/2014 06:12, Hugo Carvalho wrote:
> At this point i haven't been able to make any further progress. It seems
> like, since "repeats" is a Prop (and therefore the whole proof happens
> in a Prop context), it should be possible to switch the "member" in the
> hypothesis for "appears_in", but alas, my current strategy seems to
> depend on the Type-ness of the hypothesis, that is, simply switching
> "sig"s for "exists" doesn't work (crucially, i have a lemma whose
> statement has projections in it).

This sounds like a case of standard Prop-to-Type leaking technique. As
Coq allows elimination of singleton types, there are roughly 3 cases
where you can escape Prop to construct something interesting in Type:

1. Elimination of False
2. Rewriting of equality
3. Induction over accessible predicates (Coq.Init.Wf.Acc)

I think you are in the third case. If your equality is decidable, then
you can use the proof technique described here:

https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html

This will allow to transform your Prop-based appear_in into a Type-based
one.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature