Lean4
/-- Given a Type `R` with instances for each of the `Ring` operations, make a
`Language.ring.Structure R` instance, along with a proof that the operations given
by the `Language.ring.Structure` are the same as those given by the `Add` or `Mul` etc.
instances.
This definition can be used when applying a theorem about the model theory of rings
to a literal ring `R`, by writing `let _ := compatibleRingOfRing R`. After this, if,
for example, `R` is a field, then Lean will be able to find the instance for
`Theory.field.Model R`, and it will be possible to apply theorems about the model theory
of fields.
This is a `def` and not an `instance`, because the path
`Ring` => `Language.ring.Structure` => `Ring` cannot be made to
commute by definition
-/
def compatibleRingOfRing (R : Type*) [Add R] [Mul R] [Neg R] [One R] [Zero R] : CompatibleRing R :=
{ funMap := fun {n} f =>
match n, f with
| _, .add => fun x => x 0 + x 1
| _, .mul => fun x => x 0 * x 1
| _, .neg => fun x => -x 0
| _, .zero => fun _ => 0
| _, .one => fun _ => 1
funMap_add := fun _ => rfl, funMap_mul := fun _ => rfl, funMap_neg := fun _ => rfl, funMap_zero := fun _ => rfl,
funMap_one := fun _ => rfl }
