simp contextual tactic syntax

Stream: general

[Joachim Breitner]

Is it just me that sees simp (config := {contextual := true}) […] and thinks

:thought: surely this kind of config fiddling is not meant for everyday use, given the verbose and confusing syntax; maybe this exists only for use within other tactics or so”

and would think quite different it was, say,

    simp contextual [charP_iff, zero_dvd_iff, iff_def, H]

[Kyle Miller]

I've wanted contextual to be a more accessible option for a long time. Why does autoUnfold get ! but no other option gets a quick syntax?

[Joachim Breitner]

only has quick syntax! As does ?. In a way.

[Notification Bot]

3 messages were moved here from #general > How to learn "idiomatic" lean? by Joachim Breitner.

[Kyle Miller]

Those ones don't affect the Simp.config though, they're more special.

[Kyle Miller]

I found a proposal of mine from a couple years ago. With simp/c, I was thinking about refinement syntax from Rebol. There, f/x/y/z a b c is sort of like doing f (x := true) (y := true) (z := true) a b c, where the default values for x, y, and z are false.

(The later proposal about simp+c and simp+c-b, etc, is not one I'd like to see in Lean!)

[Kyle Miller]

Would it be too weird having simp +contextual [...] and simp -beta [...] be short forms for simp (config := {contextual := true}) [...] and simp (config := {beta := false}) [...]? A thought here is that + and - prefixes could make it be more likely that the (config := ...) parser and elaborator could be adjusted to handle this all at once across all tactics that use it.

[Mario Carneiro]

I've been wanting to write a general purpose config argument parser which would allow writing (contextual := true) instead of (config := {contextual := true})

[Brendan Seamas Murphy]

Joachim Breitner said:

Is it just me that sees simp (config := {contextual := true}) […] and thinks

:thought: surely this kind of config fiddling is not meant for everyday use, given the verbose and confusing syntax; maybe this exists only for use within other tactics or so”

and would think quite different it was, say,

    simp contextual [charP_iff, zero_dvd_iff, iff_def, H]

I feel this way whenever I write (config := {singlePass := true}), too

[Eric Rodriguez]

Mario Carneiro said:

I've been wanting to write a general purpose config argument parser which would allow writing (contextual := true) instead of (config := {contextual := true})

This is better, but I still think it's too verbose. I think one character flags for these common things should be the norm.

[Johan Commelin]

Agreed. I really like the +contextual - beta idea.

[Johan Commelin]

Atm it feels to me like I'm telling simp "go in expensive mode" :dollars: :dollars: :money:

Maybe it is true! And then we probably shouldn't change the syntax. But I actually think it isn't that expensive, and so I would be happy to have "cheaper" syntax :grinning:

[Mario Carneiro]

I'm fine with there being an even more compact syntax for boolean options, but it may interfere with regular arguments of the tactic if it's a general purpose config arg parser

[Kim Morrison]

I think one character flags would be unkind to learners and readers.