pp_dot?

Stream: lean4

[Joachim Breitner]

Is there a way to nudge the elaborator to use the dot syntax? In particular I’d like it to use h.symm rather than Eq.symm h. Judging from the code it never uses the dot syntax on proofs, and the only attribute to control the behavior (pp_nodot) goes the wrong way.

[Kyle Miller]

You are correct, there's currently no way to get proofs to pretty print with dot notation.

The justification for this is that it's less likely for dot notation to be able to elaborate, and we want pretty printing to support features like exact?. With h.symm, you have to figure out that h : Eq _ _ before it can be resolved, but from Eq.symm h you know both the function and that h : Eq _ _ .

[Kyle Miller]

(Here's the relevant code: docs#Lean.PrettyPrinter.Delaborator.fieldNotationCandidate?)

[Joachim Breitner]

Right, but if h inherently has clearly Eq type, then it should be fine and is actually pretty.

This isnt important, I was just wondering if I can make the calcify output more pretty that way. For now I add an ad-hoc support for this:
https://github.com/nomeata/lean-calcify/commit/67b07fc2ec499e6e029b5e6b301269ca0f36fce4

[Kyle Miller]

It can be pretty tricky determining whether h clearly has Eq type with the current architecture. For example, what if h is from a fun binder? Normally fun binders don't print types, and somehow the fun delaborator would need to collaborate with the dot notation delaborator to make sure it comes out as either fun h => Eq.symm h or fun (h : Eq a b) => h.symm.

[Kyle Miller]

I think we could relax the restriction (behind an option). Theoretically pp.analyze, when it's enabled, can determine whether to suppress dot notation automatically, but it's not been tested nearly enough.

The current version is "I'll make this be conservative with proofs because I really don't want to break anything when we roll out generalized dot notation" :-)

[Joachim Breitner]

That's a very good point. I wonder if I'll have to revert this change in light of this.

I expect that we'll see more and more tactics that want to delaborate reliably and prettily, and might need a robust pp.analyze eventually.

[Joachim Breitner]

Recently I had to debug something and what worked was to use pp.raw and then manually fix the syntax :disappointed:

[Kyle Miller]

Something I've wondered for a long time was whether we could have ← be a prefix operator that applies some sort of symmetry to a term. For example, it could work like this:

variables (h : 2 = 3) (h' : p ↔ q) (h'' : ∀ n : Nat, n + 1 - 1 = n)

#check ← h
-- 3 = 2
#check ← h'
-- q ↔ p
#check ← h''
-- ∀ n : Nat, n = n + 1 - 1

(This is how I thought the arrow worked in rw in my first few hours of learning Lean.)

[Kyle Miller]

(Incidentally, it'd be neat if there were a dot notation syntax that can eagerly enter under a function type, like imagine my_thm..mp a b instead of needing to write (my_thm a b).mp.)

[Joachim Breitner]

Maybe not that notation, but a convenient way to apply iff theorems would be amazing. If we had that, I would write only a third of the theorems I do now! (Slight exaggeration)

I think in Isabelle apply simply recognizes iff lemma and tries .mp or .mpr implicitly, but I may misremember