Temporary opaqueness in the middle of the proof?

Stream: new members

[Youngju Song]

In the middle of the proof, I would like to temporarily make some definition as opaque/irreducible. Would it be possible?
Context: I am applying tactics like simp_all but it is unfolding a bit more than I wanted. Thus, I want to mark some definitions as opaque, apply simp_all, and rollback those definitions to be transparent again.

[Eric Wieser]

A seal foo in _ term elaborator would indeed be a nice feature, though I don't know enough to be sure it actually makes sense

[Daniel Weber]

Could you simp_all [-bad_theorem]?

[Youngju Song]

@Daniel Weber Thank you for the suggestion! Unfortunately, it didn't make a change, but I was able to find another proof.

[Youngju Song]

@Eric Wieser That would be quite nice and compositional. In Coq, I used to do a lot of

Local Opaque mydef.
some_reduction_tactic.
Local Transparent mydef.

but your syntax looks much nicer!

[Eric Wieser]

Perhaps I should mention that seal foo in already exists at the command level, just not the term or tactic level

[Youngju Song]

@Eric Wieser , Thanks, that could be useful. I tried to use it in the middle of the proof in tactic mode (like seal foo; some_tactic; unseal foo) but (as you said) it doesn't seem to work at the moment.
It seems like the top-level commands are in general not working in tactic mode, but it would be very useful to allow some at least commands to be executable in the tactic mode. Few such commands in Coq that I miss are: Set Printing Notations (set_option pp.notation true in Lean), Set Printing All (set_option pp.explicit true in Lean), Search and SearchAbout (not sure what they are in Lean), and Print Instances (not sure what they are in Lean).

[Eric Wieser]

set_option _ in _ works fine in tactic mode

[Youngju Song]

@Eric Wieser That is interesting. In my environment, the following code shows @LE.le Nat instLENat ... instead of ≤ during the proof as expected

set_option pp.notation true
set_option pp.explicit true -- having "in" at the end also works
example : 1 ≤ 2 := by
  skip
  sorry

but the following does not - it always shows ≤ and never shows @LE.le ... no matter where I place my cursor:

example : 1 ≤ 2 := by
  set_option pp.notation true in
  set_option pp.explicit true in -- without "in" it is a syntax error
  skip
  sorry

Is this the same for you?

[Daniel Weber]

I think this is because the cursor doesn't look at options in this resolution - you can see the effect if you use the trace_state tactic, for example

[Eric Wieser]

Arguably this is a bug; I'd encourage you to report it

[Eric Wieser]

(it's probably very low priority, but it's worth having something to refer to)