ext?

Stream: Is there code for X?

[Kenny Lau]

Is it possible to implement ext??
Presumably it would have a clickable text to convert it to refine [ext_lemma] fun i ↦ ?_

[Aaron Liu]

Of course, it is possible

[Yaël Dillies]

IMO it would be much more productive if you started opening issues instead (or at the conclusion) of all those threads

[Riccardo Brasca]

In my experience show_term ext works very well, so this may be very easy.

[Kenny Lau]

Yaël Dillies said:

IMO it would be much more productive if you started opening issues instead (or at the conclusion) of all those threads

https://github.com/leanprover-community/mathlib4/issues/26042

[Aaron Liu]

Riccardo Brasca said:

In my experience show_term ext works very well, so this may be very easy.

In my experience, this does not work very well, because of delayed assignment hiding what happens under binders.

[Aaron Liu]

example : ∀ (x y z : Nat), True := by
  -- Try this: refine fun x ↦ ?_
  show_term intro x y z

[Yaël Dillies]

Do you have an example with show_term ext specifically, though?

[Kenny Lau]

@Yaël Dillies

import Mathlib

lemma test {X Y Z : Type*} (f g : X → Y → Z) : f = g := by
  ext x y
  -- ⊢ f x y = g x y
  sorry

lemma test' {X Y Z : Type*} (f g : X → Y → Z) : f = g := by
  show_term ext x y
  -- Try this: refine funext fun x ↦ ?_
  sorry

[Yaël Dillies]

Sounds like it's a bug in show_term though, and implementing ext? as doing the same thing as show_term ext is correct

[Damiano Testa]

by the way, by? performs better.

[Aaron Liu]

That's because it sorrys at the end, which fills all the metavariables

[Kyle Miller]

Mathlib could implement ext? as show_term ext

I think any implementation of ext? would be using the pretty printer. @Aaron Liu's point about limitations of the pretty printer are valid, but I'm not sure if that has any bearing on ext? per se.

(Aaron: If you've got a good handle on delayed assignments, do you want to try experimenting with making a delayed assignment forcer? The idea would be to have a more aggressive instantiateMVars that takes the assigned value of a delayed assignment and then reabsracts it in the current context. If we get a good efficient one, we could add it as a pretty printer option. Alternatively, the pretty printer could attempt to pretty print delayed assignment values, but I've hesitated implementing it that way because that not obviously correct...)

[Aaron Liu]

I guess it's time to learn delayed assignments

[Kyle Miller]

The source code to instantiateMVars from sometime last year, before it was moved to C++, is informative. Feel free to ping me with questions.

[Kenny Lau]

Kyle Miller said:

@Aaron Liu's point about limitations of the pretty printer are valid, but I'm not sure if that has any bearing on ext? per se.

I'm not sure if I understand this point. This leads to the result of ext? producing a different result from the ext call.

[Kyle Miller]

Given a delayed assignment ?n fvars := ?m, where ?m is the original metavariable, it might work to simply take ?m, see if it has an assignment ?m := v, and if so, then replace ?n x1 ... xn with (<- mkLambdaFVars fvars v).headBeta #[x1, ..., xn], after recursively expanding v with the same process. The mkLambdaFVars would be responsible for creating some new delayed assignments — but these would be at the synthetic opaque metavariables, so for pretty printing purposes it is exactly what we want.

There are some complications though, with the way let variables are handled with delayed abstractions. The top of MetavarContext.lean has a long module doc with the "gruesome details", and within there is a small comment about how actually assigning ?n itself "may not even be type correct". That's a very important subtle detail here (one which I only really appreciated in the last few weeks). I haven't thought through whether this is important here. In short: for lets, the system assumes that the value passed to ?n is defeq to what the local context of ?m says it should be.

[Kyle Miller]

Kenny Lau said:

This leads to the result of ext? producing a different result from the ext call.

Yes, certainly, but what is ext? supposed to do except use the pretty printer with the term it produced?

[Kyle Miller]

show_term is simply a frontend to the pretty printer

