What does the `ematch` attribute do?

Stream: general

[Kevin Buzzard]

I thought I'd try and figure out what ematch did because I can't find out how to look it up. I searched in mathlib and the first occurrence I found was that one_mul is tagged ematch; the second was in algebra.group_power.lemmas where on line 104 Mario wrote local attribute [ematch] le_of_lt 4 years ago. I commented the line out. The file still compiles. zero_mul is tagged with it, and then the next occurrence is another local le_of_lt in algebra.group_with_zero.power and again if I comment it out then nothing breaks. These are local attributes so they're genuinely doing nothing at all, right? le_Sup has it too in order.complete_lattice and I commented that one out and the file still compiled (but this was global so it might have broken something else).

So what does ematch do? Anything at all??

[Kyle Miller]

I remember finish having a docstring about how one of the things it does is package things up for SMT solving, and it has something to do with ematch lemmas.

[Kyle Miller]

Maybe it's like the quantifier instantiation described in the Z3 tutorial https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-e-matching-based-quantifier-instantiation

[Kevin Buzzard]

So poking around the git history I wonder whether at some point finish was used to prove a bunch of lemmas, and then lower-level proofs were found but the attribute was never removed from le_of_lt.

[Kyle Miller]

I plugged in the axioms of the group $S_3$ to see what finish could do. With the ematch lemmas I gave it, it doesn't seem to be able to always solve the word problem, but, still, it's able to automatically prove more than I expected. I didn't realize this was within the purview of finish.

axiom G : Type
constants (e σ τ : G)
constant mul : G → G → G
constant inv : G → G
@[ematch]
constant assoc : Π (a b c : G), mul (mul a b) c = mul a (mul b c)
@[ematch]
constant mul_one : Π (a : G), mul a e = a
@[ematch]
constant one_mul : Π (a : G), mul e a = a
@[ematch]
constant inv_mul : Π (a : G), mul (inv a) a = e
@[ematch]
constant mul_inv : Π (a : G), mul a (inv a) = e

@[ematch]
constant ax1 : mul τ τ = e
@[ematch]
constant ax2 : mul (mul σ σ) σ = e
@[ematch]
constant ax3 : mul σ τ = mul τ (inv σ)

lemma test : mul (mul τ σ) τ = inv σ :=
begin
  finish
end