Named representation and syntactic constructs

[h0nzZik]

We have three use-cases for named representation of matching logic:

• export of proofs to MetaMath
• import of K definitions
• pretty printing in proof mode

1. However, it would be very unfortunate if we had to define every derived syntactic construct twice.
2. It would be even more unfortunate if the conversion between locally nameless representation and named representation lost the abstraction layer provided by derived syntactic constructs.

I have some rough ideas how to solve that; however, for now I would like to hear some opinions on this.

[daniel-horpacsi]

• You need to preserve the names you get from K (Kore), to make the theory and the proof states comprehensible for the user. This does not mean that you need to store the patterns in a named representation, you only need to be able to pretty-print with names. For this, it suffices to store the names of variables in the quantifiers that bind them.
• We may let binders be constructed without explicit names. If the user works with theories not having names in the binders (e.g., the theories do not come from K), names for bound variables need to be generated. This does not necessarily mean that you need to translate everything to a named representation, it may be enough to inject generated names into the binders, and pretty-print to MetaMath with names.
• That is, a single "annotated on-demand" locally nameless pattern representation may do the job.

[h0nzZik]

Still, if we traverse the pattern and print names from the annotations naively, we lose the abstractions created by using derived syntactical sugar. It is the same problem as with evar_open.

[berpeti]

Can you give an example please, that illustrates this? I do not completely understand the problem.

[h0nzZik]

Lets say, that we have a pattern in locally nameless representation:

patt_or (patt_sym s1) (patt_sym s2)

When we programatically convert this to a named representation, using some Fixpoint that goes on the structure of the formula, we get

npatt_imp (npatt_imp (npatt_sym s1) npatt_bot) (npatt_sym s2)

[berpeti]

I see the point. I think we could avoid this by extended pattern matching in the fixpoint, but then this Fixpoint needs to be modified every time we introduce a new syntactic sugar. Also, in this case, we need to face the same issue, that is caused by notations. E.g. (p ---> patt_bot) ---> patt_bot could be written as ! (! p) or ! p or patt_bot too.

[berpeti]

There is another drawback of using names in binders, namely, we need to introduce a notion of alpha equivalence, since ex x, \phi and ex y, \phi will not be syntactically equal anymore.

[daniel-horpacsi]

For the record, the documentation of metaprogramming in Lean4 explains that they use a so-called locally closed representation. For example, λ (x : Nat), Nat.add x x is represented as

.lam `x (.const ``Nat []) (mkAppN (.const ``Nat.add []) #[.bvar 0, .bvar 0])

Essentially, this is locally nameless, where the binders store the names of the variables they bind. There is an important convention, however: binders are to be constructed with corresponding constructors (for example, mkLambdaFVars for lambda expressions) which do the closing operation on an otherwise well-formed body expression. This way, they avoid dealing with expressions containing dangling (as they say, 'loose') bound variables. Similar consideration goes for deconstruction: they do not pattern match on binders, but they use opening to obtain the body, thus replacing bound variables with their name (see forallTelescope).

The ML-in-Lean formalization project is working on a metaprogramming-based proof extraction, where they traverse the Lean expression's structure to translate patterns and proofs to Metamath; they do rely on functions like forallTelescope when turning locally nameless expressions to named ones.