Email Gateway (Aug 19 2022 at 14:22): Email Gateway (Aug 19 2022 at 14:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
in the example beneath, on the last setup_lifting command, I get »No
relator for the type poly_mapping found«
I tried my best to glimpse from exisiting lifting examples and the
reference manual what is missing and added poly_mapping_rel with some
characteristic properties (proofs only sketched), but the warning remains.
Any hints?
Thanks a lot,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 14:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
When setup_lifting warns you about missing relators, it looks for a corresponding quotient
theorem that is registered as [quot_map], something like
lemma Quotient_poly_mapping [quot_map]:
assumes Q1: "Quotient R1 Abs1 Rep1 T1"
and Q2: "Quotient R2 Abs2 Rep2 T2"
shows "Quotient (poly_mapping_rel R1 R2) (map_poly_mapping Rep1 Abs2) (map_poly_mapping
Abs1 Rep2) (poly_mapping_rel T1 T2)"
If you can prove such a quotient theorem, setup_lifting will generate a parametrised
relator for lifting to nat_mapping where the type of the type parameter can change. The
lemmas that you have shown will help setup_lifting to prove properties of the relator
pcr_nat_mapping.
Andreas
PS: I do not think that you can prove a quotient theorem like the above, because
poly_mapping is not really parametric in its type parameters: 0::'b::zero has to be mapped
to zero in the other type, and the finiteness constraint prevents quotients with
non-finite equivalence classes.
Last updated: Apr 26 2024 at 20:16 UTC