making implicit variable explicit in output

Stream: Is there code for X?

[Filippo A. E. Nuccio]

When applying a certain lemma (notably docs#finset.le_max'), the conclusion contains and underscore that I can't turn into something more explicit. My question is not about these finset.max' issues, but about the underscore, it just so happens that I met the problem while playing with finsets. A MWE is the following

import tactic

open finset

example (A : finset ℕ) (H : finset.nonempty A) (a B : ℕ) (ha : a ∈ A) (hB : B = A.max' H) :
  a ≤ B.succ :=
begin
  have one := A.le_max' a ha,
  have two := nat.le_succ (A.max' H),
  have three := one.trans two,
  rwa [← hB] at three,
end

which works, but

import tactic

open finset

example (A : finset ℕ) (H : finset.nonempty A) (a B : ℕ) (ha : a ∈ A) (hB : B = A.max' H) :
begin
  a ≤ B.succ :=
  have := (A.le_max' a ha).trans (nat.le_succ (A.max' H)),
  rw [← hB] at this, -- rewrite tactic failed, did not find instance of the pattern in the target expression
  --A.max' H
end

does not (if I replace rw [← hB] at this by erw [← hB] at this, everything is fine, but that is not the point of my question). The funny thing is that in the first example, after introducing one and two, their transitive composition is three : a ≤ (A.max' H).succ whereas in the second example the "direct" transitive composition is this : a ≤ (A.max' _).succ.

So my questions are

1. Is there a way to force Lean to remember what the underscore was even if the conclusion of thelemma contains a _?
2. Why is the transitive composition of one and two remembering H, whereas the direct composition does not?
3. Is there a reason why in mathlib we prefer (if I undestand correctly) the version of the lemma with the _?

[Reid Barton]

It's not really an "underscore" in finset.le_max', the documentation generator is just printing it that way for some reason.

[Reid Barton]

Does rw not understand definitional proof irrelevance?

[Reid Barton]

You should probably write an expected type on the have (involving H), then the rw works fine

[Patrick Johnson]

1. Is there a way to force Lean to remember what the underscore was even if the conclusion of the lemma contains a _?

Underscore is not a thing in the type theory. It's just a pretty-print feature that hides complicated proofs (because of proof irrelevance). Lean knows how each underscore is constructed and you can extract a proof as an assumption using generalize_proofs tactic. You can either do

have : a ≤ (A.max' H).succ := (A.le_max' a ha).trans (nat.le_succ (A.max' H)),
rw ←hB at this,

or

have := (A.le_max' a ha).trans (nat.le_succ (A.max' H)),
generalize_proofs at this,
rw ←hB at this,

[Filippo A. E. Nuccio]

Thanks!

[Riccardo Brasca]

Does set_option pp.proofs true help?

[Patrick Johnson]

2. Why is the transitive composition of one and two remembering H, whereas the direct composition does not?

The underscore from A.le_max' a ha is Exists.intro a ha, which is definitionally equal to the proof of A.nonempty (because ∃ (x : ℕ), x ∈ A is definitionally equal to A.nonempty).

When you write have two := nat.le_succ (A.max' H), the type includes H because you explicitly used H to construct the proof. On the other hand, when you write have three := (A.le_max' a ha).trans (nat.le_succ (A.max' H)), the proof of H gets unified with Exists.intro a ha (because they are defeq). Since there is no (syntactically equal) proof of Exists.intro a ha in the assumptions, it gets displayed as underscore and rw gets confused.

[Patrick Johnson]

3. Is there a reason why in mathlib we prefer (if I undestand correctly) the version of the lemma with the _?

finset.le_max' could be defined in a slightly different way to avoid underscores:

lemma finset.le_max' {α : Sort*} [linear_order α] (s : finset α) (x : α) (h : x ∈ s) :
  ∃ h₁, x ≤ s.max' h₁ :=
Exists.intro ⟨_, h⟩ (le_max_of_mem h (option.get_mem _))

Use it with (A.le_max' a ha).some_spec

[Yaël Dillies]

This cause problem in Lean 3 however because we don't have eta expansion.

[Yaël Dillies]

No, I am not making sense.

[Yaël Dillies]

What about using a default argument?

lemma le_max' {α : Type*} [linear_order α] (s : finset α) (x : α) (hx : x ∈ s)
  (h : s.nonempty := ⟨x, hx⟩) :
  x ≤ s.max' h := sorry

[Reid Barton]

What's the rationale for rw not working in the second example considering that the types match up to definitional proof irrelevance?

[Reid Barton]

Is it that rw might want to inspect the proof argument to infer the values of some non-propositional variables?

[Reid Barton]

Would it make sense for rw to treat the proof as irrelevant as a fallback option?

[Patrick Johnson]

Simplified example:

import data.finset.basic

example {α : Type} {s : finset α} {f : s.nonempty → ℕ}
  {h₁ : s.nonempty}
  {h₂ : ∃ (a : α), a ∈ s}
  (h₃ : f h₁ = 0) :
  f h₂ = 0 :=
begin
  rw h₃, -- fails
end

Seems like rw does not unfold finset.nonempty

[Reid Barton]

That's interesting and not what I thought was happening but, in some ways, leaves me more confused!

[Reid Barton]

Namely, it does work with h₂ : s.nonempty instead

[Filippo A. E. Nuccio]

Very interesting, thank you very much. I am not sure I fully understand your answer to point 2., but that is my lack of knowledge. I will read carefully and try to come back if I need further clarification. :working_on_it:

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Does set_option pp.proofs true help?

No, unfortunately it does not, because with this option instead of

have := (A.le_max' a ha).trans (nat.le_succ (A.max' H)), -- a ≤ (A.max' _).succ

I find

have := (A.le_max' a ha).trans (nat.le_succ (A.max' H)), -- a ≤ (A.max' (Exists.intro a ha)).succ

which (much in the spirit of @Patrick Johnson 's suggestions) is not matched neither when doing rw ← hB (for hB : B = A.max' H).