feat(Tactic/Algebraize): Allow the algebraize tactic to use lemmas which don't (directly) mention RingHom (#24661)

This PR allows the `algebraize` tactic to be applied in more cases. Specifically, in cases where the assumption is not (directly) about RingHom, it should still be able to apply lemmas.

Written at the suggestion of @chrisflav , with the following example usecase:
```lean-4
import Mathlib

open AlgebraicGeometry

attribute [algebraize flat_of_flat] Flat -- pretend this is added where `AlgebraicGeometry.Flat` is defined

lemma flat_of_flat {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Flat (Spec.map (CommRingCat.ofHom f))) : @module.Flat R S _ _ f.toAlgebra.toModule := by
  have : f.Flat := sorry -- supposedly, this is true. ask christian.
  algebraize [f]
  assumption

set_option tactic.hygienic false -- allow the tactic to produce accessible names for testing

example {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Flat (Spec.map (CommRingCat.ofHom f))) : True := by
  algebraize [f]
  guard_hyp algebraizeInst : Module.Flat R S -- used to fail, succeeds now
  trivial
```

the key changes that makes this possible are the following:
- a different way of making lemma/type applications, creating a term which can be added to the context
- a different way of checking that the previously mentioned term actually relevant w/r/t the arguments provided to the tactic 

The previous check was ad-hoc and flimsy, making requirements of the precise order and the types of the arguments of lemmas or definitions, which resulted in the lemma being applicable in limited cases only.
Now we still have some requirements, but these are less stringent.



Co-authored-by: blizzard_inc <[email protected]>
Co-authored-by: Edward van de Meent <[email protected]>
Co-authored-by: blizzard_inc <[email protected]>

Author: edegeltje

Mathlib/Tactic/Algebraize.lean

@@ -176,38 +176,44 @@ def addProperties (t : Array Expr) : TacticM Unit := withMainContext do
     -- If it has, `p` will either be the name of the corresponding `Algebra` property, or a
     -- lemma/constructor.
     | some p =>
