Meven Lennon-Bertrand (Nov 16 2022 at 11:58): Meven Lennon-Bertrand (Nov 16 2022 at 11:58):I am trying to set up a good notation system for a development tackling meta-theory of type systems. This means I have two "dimensions" of definitions: I have a wealth of different relations/predicates (a context is well-formed, a term has a certain type, two terms are convertible, and so on), and multiple variants of each of these (one of these variants is the standard declarative presentation, while another is more algorithmic in flavour, etc.). What I want to have is a setting where:
1) I can define a generic notion for each relation/predicate, with generic notations, and be able to reason on this generically
2) also be able to work with a single, specific instance, while keeping all the nice generic notations: say I have a file where I show that algorithmic conversion is transitive, this file only talks about the algorithmic notions, so I do not want to annotate every instance of typing in it to say it is the algorithmic one
3) be able to be more explicit when I need to talk about two different variants at the same time, so that I can write theorems like "this version of typing implies this other version of typing" in a readable way, but ideally in a way that is still generic, in the sense that I do not want to redefine a hardcoded subtly different set of notations for each variant
This looks somewhat similar to the question of generic notations for algebraic structures, but with two twists:
1) since all related relations have the same carrier, I cannot use a canonical-structure-like technique to disambiguate the notation
2) I want to have a non-ambiguous but still generic notation, rather than the situation for eg sums where the generic notion in practical instances (nat, Z, Q…) reduces to basically different hardcoded notations (or, rather, the same notation "+" in different scopes).
Does this ring a bell to any of you? Have you seen something like this before? Otherwise, any clue on how to achieve that? I have a first experiment in this gist, which gives a better idea of what I am trying to achieve in a simple setting, with comments on the parts I am unhappy with.
Paolo Giarrusso (Nov 17 2022 at 03:58):Instead of Class relgen := {rel : bool -> bool -> Type }. I'd expect Class relgen := rel : bool -> bool -> Type., and that might avoid some of the problematic econstructor calls
Paolo Giarrusso (Nov 17 2022 at 03:59):(examples in "typeclasses for mathematics in type theory", math-classes and stdpp, but they're not literally about your scenario)
Paolo Giarrusso (Nov 17 2022 at 04:02):The tag-based approach you have is probably going to be more robust. But you most likely want a hint mode marking the tag as an input; otherwise, Coq will be free to infer the first tag that works.
Paolo Giarrusso (Nov 17 2022 at 04:02):that's even more important for implicit arguments since you don't specify them explicitly
Meven Lennon-Bertrand (Nov 17 2022 at 13:55):Thanks for the tips! The ideas of having the tag-based and tag-free variants was to be able to hide the tags when they are irrelevant (either in the generic setting or when working on a particular example). But maybe this should just be notations over a single kind of typeclass which uses tags
Paolo Giarrusso (Nov 17 2022 at 19:13):Yeah maybe a variant notation can supply a default tag — possibly _ letting TC choose (which contradicts my other advice, but maybe #[export] Hint Mode exists and lets you change behavior locally?)
Last updated: Apr 20 2024 at 07:01 UTC