Bringing names to proof mode

[h0nzZik]

What are the alternative approaches to having names in proof mode, and in imported Kore definitions?
ProofModePattern - this implements something resembling a weak HOAS.

If we introduce a new syntax for named patterns - are all translations of patterns into locally nameless well-formed?

[berpeti]

Additional comments:

• An alternative idea to weak HOAS could be a locally nameless representation with names in the binders.
• The current MLConstruct is describing an abstract meta-level syntax. Is this abstraction needed?
• Should positivity/negativity of variables be included in the PContext? So that we can determine which variables are allowed to use to name de Bruijn indices.
• Should positivity be omitted from the locally-nameless syntax, and only used in PreFixpoint? Probably this refactoring would cause a lot of issues with well-formedness constraint solving which relies on the fact that all provable patterns are well-formed.

[h0nzZik]

A clarification regarding the fourth point: omission of positivity from the locally-nameless syntax would break the property that all provable patterns are well-formed. That would in turn create the need to solve well-formedness constraints: we use the property to ensure that we do not need to generate such constraints often in the first place.

Regarding "locally nameless representation with names in the binders": (1) how would formulas in such representation be printed? Some time ago I tried to write pretty-printer which would be given a formula together with a bunch of names; however, it is not easy to hook arbitrary code to Coq's pretty printing mechanism. The ProofModePattern solution has an advantage here - it is easy to define Coq notations on top of the applications of pmpatt_construct, something like:

