The Coq mailing list

[roconnor AT theorem.ca]

On Sat, 17 Oct 2009, 
roconnor AT theorem.ca
 wrote:

> On Sat, 17 Oct 2009, muad wrote:
>
> > I feel like I might still not understand exactly what is needed, but 
> > perhaps
> > this is a solution?
> >
> > Inductive SillyTreePair SillyTree (b:bool) : Type :=
> > | stp : SillyTree b -> SillyTree b -> SillyTreePair SillyTree b.
> >
> > Inductive SillyTree : bool -> Type :=
> > | leaf : SillyTree true
> > | node : forall b, SillyTreePair SillyTree b -> SillyTree false.
> >
> > Definition sillyFunction (st:SillyTree false) : bool :=
> >  match st with
> >    | node a (stp leaf leaf) => a
> >    | _ => false
> >  end.
> >
> > SillyTree is making use of the fact that SillyTreePair f b is a strictly
> > positive operator in f.
>
> Yes this works, and is a varient of what I had in mind for my very last 
> possible solution that I didn't write out in detail.  It is just a little sad 
> that SillyTreePair ends up being polymorphic in the SillyTree parameter, 
> which means another parameter needs to be passed everywhere.
>
> I would probably rename your SillyTreePair as preSillyTreePair and then 
> define (prehaps a notation) SillyTreePair := preSillyTreePair SillyTree.

Remark: a notation didn't work in my real application because I need 
`SillyTreePair' to be a target for a coercion.

> Perhaps this is the best compromise, but it still isn't as nice as what you 
> can express in Agda.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''