Make `apply?` show more than one result upon success?

Stream: general

[Markus de Medeiros]

I'm in a situation where I often have to use apply .trans Y. If I want to look for a selection of possible Y's, I'd like to do something like apply .trans (by apply?), but apply? always just gives me rfl and gives up! Is there any way to change this behavior?

[Shreyas Srinivas]

One easy workaround might be to just call apply? in the next line

[Shreyas Srinivas]

Like so:

example (h₁ : x = y) (h₂ : y = z) : x = z := by
  apply Eq.trans
  apply?

[Shreyas Srinivas]

This also works:

example (h₁ : x = y) (h₂ : y = z) : x = z := by
  apply (Eq.trans (by apply?) (by apply?))

[Shreyas Srinivas]

I tried to replicate the behaviour you describe but it only happened when the goal was wrong. For example here:

import Mathlib

example {x y z : ℝ} (h₁ : x < y) (h₂ : y < z) : x = z := by
  apply Eq.trans (by apply?)

[Markus de Medeiros]

Ah, I actually misunderstood my problem somewhat. It's not that it gives me rfl, but that it gives me .rfl, which is a term in the equivalence relation I'm using. Here's a more concrete example:

-- Boilerplate
abbrev Relation (α : Type _) := α → α → Prop
class Transitive (R : Relation α) where
  trans {x y z : α} : R x y → R y z → R x z

-- Example: Want to find the proof HT1.trans HT2
variable (T : Type) (R : Relation T) [Transitive R]
variable (t1 t2 t3 t4 : T) (HTbad : R t1 t4) (HT1 : R t1 t2) (HT2 : R t2 t3)
example : R t1 t3 := by
  apply Transitive.trans
  · apply?
    -- Messages (2)
    -- mathlib-demo.lean:16:4
    -- Try this: exact HTbad
  all_goals sorry

You can see that apply? gives up after finding HTbad, which works but is not what I'm looking for. I'm also wondering if there's something I can do to seek out HT1 as well.

[Markus de Medeiros]

The analogue in this case is rw?(as a sidenote, the people working on generalized rewriting should think about adding this capability as well!)

[Shreyas Srinivas]

Right, so what's wrong with apply? is that, at least as far as local hypothesis are concerned, it looks at the hypotheses in the order of appearance and just applies the first one in sequence. This is also what rw? is doing at present

[Shreyas Srinivas]

See the following examples:

import Mathlib

example {x y z w : ℝ} (h₀ : x = w) (h₁ : x = y) (h₂ : y = z) : x = z := by
  apply Eq.trans (by apply?)

example {x y z w : ℝ} (h₀ : x = w) (h₁ : x = y) (h₂ : y = z) : x = z := by
  rw?

[Shreyas Srinivas]

you can check this by adding similar dummy hypothesis and changing their order of appearance

[Shreyas Srinivas]

For example, here I just changed the order of h0 and h1 and suddenly it finds the correct hypothesis:

example {x y z w s : ℝ} (h₁ : x = y) (h₀ : x = w) (h₂ : y = z) : x = z := by
  apply Eq.trans (by apply?)

[Shreyas Srinivas]

In contrast, simp_all only finds the entire proof

[Markus de Medeiros]

In your example rw? tells you both that you could apply h0 or h1, whereas apply? only tells you that you could apply h0 because that closes the goal, despite the fact that there are other ways close the goal.

[Shreyas Srinivas]

Right that's true. apply? can also give you a long list of examples in general.

[Markus de Medeiros]

Do you know of any way to make it give you that list even when one of them closes the goal?

[Markus de Medeiros]

It's not a huge deal or anything but that's what I'm after.

[Shreyas Srinivas]

you can do something apply Eq.trans using h1

[Shreyas Srinivas]

example {x y z w s : ℝ} (h₀ : x = w) (h₁ : x = y)  (h₂ : y = z) : x = z := by
  apply Eq.trans (by apply? using h₁)

[Shreyas Srinivas]

But I don't know any standard way to change how apply? lists its options

[Shreyas Srinivas]

arguably using is already modifying this listing by suggesting the hypotheses to use as early as possible in some intuitive sense.

[Chase Norman]

Not sure if this is helpful, but Canonical can generate this term. If you want to explore the tree of possible applications, canonical +refine can do this. If you just want a list of terms, canonical (count := 10) can do this.

-- Example: Want to find the proof HT1.trans HT2
variable (T : Type) (R : Relation T) [Transitive R]
variable (t1 t2 t3 t4 : T) (HTbad : R t1 t4) (HT1 : R t1 t2) (HT2 : R t2 t3)
example : R t1 t3 := by
  -- canonical
  exact Transitive.trans HT1 HT2

[Shreyas Srinivas]

simp_all already handles this goal. I think Markus is specifically keen on getting apply? to list alternatives in the same way as rw? does. In this case, apply? doesn’t even offer HT1 as a second option