jvanbruegge/binder_datatypes

A new foundational package for Isabelle/HOL that implements binding-aware datatypes

binder_datatypes's Issues

Allow to specify a predicate for the parameters in the recursor

Currently you have to use a typedef to restrict the type of the parameters in the recursor. This is e.g. necessary to allow only small support functions in vvsubst.
It would be nice if the user could specify a predicate that is threaded through all the recursor proofs that can be used to proof the axioms.

Make sugar allow passive positions

Prerequisites:

• #35

Implement the corecursor

Currently the package only defines a recursor. This makes it impossible to have infinitely deep types. Defining the corecursor would fix that.

Register mixfix syntax associated with constructors

Currently you can already specify mixfix syntax, but it is not used by the implementation.

Create a parser for the custom binder_datatype syntax

Currently, datatypes have to be created from ML. Similar to normal datatypes, binder_datatypes should have custom syntax to define datatypes easily. The idea at the moment is to support syntax like this:

binder_datatype (FVars: 'a, 'b) foo =
  Var 'a
| Ann 'b
| Lam x::'a t::"('a, 'b) foo" binds x in t
| App "('a, 'b) foo" "('a, 'b) foo"
| LetRec "(xs::'a * ts::(('a, 'b) foo)) list" t::"('a, 'b) foo" binds xs in ts t
for
  map: vvsubst

Open questions about syntax:

• It would be convenient for the user to work with a concrete variable type. Should we automate this and how should we specify this? Current idea: separate command
• Should we automate singular substitution and multi- (list) substitution? Would be more convenient for the user as this could discharge all cardinality assumptions.

Prerequisites:

• #9

Allow to bind in other things not just in recursive positions

This would allow to easily express a global binding like XML, or get rid of the mutual types trick for Pi-commitments

Generalize the recursor to allow passive positions and mutually recursive types

Currently all positions have to be part of the fixpoint. Most of the complexity is in defining the map/set/rel constants using the recursor such that the passive positions are accounted for.
Additionally, types cannot be mutually recursive at the moment. Doing this generalization at the same time as passive variables is probably easier than afterwards

Make sugar allow mutual recursion

Prerequisites:

• #34

Provide FFVars_tvsubst again

This theorem was removed because of difficulties proving it, but the solution is to generate a theorem on the fly that re-associates the set unions as needed.

Generalize vvsubst to allow mutual recursion and passive positions

This involves defining set functions via the recursor. The relator can be defined corecursively. This might be possible for sets as well.

Prerequisites:

• #10

Fix binder_induction in relators and under quantifiers

Currently it still struggles with those

Make tvsubst compose

Currently, using a nested binder_datatype does not compose the substitution functions. This is needed to e.g. substitute types in term of System F.
Prerequisites:

• #10
• #18
• #35

Make tvsubst allow mutual recursion

Allow to specify a predicate for the codomain of the recursor

Similar to #15

Do not generate a new class at every step of the composition or mrbnf definition

In general we usually deal with either natLeq or card_suc natLeq. Instead of creating the same class over and over again we should create it once (probably even in normal Isar) and then use it when appropriate.
This has several advantages:

• Performance: There are a lot of theorems that are proven again and again for no reason
• Clutter: Currently using print_theorems after creating a binder type shows a ton of class theorems that are irrelevant for the user
• Readability: If we define the two common classes by hand, we can give them sensible names like var_finite and var_countable

Fix more_consumes vs nmajor cases bug

See rule induction proofs in STLC

Allow to specify the minimum cardinal in the recursor again

During #14 this feature was removed. It is necessary however for tvsubst with more than one variable position

Create a binder_(co)primrec to define primitive recursive functions on binder_datatypes

Currently the only way to define a function on a binder_datatype is to drop down to ML and call the recursor axiomatization directly. There should be an easier way for the user to do this by transforming primitve recursive equations into the fold that is the recursor.

Open questions:

• How to specify parameters and how should the user prove the axioms about the parameters?
• How to deal with monomorphic functions? At the moment the recursor expects to work abstractly.

Automate singular/list substitution

For most syntaxes singular or list substitution is enough. This would have the advantage that all cardinality assumptions could be discharged automatically making it easier to use.

Fix binder_induction method for mutual recursion and more than one variable kind

Allow changing the names of the involved constants

Currently some constants have a hard coded name based of their type. In the future we should allow to specify any name for user-facing constants and types.

Make tvsubst allow passive positions

Investigate monomorphic recursor

This should not be hard, the proofs should stay the same