Stream: Coq users

Topic: Using custom entries


view this post on Zulip Pierre Castéran (Sep 25 2023 at 16:04):

Is there a simple way to define a notation for sequences of substitutions?
Let us consider the following context:

Parameter Exp:Set.
Definition var := nat.
Parameter subst : Exp -> var -> Exp -> Exp.

I would like to build a notation msubst e v1 <- t1 ; v2 <- t2; ... ; vn <- tn for subst ... (subst e v1 t1) v2 t2) ... vn tn.
I would prefer not to define msubst as a function, since it would break very long proof scripts which use nested substs.

Are custom entries the right tool for that?

view this post on Zulip Paolo Giarrusso (Sep 25 2023 at 18:15):

Naively, it seems like this should be possible with recursive notations, no custom entries seem necessary? Or did you notice some problem I'm missing?

view this post on Zulip Paolo Giarrusso (Sep 25 2023 at 18:20):

https://plv.mpi-sws.org/coqdoc/iris/iris.bi.lib.atomic.html uses recursive notations on a larger example — sorry I don't have code for your example, but Coq notations never seem to be 5-minute affairs.

view this post on Zulip Pierre Castéran (Sep 25 2023 at 19:11):

Thanks @Paolo Giarrusso
There exists a thread on this topic already. I will have to check if there exists a solution which satisfies my constraints (some long scripts in the goedel library contain nested substitutions, and I'm looking for readable notations for these big terms).

view this post on Zulip Paolo Giarrusso (Sep 25 2023 at 19:13):

Ooh I see, that link points to custom entries indeed


Last updated: Jun 23 2024 at 05:02 UTC