The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> Dear Adam,
>
> Adam Chlipala wrote:
> > > Your theorem above tie things down quite nicely - many thanks for 
> > > that. But I was also wondering (for curiosity sake more than 
> > > anything else) whether <-> could be replaced by ->, if the implicand 
> > > constrained Y to be the smallest possible list. If that were 
> > > possible, (X p') wouldn't then be a witness.
> >
> > Do you have some convention in mind for doing such constraining with 
> > an implication?  I've never seen such a feature in logic or math, on 
> > paper or on a computer.  You could certainly do it with an extra 
> > conjunction and universally-quantified fact, though.
>
> I hope I've used the right terminology. I suggested constraining the 
> implicand, not the implication. As far as I'm aware, the implicand is 
> the conclusion of the implication.

Right, I understood that.  The problem is that you are trying to make a 
"non-local statement" about the range of a quantifier that occurs 
outside the implicand, where you are only allowed to mention one value 
of the quantified variable "at a time."  I don't know how to do that 
without using computational effects in the fairly exotic way that 
linguists use them to model some features of natural language.