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.
Last updated: Nov 16 2025 at 20:22 UTC