[Kenny Lau]

Kyle Miller said:

Kenny Lau said:

This leads to the result of ext? producing a different result from the ext call.

Yes, certainly, but what is ext? supposed to do except use the pretty printer with the term it produced?

but isn't funext fun x ↦ funext fun y ↦ ?_ the term produced?

lemma test {X Y Z : Type*} (f g : X → Y → Z) : f = g := by
  ext x y
  -- ⊢ f x y = g x y
  sorry
#print test
/-
theorem test.{u_1, u_2, u_3} : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f g : X → Y → Z), f = g :=
fun {X} {Y} {Z} f g ↦ funext fun x ↦ funext fun y ↦ sorry
-/

[Aaron Liu]

Kyle Miller said:

In short: for lets, the system assumes that the value passed to ?n is defeq to what the local context of ?m says it should be.

This is so much fun

/--
warning: declaration uses 'sorry'
---
error: (kernel) application type mismatch
  [1, 2][k]
argument has type
  1 < [1, 2].length
but function has type
  (fun as i ↦ i < as.length) [1, 2] k → ℕ
-/
#guard_msgs in
example : ∃ P : Prop, P := by
  refine ⟨?P, ?_⟩
  refine let k := 1; ?_
  swap
  rw [Classical.choose_spec (show ∃ x, 1 = x from ⟨1, rfl⟩)]
  swap
  exact [1, 2][k] = 2
  intro k
  sorry

[Kyle Miller]

@Aaron Liu Feel free to post more examples to lean4#8488

[Kyle Miller]

@Kenny Lau Unless you want to get into the weeds of delayed assignments, the short answer is "yes, that's the term it produced, but partial proofs with binders are complicated and confuse the pretty printer".

This is a fundamental problem that, if the pretty printer can't handle it, I don't see how ext? would do any better.

[Kenny Lau]

@Kyle Miller I do not want to get into the details, but, could we instead have two refines? As in, I assume ext is secretly doing:?

refine funext fun x ↦ ?_
refine funext fun y ↦ ?_

[Kenny Lau]

as in, I assume that we can do a tactic based on show_term that keeps calling ext afterwards and recording the new proofs

[Kyle Miller]

That would be reasonable for ext?. For that, it could even do funext x; funext y.

It all depends what you want from ext? though. Is the point getting a proof term? Or to use simple tactics? Or only refines? Or what?

[Kenny Lau]

@Kyle Miller only refine.

[Kyle Miller]

I think you need to justify that, given that there are lots of options in this design space.

[Kyle Miller]

Especially since you're talking about using multiple refines rather than a single refine. Why is that better? Is it what you'd want more in general? Or is it only a way to work around the pretty printer?

[Kenny Lau]

@Kyle Miller It's because refine is the most commonly used low-level tactic, and outputting multiple refines allows the user (i.e. me) to chain them together manually. honestly, the point was just so that I know which ext lemma it used, so that I can convert the tactic proof manually to a term.

[Kenny Lau]

as long as it can give me a list of the @[ext] lemmas used, I'm fine with whatever it outputs

[Kyle Miller]

What I'm hearing is that if show_term could show the whole partial proof, you would have no need for ext?, right?

[Kyle Miller]

That's the general approach, and otherwise we're in a situation where every single tactic has a ? variant.

[Kenny Lau]

yes, well, i also didn't know that show_term (and also by?) existed prior to this thread :slight_smile:

[Kyle Miller]

@Aaron Liu Another approach to this pretty printing problem, instead of a delayed assignment forcer, could be to have a pretty printer pass that assigns some dummy values to every leaf metavariable. Those dummy values could record the mvarids so that they can print as the correct expression.

The delayed assignment forcer could still be useful though, to get some defeqs to go through that otherwise wouldn't (since delayed assignments are effectively opaque)

[Mario Carneiro]

I believe ext? used to exist in lean 3, and it would not just do show_term (I don't see the point of that), it would suggest the pattern to use after ext. There was something similar for rintro and rcases