Notation "phi1 ---> phi2" := (pmpatt_construct (mlc_imp) [# phi1; phi2] vnil vnil).

or we may also define an intermediate layer (which I would vote for doing):

Definition npatt_imp phi1 phi2 := (pmpatt_construct (mlc_imp) [# phi1; phi2] vnil vnil).

Also, (2) the user would still to write the deBruijn indices instead of names for occurrences of bound variables. And even the translator from the matching logic specification language would need to work with indices.

Another alternative mentioned in the meeting today was to have one inductive with all the supported derived notations (typically those of Kore). I am strongly against that, as that (1) does not lead to an extensible proof mode, and (2) does not allow reusing Nishant's matching logic specification language.

[h0nzZik]

Regarding the MLConstruct. We need to represent derived notions somehow. So what are the options?
(1) Using Coq's notation mechanism directly - this is not a good idea, as we argued in the FROM'22 paper.
(2) Using Coq's definitions as we do with the locally nameless syntax. Note that this does not allow us to distinguish between different kinds of parameters a notation might have, such as "element variable binder", "set variable binder", or "pattern", without reflection ala MetaCoq. Is this ability necessary? Probably not, but having that would allow us to immediately and programmatically recognize bound variables, without expanding all the notations down to primitives.

We also need to somehow represent variable renaming and general substitution. This is tricky. Currently, in the locally nameless representation we ended up having typeclass instances for each syntactic construct, basically because we wanted to avoid expanding the notations when applying substitution. We probably want the same property in the named representation, and therefore we will need some objects representing the notations and their properties anyway. So why not making these properties part of the definition of derived construct? Also, in the locally nameless representation we do not have one typeclass representing a construct properties, but a bunch of them - one for ebinder, one for sbinder, one for binary connective, one for nullary, etc. And if some derived construct falls outside those categories, we have to create a new typeclass for it. I would prefer not to duplicate this non-elegance into the named setting.

[berpeti]

I think, this is an important observation about the substitution. Is it not possible to lift these properties from the locally nameless setup to the named in some way? (Or the other way around - since the named syntax is more abstract?)

[h0nzZik]

Can you elaborate on that? Given which kind of named syntax? And as I said, what we have in the LN setting is not very elegant.

[h0nzZik]

Just an idea: maybe we could refine the MLConstruct further. Instead of taking a list/vector of patterns, it would take two of those - one containing patterns in which the derived construct is positive, and one in which it is negative. Knowing which are which might be useful even outside well-formedness - for example, we have some monotonicity and anti-monotonicity lemmas (near the deduction theorem working with mu) which depend on this notion.

[berpeti]

We created an alternative representation for named patterns, in some sense similar to Pattern_in_Context. A named pattern is a locally nameless pattern indexed by a list of names (which are used to denote the dangling de Bruijn indices of a pattern):

AML-Formalization/matching-logic/src/Experimental/NamedSyntax.v

Lines 121 to 123 in 7707101

	Record NamedPattern (l : list evar) : Set := to_named {
	pat :> Pattern;
	}.

The coercion :> allows us to automatically lift locally nameless patterns to the named level. Compared to Pattern_in_Context, here we index the type with the names rather than having a function parameter mapping names to locally nameless patterns. This allows us to use the type to express how binders should be handled. Thereafter, we derive the primitives:

AML-Formalization/matching-logic/src/Experimental/NamedSyntax.v

Lines 127 to 139 in 7707101

	(* Primitives *)
	Definition named_var {l : list evar} (x : evar) : NamedPattern l :=
	match index_of x l with
	| None => to_named l (patt_free_evar x)
	| Some n => to_named l (patt_bound_evar n)
	end.
	Definition named_imp {l} (p1 : NamedPattern l) (p2 : NamedPattern l) : NamedPattern l :=
	to_named l (patt_imp p1 p2).
	Definition named_app {l} (p1 : NamedPattern l) (p2 : NamedPattern l) : NamedPattern l :=
	to_named l (patt_app p1 p2).
	Definition named_exists {l} (x : evar) (p : NamedPattern (x::l)) : NamedPattern l :=
	to_named l (patt_exists p).
	Definition named_bot {l} : NamedPattern l := to_named l patt_bott.

For these, we use the record constructor to_named, but this constructor should not be used for any other purposes. The list of names is used to denote variables, i.e., the variable x is a free variable, if it is not in the list, otherwise, it is a bound variable and the index of x denotes the actual de Bruijn index.

In case of the existential quantification, the body of the pattern (potentially) includes a new dangling index, for which the name is appended to the front of the list of names.

Another key point of this formalism is blocking Coq's computation so that the named patterns are not automatically simplified to locally nameless patterns every case simpl or cbn is used (unfold still works):

AML-Formalization/matching-logic/src/Experimental/NamedSyntax.v

Line 143 in 7707101

Arguments pat : simpl never. (* <- This is the key *)

The derived notations should not be expressed with to_named, instead we derive them (as in the locally nameless approach):

AML-Formalization/matching-logic/src/Experimental/NamedSyntax.v

Lines 145 to 148 in 7707101

	Definition named_not {l} (p : NamedPattern l) : NamedPattern l :=
	named_imp p named_bot.
	Definition named_forall {l} (x : evar) (p : NamedPattern (x::l)) : NamedPattern l :=
	named_not (named_exists x (named_not p)).

Based on these definitions, the usual notations can be introduced and used for the named syntax:

AML-Formalization/matching-logic/src/Experimental/NamedSyntax.v

Lines 170 to 178 in 7707101

	Notation "a $ₙ b" := (named_app a b) (at level 65, right associativity) : ml_scope.
	Notation "'Botₙ'" := named_bot : ml_scope.
	Notation "⊥" := named_bot : ml_scope.
	Notation "a --->ₙ b" := (named_imp a b) (at level 75, right associativity) : ml_scope.
	Notation "'ex' x , phi" := (named_exists x phi) (at level 80) : ml_scope.
	Notation "x 'ₑᵥ'" := (named_var x) (at level 1, format "x ₑᵥ") : ml_scope.
	Notation "!ₙ p" := (named_not p) (at level 71, right associativity) : ml_scope.
	Notation "'all' x , phi" := (named_forall x phi) (at level 80) : ml_scope.

Finally, the best feature of this approach is that the locally nameless lemmas and well-formedness can automatically be used in the named syntax (for this reason, the proof mode also works without any modification). There are a number of examples in NamedSyntax.v. There is one disadvantage: in case of substitutions the locally nameless notations are used.

Adding well-formedness to this approach

We can also build the closedness into this representation by saying that there are at least as many names in the list as many dangling indices:

AML-Formalization/matching-logic/src/Experimental/NamedSyntax.v

Lines 334 to 337 in 7707101

	Record NamedPattern (l : list string) : Set := to_named {
	pat :> Pattern;
	names_enough : length l >= greatest_dangling_index pat
	}.

This addition makes the definitions more robust, but obtaining locally nameless proofs from named ones is more challenging in this case.

[berpeti]

A technical sidenote: if we want to reuse the nameless notations in the named setup, we might need to overload notations.