-      -- The last argument of the `RingHom` property is assumed to be `f`
-      let f := args[args.size - 1]!
-      -- Check that `f` appears in the list of functions given to `algebraize`
-      if ¬ (← t.anyM (Meta.isDefEq · f)) then return
-
-      let cinfo ← getConstInfo p
-      let n ← getExpectedNumArgs cinfo.type
-      let pargs := Array.replicate n (none : Option Expr)
-      /- If the attribute points to the corresponding `Algebra` property itself, we assume that it
-      is definitionally the same as the `RingHom` property. Then, we just need to construct its type
-      and the local declaration will already give a valid term. -/
-      if cinfo.isInductive then
-        let pargs := pargs.set! 0 args[0]!
-        let pargs := pargs.set! 1 args[1]!
-        let tp ← mkAppOptM p pargs -- This should be the type `Algebra.Property A B`
-        unless (← synthInstance? tp).isSome do
-        liftMetaTactic fun mvarid => do
-          let nm ← mkFreshBinderNameForTactic `algebraizeInst
-          let (_, mvar) ← mvarid.note nm decl.toExpr tp
-          return [mvar]
-      /- Otherwise, the attribute points to a lemma or a constructor for the `Algebra` property.
-      In this case, we assume that the `RingHom` property is the last argument of the lemma or
-      constructor (and that this is all we need to supply explicitly). -/
-      else
-        let pargs := pargs.set! (n - 1) decl.toExpr
-        let val ← mkAppOptM p pargs
-        let tp ← inferType val
-        unless (← synthInstance? tp).isSome do
-        liftMetaTactic fun mvarid => do
-          let nm ← mkFreshBinderNameForTactic `algebraizeInst
-          let (_, mvar) ← mvarid.note nm val
-          return [mvar]
+      let cinfo ← try getConstInfo p catch _ => return
+      let p' ← mkConstWithFreshMVarLevels p
+      let (pargs,_,_) ← forallMetaTelescope (← inferType p')
+      let tp' := mkAppN p' pargs
+
+      let getValType : MetaM (Option (Expr × Expr)) := do
+        /- If the attribute points to the corresponding `Algebra` property itself, we assume that it
+        is definitionally the same as the `RingHom` property. Then, we just need to construct its
+        type and the local declaration will already give a valid term. -/
+        if cinfo.isInductive then
+          pargs[0]!.mvarId!.assignIfDefEq args[0]!
+          pargs[1]!.mvarId!.assignIfDefEq args[1]!
+          -- This should be the type `Algebra.Property A B`
+          let tp ← instantiateMVars tp'
+          if ← isDefEqGuarded decl.type tp then return (decl.toExpr, tp)
+          else return .none
+        /- Otherwise, the attribute points to a lemma or a constructor for the `Algebra` property.
+        In this case, we assume that the `RingHom` property is the last argument of the lemma or
+        constructor (and that this is all we need to supply explicitly). -/
+        else
+          try pargs.back!.mvarId!.assignIfDefEq decl.toExpr catch _ => return .none
+          let val ← instantiateMVars tp'
+          let tp ← inferType val -- This should be the type `Algebra.Property A B`.
+          return (val, tp)
+      let .some (val,tp) ← getValType | return
+      /- Find all arguments to `Algebra.Property A B` which are of the form
+        `RingHom.toAlgebra x` or `Algebra.toModule (RingHom.toAlgebra x)`. -/
+      let ringHom_args ← tp.getAppArgs.filterMapM <| fun x => liftMetaM do
+        let y := (← whnfUntil x ``Algebra.toModule) >>= (·.getAppArgs.back?)
+        return (← whnfUntil (y.getD x) ``RingHom.toAlgebra) >>= (·.getAppArgs.back?)
+      /- Check that we're not reproving a local hypothesis, and that all involved `RingHom`s are
+        indeed arguments to the tactic. -/
+      unless (← synthInstance? tp).isSome || !(← ringHom_args.allM (fun z => t.anyM
+        (withoutModifyingMCtx <| isDefEq z ·))) do
+      liftMetaTactic fun mvarid => do
+        let nm ← mkFreshBinderNameForTactic `algebraizeInst
+        let (_, mvar) ← mvarid.note nm val tp
+        return [mvar]
     | none => return
 
 /-- Configuration for `algebraize`. -/

MathlibTest/algebraize.lean

@@ -6,57 +6,57 @@ section example_definitions
 
 /-- Test property for when `RingHom` and `Algebra` properties are definitionally the same,
 see e.g. `RingHom.FiniteType` for a concrete example of this. -/
-class Algebra.testProperty1 (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] : Prop where
+class Algebra.TestProperty1 (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] : Prop where
   out : ∀ x : A, algebraMap A B x = 0
 
 /-- Test property for when `RingHom` and `Algebra` properties are definitionally the same,
 see e.g. `RingHom.FiniteType` for a concrete example of this. -/
 @[algebraize]
-def RingHom.testProperty1 {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) : Prop :=
-  @Algebra.testProperty1 A B _ _ f.toAlgebra
+def RingHom.TestProperty1 {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) : Prop :=
+  @Algebra.TestProperty1 A B _ _ f.toAlgebra
 
 /-- Test property for when the `RingHom` property corresponds to a `Module` property (that is
 definitionally the same). See e.g. `Module.Finite` for a concrete example of this. -/
-class Module.testProperty2 (A M : Type*) [Semiring A] [AddCommMonoid M] [Module A M] : Prop where
+class Module.TestProperty2 (A M : Type*) [Semiring A] [AddCommMonoid M] [Module A M] : Prop where
   out : ∀ x : A, ∀ M : M, x • M = 0
 
 /-- Test property for when the `RingHom` property corresponds to a `Module` property (that is
 definitionally the same). See e.g. `Module.Finite` for a concrete example of this. -/
-@[algebraize Module.testProperty2]
-def RingHom.testProperty2 {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) : Prop :=
+@[algebraize Module.TestProperty2]
+def RingHom.TestProperty2 {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) : Prop :=
   letI : Algebra A B := f.toAlgebra
-  Module.testProperty2 A B
+  Module.TestProperty2 A B
 
 /-- Test property for when the `RingHom` property corresponds to a `Algebra` property that is not
 definitionally the same, and needs to be created through a lemma. See e.g. `Algebra.IsIntegral` for
 an example. -/
-class Algebra.testProperty3 (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] : Prop where
-  out : Algebra.testProperty1 A B
+class Algebra.TestProperty3 (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] : Prop where
+  out : Algebra.TestProperty1 A B
 
 /- Test property for when the `RingHom` property corresponds to a `Algebra` property that is not
 definitionally the same, and needs to be created through a lemma. See e.g. `Algebra.IsIntegral` for
 an example. -/
-@[algebraize Algebra.testProperty3.mk]
-def RingHom.testProperty3 {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) : Prop :=
-  f.testProperty1
+@[algebraize Algebra.TestProperty3.mk]
+def RingHom.TestProperty3 {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) : Prop :=
+  f.TestProperty1
 
 /- Test property for when the `RingHom` (and `Algebra`) property have an extra explicit argument,
 and hence needs to be created through a lemma. See e.g.
 `Algebra.IsStandardSmoothOfRelativeDimension` for an example. -/
-class Algebra.testProperty4 (n : ℕ) (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] : Prop where
+class Algebra.TestProperty4 (n : ℕ) (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] : Prop where
   out : ∀ m, n = m
 
 /- Test property for when the `RingHom` (and `Algebra`) property have an extra explicit argument,
 and hence needs to be created through a lemma. See e.g.
 `Algebra.IsStandardSmoothOfRelativeDimension` for an example. -/
-@[algebraize testProperty4.toAlgebra]
-def RingHom.testProperty4 (n : ℕ) {A B : Type*} [CommRing A] [CommRing B] (_ : A →+* B) : Prop :=
+@[algebraize RingHom.TestProperty4.toAlgebra]
+def RingHom.TestProperty4 (n : ℕ) {A B : Type*} [CommRing A] [CommRing B] (_ : A →+* B) : Prop :=
   ∀ m, n = m
 
-lemma testProperty4.toAlgebra (n : ℕ) {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B)
-    (hf : f.testProperty4 n) :
+lemma RingHom.TestProperty4.toAlgebra (n : ℕ) {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B)
+    (hf : f.TestProperty4 n) :
     letI : Algebra A B := f.toAlgebra
-    Algebra.testProperty4 n A B :=
+    Algebra.TestProperty4 n A B :=
       letI : Algebra A B := f.toAlgebra
       { out := hf }
 
@@ -78,7 +78,7 @@ example (A B : Type*) [CommRing A] [CommRing B] (f : A →+* B) : True := by
   fail_if_success -- Check that this instance is not available by default
     have h : Algebra A B := inferInstance
   algebraize [f']
-  guard_hyp algInst := f'.toAlgebra
+  guard_hyp algInst :=ₛ f'.toAlgebra
   trivial
 
 /-- Synthesize algebra instance from a composition -/
@@ -99,35 +99,113 @@ example (A B C : Type*) [CommRing A] [CommRing B] [CommRing C] (f : A →+* B) (
   guard_hyp scalarTowerInst := IsScalarTower.of_algebraMap_eq' rfl
   trivial
 
-example (A B : Type*) [CommRing A] [CommRing B] (f : A →+* B) (hf : f.testProperty1) : True := by
+example (A B : Type*) [CommRing A] [CommRing B] (f g : A →+* B) (hf : f.TestProperty1)
+    (hg : g.TestProperty1) : True := by
   algebraize [f]
-  guard_hyp algebraizeInst : Algebra.testProperty1 A B
+  guard_hyp algebraizeInst : @Algebra.TestProperty1 A B _ _ f.toAlgebra
+  fail_if_success
+    guard_hyp algebraizeInst_1
   trivial
 
-example (A B : Type*) [CommRing A] [CommRing B] (f : A →+* B) (hf : f.testProperty2) : True := by
+example (A B : Type*) [CommRing A] [CommRing B] (f g : A →+* B) (hf : f.TestProperty2)
+    (hg : g.TestProperty2) : True := by
   algebraize [f]
-  guard_hyp algebraizeInst : Module.testProperty2 A B
+  guard_hyp algebraizeInst : @Module.TestProperty2 A B _ _ f.toAlgebra.toModule
+  fail_if_success
+    guard_hyp algebraizeInst_1
   trivial
 
-example (A B : Type*) [CommRing A] [CommRing B] (f : A →+* B) (hf : f.testProperty3) : True := by
+example (A B : Type*) [CommRing A] [CommRing B] (f g : A →+* B) (hf : f.TestProperty3)
+    (hg : g.TestProperty3) : True := by
   algebraize [f]
-  guard_hyp algebraizeInst : Algebra.testProperty3 A B
+  guard_hyp algebraizeInst : @Algebra.TestProperty3 A B _ _ f.toAlgebra
+  fail_if_success
+    guard_hyp algebraizeInst_1
   trivial
 
-example (n : ℕ) (A B : Type*) [CommRing A] [CommRing B] (f : A →+* B) (hf : f.testProperty4 n) :
-    True := by
+example (n m : ℕ) (A B : Type*) [CommRing A] [CommRing B] (f g : A →+* B) (hf : f.TestProperty4 n)
+    (hg : g.TestProperty4 m) : True := by
   algebraize [f]
-  guard_hyp algebraizeInst : Algebra.testProperty4 n A B
+  guard_hyp algebraizeInst : Algebra.TestProperty4 n A B
+  fail_if_success
+    guard_hyp algebraizeInst_1
   trivial
 
 /-- Synthesize from morphism property of a composition (and check that tower is also synthesized). -/
 example (A B C : Type*) [CommRing A] [CommRing B] [CommRing C] (f : A →+* B) (g : B →+* C)
-    (hfg : (g.comp f).testProperty1) : True := by
+    (hfg : (g.comp f).TestProperty1) : True := by
   fail_if_success -- Check that this instance is not available by default
     have h : Algebra.Flat A C := inferInstance
   fail_if_success
     have h : IsScalarTower A B C := inferInstance
   algebraize [f, g, g.comp f]
-  guard_hyp algebraizeInst : Algebra.testProperty1 A C
+  guard_hyp algebraizeInst : Algebra.TestProperty1 A C
   guard_hyp scalarTowerInst := IsScalarTower.of_algebraMap_eq' rfl
   trivial
+
+section
+/- Test that the algebraize tactic also works on non-RingHom types -/
+
+structure Bar (A B : Type*) [CommRing A] [CommRing B] where
+  f : A →+* B
+
+@[algebraize testProperty1_of_bar]
+def Bar.TestProperty1 {A B : Type*} [CommRing A] [CommRing B] (b : Bar A B) : Prop :=
+  ∀ z, b.f z = 0
+
+lemma testProperty1_of_bar {A B : Type*} [CommRing A] [CommRing B] (b : Bar A B) (h : b.TestProperty1) :
+  @Algebra.TestProperty1 A B _ _ b.f.toAlgebra := @Algebra.TestProperty1.mk A B _ _ b.f.toAlgebra h
+
+@[algebraize testProperty2_of_bar]
+def Bar.testProperty2 {A B : Type*} [CommRing A] [CommRing B] (b : Bar A B) : Prop :=
+  letI : Algebra A B := b.f.toAlgebra;
+  ∀ (r : A) (M : B), r • M = 0
+
+lemma testProperty2_of_bar {A B : Type*} [CommRing A] [CommRing B] (b : Bar A B) (h : b.testProperty2) :
+  @Module.TestProperty2 A B _ _ b.f.toAlgebra.toModule :=
+    @Module.TestProperty2.mk A B _ _ b.f.toAlgebra.toModule h
+
+example {A B : Type*} [CommRing A] [CommRing B] (b c : Bar A B) (hb : b.TestProperty1)
+    (hc : c.TestProperty1) : True := by
+  algebraize [b.f]
+  guard_hyp algebraizeInst : @Algebra.TestProperty1 A B _ _ b.f.toAlgebra
+  fail_if_success -- make sure that only arguments are used
+    guard_hyp algebraizeInst_1 : @Algebra.testProperty1 A B _ _ c.f.toAlgebra
+  trivial
+
+example {A B : Type*} [CommRing A] [CommRing B] (b c : Bar A B) (hb : b.testProperty2)
+    (hc : c.testProperty2) : True := by
+  algebraize [b.f]
+  guard_hyp algebraizeInst : @Module.TestProperty2 A B _ _ b.f.toAlgebra.toModule
+  fail_if_success
+    guard_hyp algebraizeInst_1 --: @Module.testProperty2 A B _ _ c.f.toAlgebra.toModule
+  trivial
+
+structure Buz (A B : Type*) [CommRing A] [CommRing B] where
+  x : (A →+* B) ⊕ (A →+* B)
+
+@[algebraize testProperty1_of_buz_inl]
+def Buz.TestProperty1 {A B : Type*} [CommRing A] [CommRing B] (b : Buz A B) :=
+  b.x.elim (@Algebra.TestProperty1 A B _ _ ·.toAlgebra) (fun _ => False)
+
+lemma testProperty1_of_buz_inl {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B) :
+  Buz.TestProperty1 ⟨.inl f⟩ → @Algebra.TestProperty1 A B _ _ f.toAlgebra := id
+
+-- check that this also works when the argument *contains* a ringhom
+example {A B : Type*} [CommRing A] [CommRing B] (f g : A →+* B)
+    (hf : Buz.TestProperty1 ⟨.inl f⟩) (hg : Buz.TestProperty1 ⟨.inl g⟩) : True := by
+  algebraize [f]
+  guard_hyp algebraizeInst : @Algebra.TestProperty1 A B _ _ f.toAlgebra
+  fail_if_success
+    guard_hyp algebraizeInst_1 --: @Algebra.testProperty1 A B _ _ g.toAlgebra
+  trivial
+
+-- check that there is no issue with trying the lemma on a mismatching argument.
+example {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B)
+    (hf : Buz.TestProperty1 ⟨.inr f⟩) : True := by
+  algebraize [f] -- this could error if it tried applying `testProperty1_ofBuz_inl` to `hf`
+  fail_if_success
+    guard_hyp algebraizeInst
+  trivial
+
+end