Marco David (May 26 2022 at 13:45): Marco David (May 26 2022 at 13:45):Dear Isabelle Community, I would like to better understand the 'setup_lifting' command and have spelled out a detailed question about this command here: https://stackoverflow.com/questions/72392804/how-to-setup-lifitng-with-custom-types-aka-how-to-define-a-relator
I would much appreciate your help!
Wenda Li (May 26 2022 at 14:10):Hi Marco,
The setup_lifting is only useful if you intend to use the lifting-and-transfer framework, for the details of which you can read Huffman and Kuncar's CPP paper. Some recent progress in this framework is mostly related to bounded natural functors, for which you can have a look at this paper.
Proposing suitable relators requires insight of the data type. Here setup_lifting gives us some relatively easy relator theorems for free.
Marco David (May 27 2022 at 13:01):I appreciate the reference to the theory behind this framework (an interesting glimpse into Isabelle history), but I care about using this framework for a specific example in formalizing mathematics — polynomials —, where two typedefs build on top of each other. Unfortunately, neither of two links above seems to be of much help to learn how to use the framework.
In the CPP paper, there are two examples of quotient theorems for relators — apparently the type of theorem I should care about — at the beginning of section 3.2. However, the next paragraph immediately states
Users generally will not prove the Quotient theorem manually for new types, as special commands exist to automate the process. The command quotient type defines a new quotient type, internally proves the corresponding Quotient theorem and registers it with setup lifting. We also support types defined by the command typedef. The theorem type_definition Rep Abs {x. P x}, which axiomatizes the newly defined subtype, can be supplied to setup_lifting.*
(emphasis mine)
As explained on StackOverflow, I am working with the typedef command. How can I supply this "Quotient theorem" about my monom type to setup_lifting?
Wenda Li (May 27 2022 at 14:19):Then I guess you are running into the problem of proposing a relator for some concrete types, which again can be highly non-trivial and sometimes even impossible... I have been working on the relator for the topology type and asked a similar question in the mailing list -- not sure if you can find the discussions online.
For a starting point of self-proposing a relator, you can have a look at the relator for sets and that for filters. Essentially, you need to propose a relation rel_monom of type ('a => 'b => bool) => 'a mono => 'b monom => bool and then prove properties like
lemma rel_monom_eq[relator_eq]: "rel_monom (=) = (=)"
lemma rel_monom_mono[relator_mono]: "rel_monom R ≤ rel_monom S" if "R ≤ S"
lemma rel_monom_distr [relator_distr]: "rel_monom A OO rel_monom B = rel_monom (A OO B)"
lemma Quotient_monom [quot_map]:
"Quotient R Abs Rep T ⟹ Quotient (rel_monom R) (monom_map Abs) (monom_map Rep) (rel_monom T)"
Thank you for the concrete pointers and lemma statements, that looks very useful! It is surprising that quotient types and subtypes of lists, sets etc work so seamlessly but as soon as you stack type definitions, it becomes much more complicated suddenly.
Last updated: Apr 19 2024 at 01:05 UTC