Membership of substructure

Stream: Is there code for X?

[Artie Khovanov]

Is there a tactic, or even just a pattern, for proving membership in substructures?

e.g. if we have (S R : Type*) [CommRing R] [SetLike S R] [SubringClass S R] (A : S), and (x : R) (y : R) (hx : x ∈ A) (hy : y ∈ A), is there an easy way to prove x * y - (y + 1) + (y ^ 3) ∈ A?

Right now the best I can do is just chain all the closure axioms together, but this becomes very tedious in practice when working with substructures.

[Bjørn Kjos-Hanssen]

by aesop :smile:

import Mathlib

example (S R : Type*) [CommRing R] [SetLike S R] [SubringClass S R] (A : S) (x : R) (y : R) (hx : x ∈ A) (hy : y ∈ A) :
  x * y - (y + 1) + (y ^ 3) ∈ A := by aesop

[Artie Khovanov]

Thanks! That makes sense.

How can I extend this to new structures I create? For instance, I have a structure which (among other things) is a semiring containing all squares. I need to prove membership of x₁ * x₂ + (a * a) * (y₁ * y₂), given that the xs and ys are in my structure.

Can I somehow register mysquare_mem assumption with Aesop? Is there an easy way to see other lemmas already registed with Aesop, perhaps, so I can copy the pattern?

[Bjørn Kjos-Hanssen]

Not sure... Can you post a #mwe of the situation?

[Artie Khovanov]

import Mathlib

variable (S R : Type*) [CommRing R] [SetLike S R]

/-- `RingPreorderingClass S R` says that `S` is a type of (ring) preorderings on `R`. -/
class RingPreorderingClass extends SubsemiringClass S R : Prop where
  square_mem (P : S) (x : R) : x * x ∈ P /- want to "register" this -/
  minus_one_not_mem (P : S) : -1 ∉ P

variable [RingPreorderingClass S R] (P : S)

theorem closure_test (a x₁ x₂ y₁ y₂ : R)
    (hx₁ : x₁ ∈ P) (hy₁ : y₁ ∈ P) (hx₂ : x₂ ∈ P) (hy₂ : y₂ ∈ P) :
    x₁ * x₂ + a * a * (y₁ * y₂) ∈ P := by
  aesop /- doesn't work -/

[Bjørn Kjos-Hanssen]

OK I found a solution by reminding Lean that P contains all squares before invoking aesop:

import Mathlib

variable (S R : Type*) [CommRing R] [SetLike S R]

/-- `RingPreorderingClass S R` says that `S` is a type of (ring) preorderings on `R`. -/
class RingPreorderingClass extends SubsemiringClass S R : Prop where
  square_mem (P : S) (x : R) : x * x ∈ P /- want to "register" this -/
  minus_one_not_mem (P : S) : -1 ∉ P

variable [RingPreorderingClass S R] (P : S)

theorem closure_test (a x₁ x₂ y₁ y₂ : R)
    (hx₁ : x₁ ∈ P) (hy₁ : y₁ ∈ P) (hx₂ : x₂ ∈ P) (hy₂ : y₂ ∈ P) :
    x₁ * x₂ + (a * a) * (y₁ * y₂) ∈ P := by
  have := RingPreorderingClass.square_mem P
  aesop

[Artie Khovanov]

that makes sense, thanks so much!
I guess I should look through the Aesop docs to try figure out how to register the rule permanently..

[Artie Khovanov]

and yeah the a * a should be in brackets that's my bad

[Bjørn Kjos-Hanssen]

I guess in the meantime you can shorten things by writing

lemma aesop' :  ∀ (x : R), x * x ∈ P := RingPreorderingClass.square_mem P

theorem closure_test (a x₁ x₂ y₁ y₂ : R)
    (hx₁ : x₁ ∈ P) (hy₁ : y₁ ∈ P) (hx₂ : x₂ ∈ P) (hy₂ : y₂ ∈ P) :
    x₁ * x₂ + (a * a) * (y₁ * y₂) ∈ P := by
  have := aesop'; aesop

[Artie Khovanov]

true yeah

[Artie Khovanov]

(deleted)

[Artie Khovanov]

OK I found out how to register the rule -- but aesop appplies the multiplicative rule first :( so it doesn't work
I guess there is probably some priority system...

[Artie Khovanov]

so there is!

import Mathlib

variable (S R : Type*) [CommRing R] [SetLike S R]

/-- `RingPreorderingClass S R` says that `S` is a type of (ring) preorderings on `R`. -/
class RingPreorderingClass extends SubsemiringClass S R : Prop where
  square_mem (P : S) (x : R) : x * x ∈ P
  minus_one_not_mem (P : S) : -1 ∉ P

export RingPreorderingClass (square_mem)
export RingPreorderingClass (minus_one_not_mem)
attribute [aesop safe 0 apply (rule_sets := [SetLike])] square_mem

variable [RingPreorderingClass S R] (P : S)

theorem closure_test (a x₁ x₂ y₁ y₂ : R)
    (hx₁ : x₁ ∈ P) (hy₁ : y₁ ∈ P) (hx₂ : x₂ ∈ P) (hy₂ : y₂ ∈ P) :
    x₁ * x₂ + (a * a) * (y₁ * y₂) ∈ P := by
  aesop

thanks for your help @Bjørn Kjos-Hanssen ☀️ !
I think this code is idiomatic now (unless someone more experienced than me would like to weigh in?)

[Bjørn Kjos-Hanssen]

Nice! Doesn't look like you need more than attribute [aesop safe 0] square_mem in that line by the way.

[Artie Khovanov]

Yeah, the last two attributes restrict the usage scope of the rule. So (since I aim to merge to Mathlib) I think they should stay, if only for performance reasons.