exact? failure

Stream: lean4

[Kevin Buzzard]

Bhavik pointed this out to me:

import Mathlib.Data.Real.Basic

example {x y : ℝ} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by exact? -- fails
-- le_antisymm hxy hyx

I would expect exact? to work here.

[Alex J. Best]

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Exact.3F.20fails.20on.20le_antisymm/near/388994247

[Kevin Buzzard]

Sorry, thanks.

[Alex J. Best]

Well actually it seems you posted first! I just happened to answer there :smile:

[Kevin Buzzard]

I understand now that exact? can fail on equalities. But this one was surprising to me -- am I making a slip?

import Mathlib.Algebra.BigOperators.Group.Finset

theorem prod_induction {α : Type*} {s : Finset α} {M : Type*} [CommMonoid M] (f : α → M)
    (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b))
    (unit : p 1) (base : ∀ x ∈ s, p <| f x) :
    p <| ∏ x ∈ s, f x := Finset.prod_induction f p hom unit base -- already there

theorem prod_induction' {α : Type*} {s : Finset α} {M : Type*} [CommMonoid M] (f : α → M)
    (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b))
    (unit : p 1) (base : ∀ x ∈ s, p <| f x) :
    p <| ∏ x ∈ s, f x := by exact? -- fails

[Kyle Miller]

I think docs#Finset.prod_induction is especially hard because it involves higher-order unification. Granted, it's an easy one (just use p) but it might be too much to ask.

I wonder if this could be special cased somehow? Or maybe there's some unification approximation setting that could help? I'm not sure.

[Kevin Buzzard]

I'm just annoyed that I spent 5 minutes proving it :-)

[Jovan Gerbscheid]

There is no way for the discrimination tree to pick the right lemma in this case, because the pattern of the conclusion of prod_induction is just a star. You're expecting exact? to pick the lemma because the goal is a proposition involving ∏ x ∈ s, f x, and this cannot be expressed in the discrimination tree.

Although this might be worth looking into for my refined discrimination tree to see if such a thing is feasible. Would you want it to work with any proposition involving ∏ x ∈ s, f x, or just for propositions of the form p <| ∏ x ∈ s, f x (where p is a variable or a constant)?

[Jovan Gerbscheid]

I think if exact? found the lemma prod_induction, it would succeed here. Is there a way to explicitly pass a lemma to exact? to check this?