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.