George Chemmala (Nov 05 2025 at 18:13): George Chemmala (Nov 05 2025 at 18:13):I'm part of a group working on proving lemmas in projective geometry. There is a duality between points and lines, so ideally we could write a lemma and our ML function would automatically convert the lemma into the duel projective space.
I'm familiar with something like this in Lean with groups, but wasn't sure if this was also possible in Isabelle
@[to_additive]
class Monoid (α : Type) extends Semigroup α, MulOneClass α
attribute [to_additive existing] Monoid.toMulOneClass
class AddGroup (G : Type) extends AddMonoid G, Neg G where
/-- -a + a = 0 -/
neg_add : ∀ a : G, -a + a = 0
/-- a + -a = 0 -/
add_neg : ∀ a : G, a + -a = 0
@[to_additive]
class Group (G : Type) extends Monoid G, Inv G where
/-- a⁻¹ * a = 1 -/
inv_mul : ∀ a : G, a⁻¹ * a = 1
/-- a * a⁻¹ = 1 -/
mul_inv : ∀ a : G, a * a⁻¹ = 1
Usually I think you'd use the transfer package for that sort of thing. But I am not comfortable enough with it to give more specific advice.
George Chemmala (Nov 17 2025 at 23:14):Sorry for the late reply - a little green to Zulip but I will look into this - thanks!
Manuel Eberl (Nov 18 2025 at 09:49):The basic idea is that you define some kind of correspondence relation between all the relevant functions and predicates (usually some kind of homomorphism or isomorphism) and then prove so called "transfer rules" for all the functions and predicates you care about. These essentially just state that the functions/predicate respect the correspondence relation (or are compatible with it).
Then you could generally define something like a group_homomorphism or group_isomorphism locale that fixes two groups and a function or relation between them. If you do a function and want isomorphism, you then have to define the relation from that as something like rel x y = (y = f x). Then you prove the transfer rules for all your group-theoretic functions and concepts, e.g. mul, inv, 1, order. And then you can instantiate that locale for addition and multiplication and use the transfer package to transfer all the results.
For the group case, the better solution would of course be to just define a generic group locale and then instantiate that for addition and multiplication separately.
In case of duality, you can do an interpretation or sublocale in your geometry stating that there is an isomorphism between the locale and its dual, and then get all the theorems that way.
In fact, you can do that even without the transfer package. You can just do a sublocale or interpretation inside your geometry locale, proving that the dual geometry is also a geometry. Then you get all the theorems resulting from that for your dual geometric. The problem is that the theorems you get from will of course be phrased in terms of concepts regarding the dual geometry, and you then still have to do some work to relate them to the same concepts of your original geometry. That's where transfer can help you. But if it's not that many theorems or if it relating the concepts of the dual geometry to the original one is easy anyway then you can also get by without using transfer.
This is all documented e.g. in Ondřej Kunčar's PhD thesis: https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf
Note that the transfer package does have some drawbacks, e.g. proving transfer rules for recursive functions can be painful, and it does not support conditional transfer rules. This is a problem if you e.g. define the inverse of a group as inv x = (SOME y. x * y = 1). Then y may well be undefined if x is not in the carrier of the group and you will not be able to prove a transfer rule for inv (or rather the natural transfer rule for it would have the precondition x ∈ carrier. I vaguely recall that @Kevin Kappelmann is working on some new tool that can do that sort of thing. But you can often also get away with just defining your concept in a way that does have a nice transfer rule, e.g. inv x = (SOME y. if x ∈ carrier then x * y = 1 else y = 1).
George Chemmala (Nov 24 2025 at 02:07):Is there a limit to how many sublocales you can make? e.g. a subsublocale?
Chelsea Edmonds (Nov 25 2025 at 07:48):I'm yet to run into any limits for sublocales with all the work I've done (both in terms of sublocale inheritance tree depth and breadth). Where you have to be careful is when you get circular dependencies (often still possible, but needs to be done very carefully to avoid an infinite loop in the sublocale declaration proof).
Last updated: Dec 07 2025 at 04:34 UTC