TryThis uses the '⋯' token from elided proofs

Stream: lean4

[Andrés Goens]

I was trying @Joachim Breitner's Calcify to golf this proof in the #Equational project, and it gives me some elided proofs back as ⋯. I presume it's a bug with TryThis and not Calcify although I wasn't sure. (Should this return the full proofs or just _s?)

The example was just this:

-- FIXME: golf this!
theorem FreeMagma.EvalFreeMagmaWithLawsUniversalProperty {α G} {Γ : Ctx α}
(φ : α → G) [ginst : Magma G] (modelsG : G ⊧ Γ)(ψ : FreeMagmaWithLaws α Γ →◇ G) :
    ψ ∘ (⟦.⟧) ∘ Lf = φ → FreeMagmaWithLaws.eval φ modelsG = ψ := by
  intro eq
  let ψ' := (FreeMagmaWithLaws.mkMor Γ).comp ψ
  let φ' := FreeMagmaWithLaws.eval φ modelsG ∘ (⟦.⟧)
  have h : φ' = ψ' := by
    calcify
    simp only [DFunLike.coe]
    rw [← EvalFreeMagmaUniversalProperty φ]
    . simp only [FreeMagmaWithLaws.eval, φ']
      exact funext fun x ↦ rfl
    . rw [← eq]
      simp only [MagmaHom.comp, FreeMagmaWithLaws.mkMor, ψ']
      rfl
  exact Quot.liftEq (s := _) _ _ h

Which gives:

Try this: calc
        Quotient.lift (evalInMagma φ) ⋯ ∘ fun x ↦ ⟦x⟧
        _ = Quotient.lift (evalInMagma φ) ⋯ ∘ fun x ↦ ⟦x⟧ := (funext fun x ↦ rfl)
        _ = ψ'.toFun :=
          EvalFreeMagmaUniversalProperty φ ψ'
            (Eq.mpr (id (congrArg (fun _a ↦ ψ'.toFun ∘ Lf = _a) (Eq.symm eq)))
              (id
                (Eq.refl
                  ((⇑ψ ∘ ⇑{ toFun := fun a ↦ ⟦a⟧, map_op' := FreeMagmaWithLaws.mkMor.proof_1 Γ }) ∘
                    Lf))))

Should I make an issue in core for this? Or is this a Calcify problem?

[Damiano Testa]

What happens if you add set_option pp.proofs true before calcify?

[Andrés Goens]

@Damiano Testa then it suggests the full proof terms correctly

[Damiano Testa]

So maybe this is a simple fix that could be embedded into calcify

[Andrés Goens]

I would think that TryThis should ignore (override) that option though, shouldn't it? Since the result is meant to be elaborated (or at least replace those with _s)

[Damiano Testa]

I'm not sure if it "should", but extract_goal also sets it's options in a similar way.

[Damiano Testa]

To me, it seems a feature, rather than a bug: you can get as verbose as you want, defaulting to the minimum.

[Joachim Breitner]

This is a problem also with show_term, right? ( Of which calcify is an extension in a way.) Maybe it's worth setting this by default, although I'd prefer to see a more thorough solution to this, i.e. a delaboration mode that reliably produces elaboratable terms without including all too much information.

[Jannis Limperg]

That's supposed to be pp.analyze, right?

[Damiano Testa]

There could be a calcify! version that sets the option.

[Andrés Goens]

Fair enough, let me rephrase, shouldn't TryThis replace the ⋯ tokens with _, if it's respecting the verbosity of pretty printing?

[Joachim Breitner]

Right, but as I understand it isn't fully reliable. But yes, maybe I should just set that flag and deflect further complaints to that feature :-)

[Damiano Testa]

As is, it already isn't fully reliable, so this is definitely a fix! :stuck_out_tongue_wink:

[Joachim Breitner]

I think try this already works on syntax, so it's too late there. But tools using trythis should set appropriate flags :-)

[Joachim Breitner]

Damiano Testa said:

There could be a calcify! version that sets the option.

I should write a Zulip bot that reacts with :bangbang: whenever someone suggests that the first variation of a tactic foo should be called foo! :-D

[Joachim Breitner]

Damiano Testa said:

As is, it already isn't fully reliable, so this is definitely a fix! :stuck_out_tongue_wink:

Does pp.analyze help in this particular case, @Andrés Goens?

[Andrés Goens]

nope, pp.analyze leaves the ⋯ s

[Andrés Goens]

(FWIW, since ⋯ is elaborated as _ this still works, i.e. it is elaborated, but it gives a warning about it)

[Johan Commelin]

Is pp.proofs relevant?

[Johan Commelin]

Sorry, I see that was already mentioned

[Kyle Miller]

Since this isn't really written anywhere all in one place, here's an overview of pretty printer options that omit terms using ⋯. (By the way, when hovering over a ⋯ in the Infoview, it tells you which option is responsible for it. Unfortunately this doesn't appear in the main "try this" string, but show_term prints it twice, and the second one is hoverable.)

• pp.proofs (default: false). When false, any proof that isn't "simple enough" according to pp.proofs.threshold is omitted. Side note: pp.proofs.type gives you a type ascription if you want it.
• pp.maxSteps (default: 5000). Once the pretty printer elaborates more than maxSteps expressions, terms start being omitted. This is a safeguard against extremely large terms overwhelming the Infoview.
• pp.deepTerms (default: false). When false, deep terms are omitted. "Depth" means elaboration recursion depth. The definition of deep is controlled by pp.deepTerms.threshold. There is a heuristic where "shallow" terms still get pretty printed, a notion also controlled by this threshold, which helps things like numeric literals still pretty print despite the actual expression exceeding the depth limit.

[Kyle Miller]

For show_term's "try this" suggestion, it seems to me that maxSteps and deepTerms should still be enabled, and it should be able to warn you when they've been activated. This is easy, since these options install OmissionInfo into the infotrees.

[Kyle Miller]

For pp.proofs, it's less clear to me what the correct thing to do is, and how it should interact with pp.analysis. I think pp.analysis should respect pp.proofs.

Something that's come to mind is that show_term should set pp.proofs to true and pp.analysis to true, and then pp.analysis could try to omit proofs itself with _ if they can be inferred from other arguments.

[Jason Reed]

Another source of ⋯ I just ran into is controllable by the boolean option pp.showLetValues and the nat-valued options pp.showLetValues.threshold and pp.showLetValues.tactic.threshold(cf. here for source and docstrings)

The use of the ellipsis seems to have been introduced in this comparatively recent PR, so text of the above thread was correct at the time it was written

Despite it being apparently hard to determine in emacs, firing up vscode and hovering over the ellipse led me straight to the cause. Thanks much for mentioning that that works!

[Kyle Miller]

Please let me know of any issues with showLetValues in the wild! It should show the values in the infoview when you're working with tactics, and otherwise it hides them. In my experience with the feature so far, I never even think about it.

[Jason Reed]

Oh, so does it constitute undesired behavior if my cursor is in the middle of a tactic proof, the infoview shows showLetValues-induced ellipses, and showLetValues is false? Because I do have an example of that. I can try to get it down to an #mwe in a second here... It didn't bother me since I could just set showLetValues to true in order to see the hidden terms, but if that's not how the feature is supposed to work I'm happy to help debug.

[Kyle Miller]

Oh, interesting, yeah that could be considered undesirable. I thought in that case though you'd still have the goal view (with values) but the "Expected type" context would be without values, which I think is acceptable and maybe preferred since it avoids duplicate information.

[Jason Reed]

Forgive the screenshot instead of text (and I do still promise an #mwe after my lunch finishes cooking and I can spare some more attention :) but just to resolve my uncertainty about which parts of the goal view you're referring to, here's what I'm seeing:
image.png

[Jason Reed]

If I move the cursor up or down one line (from 47 to 46 or 48), the ellipses vanish and the terms they are placeholders for reappear. That seems kind of weird to me.

[Kyle Miller]

Ok, this is a known issue, but not necessarily an issue with the feature. When you see this, it means that the tactics are creating the wrong kinds of metavariables, which is something we need to address (though a proper fix likely needs some new Lean features, so it's probably too early to report problems with individual tactics)

[Kyle Miller]

I decided to implement this feature in a way that does expose these tactic issues so that when we're ready to address them we have some visual indication that something isn't quite right. (I could have also implemented it in a way that was more robust to these tactic issues.)

Sorry for any confusion, and thanks for letting me know what you ran into!

[Jason Reed]

Huh, interesting! I'm not sure I fully understand yet, but thanks for explaining. The minimal version of what I'm seeing seems to be

import Mathlib

theorem foo : ∃ _ : ℕ, ∃ _ : ℕ, True ∨ False := by
  let some_term : Set ℕ := {x | x + x < 5};
  use 42
  let _ := 42
  use 42
  let _ := 42
  exact Or.inl trivial

where

• I expect, I guess, to see the value of some_term whenever I position the cursor after its definition
• I observe that if I position it at the end of a use tactic, I see the definition of some_term replaced by an ellipsis
• But I also observe that if I position it at the end of a let here, I see the full definition as expected.

[Jason Reed]

So maybe something funny is happening with metavariables created by use? I'm just pattern-matching on what you said, I don't yet have any knowledge of lean unification internals (although learning more about that is definitely on my list...)

[Jason Reed]

In any case, no worries about any confusion created, I'm perfectly happy with the set_option pp.showLetValues true workaround for now. Feel free to ping me on any future gh issue if the time becomes ripe to report.

[Kyle Miller]

Yes, use makes "natural" metavariables instead of "synthetic opaque"

[Kyle Miller]

If you want to contribute to mathlib, you might be able to fix it by adding an argument to forallMetaTelescopeReducing to have it use (kind := .syntheticOpaque), but also that might not be right...

[Jason Reed]

So noted, thanks!

[Kyle Miller]

At least where the goals are added with setGoals, you could add a loop that sets the metavariable kinds for all the metavariables being added to .syntheticOpaque

[Kyle Miller]

(That's the most straightforward I think.)