Currently, Sterling checks what relations need to be defined mutually and groups them in the Extensibella output into the smallest mutual groups. This is necessary for relations using schematic polymorphism because of how Abella handles it. However, non-schematic relations do not need this; doing it for all relations makes it easier to ensure the full output is valid for Abella through Extensibella.
The problem is it limits how we can group properties to prove in Extensibella. If relations for expr and stmt are not currently defined mutually, then Extensibella can't reason about them via mutual induction. This means extensions can't make them mutually-inductive either, since the existing properties won't be provable. For example, when expressions can contain statements, evaluation for both will be defined mutually, and type preservation for each will depend on the other. However, if the two versions of type preservation are proven separately in the existing language, we can't combine them to prove them for the extension.
To solve this, I propose a construct in the Extensibella extension to tell it to make definitions mutual in the Extensibella output even though they aren't currently; something like
Extensibella_Mutual: evalExpr, evalStmt
This would not have any meaning outside of Extensibella translation, similar to Extensibella_Stand_In.
Currently, Sterling checks what relations need to be defined mutually and groups them in the Extensibella output into the smallest mutual groups. This is necessary for relations using schematic polymorphism because of how Abella handles it. However, non-schematic relations do not need this; doing it for all relations makes it easier to ensure the full output is valid for Abella through Extensibella.
The problem is it limits how we can group properties to prove in Extensibella. If relations for
exprandstmtare not currently defined mutually, then Extensibella can't reason about them via mutual induction. This means extensions can't make them mutually-inductive either, since the existing properties won't be provable. For example, when expressions can contain statements, evaluation for both will be defined mutually, and type preservation for each will depend on the other. However, if the two versions of type preservation are proven separately in the existing language, we can't combine them to prove them for the extension.To solve this, I propose a construct in the Extensibella extension to tell it to make definitions mutual in the Extensibella output even though they aren't currently; something like
This would not have any meaning outside of Extensibella translation, similar to
Extensibella_Stand_In.