The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

In this particular case, I did manage to use coercions.  I did have to 
change a few tactics to accommodate the appearance of the coercion 
function, but it worked.  It does feel a bit fragile, though.  In 
particular, the user type that I want numerals to work for is also 
declared to be a ring, and I need ring-simplify to work properly even in 
other cases I haven't tried yet.  Maybe I can rig the Add Ring 
declaration with the necessary preprocess/postprocess tactics to 
unfold/fold the coercion function?

But, I would like to avoid this by having everything handled in the 
parse/print layers.

As for Jason's question of how my "stupider" suggestion should handle 
open terms and printing, well, I did say it was stupider.

If there were concerns about the functions not providing an isomorphism 
(hence being able to appear to prove "2 = 3", for example) - then I 
guess it could require a Class with proofs that the two conversion 
functions provide an isomorphism.

-- Jonathan

On 02/22/2016 12:19 PM, Gregory Malecha wrote:
> Would Coercions fit the bill for the nat2mynat idea? Or are they not
> expressive enough.
>
> On Sun, Feb 21, 2016 at 8:40 PM, Jason Gross 
> <jasongross9 AT gmail.com>
>  wrote:
>
> > Jonathan, how does that work on open terms?  It'll work fine for parsing,
> > probably (though I don't really want to be able to do arbitrary computation
> > in the parsing of my numerals, that's perhaps a bit scary, but perhaps
> > useful), but seems kind-of sketchy for printing.
> >
> > On Sun, Feb 21, 2016 at 9:08 PM, Jonathan Leivent 
> > <jonikelee AT gmail.com>
> > wrote:
> >
> > > I was thinking something even stupider than that!  The user gives two
> > > functions that map between nats and the user type they want to represent
> > > with number notations:
> > >
> > > Inductive mynat : Set := ...
> > >
> > > Definition nat2mynat(n : nat) : mynat := ...
> > >
> > > Definition mynat2nat(m: mynat) : nat := ...
> > >
> > > Declare Nat Syntax mynat Using nat2mynat, mynat2nat : M_scope.
> > >
> > > The parser would, whenever it sees a number in the scope M_scope, call
> > > nat2mynat and use the result.  The printer would, whenever it sees a mynat
> > > in the scope M_scope, call mynat2nat, and print the resulting number.
> > >
> > > -- Jonathan
> > >
> > >
> > > On 02/21/2016 06:05 PM, Jason Gross wrote:
> > >
> > > > I was thinking something stupider: you pass in terms that are treated as
> > > > constructors and required to have the appropriate type signature (a type
> > > > "NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
> > > > parametric over how many universes NAT uses, and whether its polymorphic
> > > > or
> > > > not, etc), and then notations get translated to applications of S and O,
> > > > and applications of S and O get translated back, and if S and O happen to
> > > > unfold to other things, then unfolding them breaks the notation (which is
> > > > not the end of the world).
> > > > Even better would be to generalize the nat_syntax_plugin to handle things
> > > > like [trunc_index], i.e., things where the base case should be displayed
> > > > as
> > > > 1 or as -2, etc.
> > > >
> > > > I do not think that we should have to trust Ltac code to get syntax for
> > > > custom natural numbers.
> > > >
> > > > On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <
> > > > pierre-marie.pedrot AT inria.fr>
> > > >  wrote:
> > > >
> > > > On 21/02/2016 23:31, Jason Gross wrote:
> > > > > > How hard would it be to set up the syntax plugins already in Coq so
> > > > > > that
> > > > > > they registered vernaculars such as [Declare NatSyntax for nat in
> > > > > > nat_scope [O S].] and similarly for notations for negative numbers,
> > > > > > ascii, strings, etc?
> > > > > Not that difficult, I believe. Yet, we need to rely on a meta-language
> > > > > to pattern-match over terms. Ltac would fit the bill, but I personally
> > > > > find this use a little bit ugly.  The vernacular would probably look
> > > > > like:
> > > > >
> > > > > Parameter myNat : Type.
> > > > >
> > > > > Ltac reify_myNat n :=
> > > > > match n with
> > > > > (* insert a code producing a Z from a myNat here *)
> > > > > end.
> > > > >
> > > > > Declare Nat Syntax myNat reify_myNat.
> > > > >
> > > > > PMP