feat(ModelTheory): add DefinablePred for fun_prop automation

[staroperator]

This PR adds DefinablePred. It is the same as Definable, except the latter applies on Set (α → M) and the former applies on (α → M) → Prop. There main reason to add this is that I want to automate the definability proof of predicates, and that fun_prop works on functions (that include predicates) but not on sets.

For example, with appropriate fun_prop lemmas added, one can automate definability result like this:

theorem IsLinearSet.definable [Finite α] (hs : IsLinearSet s) : A.Definable presburger s := by
  ...
  -- ⊢ A.DefinablePred presburger fun x ↦
  --   ∃ y, (∃ a, ∀ (x : α), y x = ∑ x_1, a x_1 * ↑x_1 x) ∧ ∀ (x_1 : α), v x_1 + y x_1 = x x_1
  fun_prop

This PR also removes certain fun_prop tags that would or should not be used in automation.

---

Note: one may argue that we don't need a new definition if we use aesop instead of fun_prop. However, in that case, we still need to write lemmas for {x | p x} targets (e.g. for {x | p x ∧ q x}), which have almost no difference with lemmas on p or fun x => p x ∧ q x directly.

• depends on: refactor(ModelTheory): add typeclasses for algebraic symbols #38393

[github-actions]

PR summary c3e588b468

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.ModelTheory.Algebra.Ring.Basic	698	701	+3 (+0.43%)
Mathlib.ModelTheory.Arithmetic.Presburger.Basic	705	708	+3 (+0.43%)

Import changes for all files

Files	Import difference
4 files Mathlib.FieldTheory.AxGrothendieck Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.ModelTheory.Arithmetic.Presburger.Definability	1
5 files Mathlib.ModelTheory.Algebra.Field.Basic Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Ring.Basic Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.ModelTheory.Arithmetic.Presburger.Basic	3
Mathlib.ModelTheory.Algebra.Classes (new file)	698

---

Declarations diff

+ AddFunction
+ CompatibleAdd
+ CompatibleInv
+ CompatibleMul
+ CompatibleNeg
+ CompatibleOne
+ CompatibleZero
+ Constants.one
+ Definable.of_definablePred
+ Definable.preimage_map
+ DefinableFun.const
+ DefinableFun.finsetProd
+ DefinableFun.inv
+ DefinableFun.mul
+ DefinableFun.mul_nat
+ DefinableFun.natCast
+ DefinableFun.nat_mul
+ DefinableFun.npow
+ DefinableFun.one
+ DefinablePred
+ DefinablePred.and
+ DefinablePred.comp
+ DefinablePred.const
+ DefinablePred.const_eq
+ DefinablePred.eq
+ DefinablePred.eq_const
+ DefinablePred.exists
+ DefinablePred.exists_finite
+ DefinablePred.exists_pi
+ DefinablePred.forall
+ DefinablePred.forall_finite
+ DefinablePred.forall_pi
+ DefinablePred.iff
+ DefinablePred.imp
+ DefinablePred.not
+ DefinablePred.of_definable
+ DefinablePred.or
+ DefinablePred.rel
+ Functions.inv
+ Functions.mul
+ InvFunction
+ MulFunction
+ NegFunction
+ OneConstant
+ ZeroConstant
+ _root_.FirstOrder.Language.Formula.definablePred_realize
+ _root_.Set.DefinablePred.le
+ _root_.Set.DefinablePred.lt
+ instance : AddFunction presburger := ⟨presburgerFunc.add⟩
+ instance : AddFunction ring := ⟨ringFunc.add⟩
+ instance : MulFunction ring := ⟨ringFunc.mul⟩
+ instance : NatCast (L.Term α)
+ instance : NegFunction ring := ⟨ringFunc.neg⟩
+ instance : OneConstant presburger := ⟨presburgerFunc.one⟩
+ instance : OneConstant ring := ⟨ringFunc.one⟩
+ instance : Pow (L.Term α) ℕ
+ instance : ZeroConstant presburger := ⟨presburgerFunc.zero⟩
+ instance : ZeroConstant ring := ⟨ringFunc.zero⟩
+ instance [InvFunction L] : Inv (L.Term α)
+ instance [MulFunction L] : Mul (L.Term α)
+ instance [OneConstant L] : One (L.Term α)
+ instance {M : Type*} [Zero M] [One M] [Add M] : CompatibleAdd presburger M
+ instance {M : Type*} [Zero M] [One M] [Add M] : CompatibleOne presburger M
+ instance {M : Type*} [Zero M] [One M] [Add M] : CompatibleZero presburger M
+ instance {M : Type*} [Zero M] [One M] [Add M] : presburger.Structure M
+ inv_def
+ mul_eq
+ neg_eq
+ pow_succ
+ pow_zero
+ prod
+ realize_inv
+ realize_npow
+ realize_prod
++ add_eq
++ one_eq
++ zero_eq
- _root_.Set.Definable.preimage_map
- addFunc
- add_def
- funMap_add
- funMap_one
- funMap_zero
- instance (α : Type*) : Add (Language.ring.Term α)
- instance (α : Type*) : Mul (Language.ring.Term α)
- instance (α : Type*) : Neg (Language.ring.Term α)
- instance (α : Type*) : One (Language.ring.Term α)
- instance (α : Type*) : Zero (Language.ring.Term α)
- instance : Add (presburger.Term α)
- instance : NatCast (presburger.Term α)
- instance : One (presburger.Term α)
- instance : SMul ℕ (presburger.Term α)
- instance : Zero (presburger.Term α)
- instance : presburger.Structure M
- mulFunc
- negFunc
- neg_def
- oneFunc
- realize_neg
- realize_nsmul
- realize_sum
- succ_nsmul
- sum
- zeroFunc
- zero_def
- zero_nsmul
-- realize_add
-- realize_zero
--+ realize_one

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
6533	-1	backward.isDefEq.respectTransparency

Current commit 75c6194de2
Reference commit c3e588b468

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• refactor(ModelTheory): add typeclasses for algebraic symbols #38393
  By Dependent Issues (🤖). Happy coding!