Is there a way to hide internals of a definition in Lean?

Stream: Analysis I

[Rado Kirov]

I rebased and cleaned up some of my solutions for 3.3, and now I understand a lot of the pain comes from unintentionally expanding the definition of Function to its definitionally equal, but too complicated internals. Very similar thing happened in Ch3.5 for Cartesian product and OrderedPairs.

For example, every time I wanted to do something with f = g I used ext which dropped all the way down to the underlying proposition f.P x y \iff g.P. x y, but after looking over @Dan Abramov 's answers I see it works way better to just use Function.fn_ext and just work with Lean functions. Similarly, calling simp will often reduce too deep.

Is there a notion of information hiding, private/public, etc (trying not to bias towards OOPs way of solving this), where one is not allowed or at least discouraged to reduce too deep and thus nudged to look for the right theorems? The theorem themselves should be able to access the internal representation in their proofs.

[Edward van de Meent]

Rado Kirov said:

Similarly, calling simp will often reduce too deep.

Creating good API and curating a simp set are skills one acquires. In particular, having a lemma which unfolds any application of some definition marked as simp tends to be bad. (In particular, it doesn't simplify the goal.) Instead, good simp lemmas for a function tend to be one which describes the behaviour of classes of arguments. For example, a simp lemma might describe how Prod.map acts on Prod.mk a b, but not on a general variable of type Prod A B.

[Rado Kirov]

Yes, it is pretty standard software engineering practice, but only after doing the exercises in Ch3 I am starting to get a sense of what does this practically mean in Lean. In regular software evaluation runs only in one direction, while in proof assistants rewriting could run both ways, and it takes extra care by the theorem writers to emulate that one-directionality.

unfolds any application of some definition marked as simp

I have to go back and see what exactly happened, but I also noticed simp only [] doing expansions. AFAIK, simp only [] only does defeq rewriting, but what if sometimes we don't want that?

[Edward van de Meent]

afaik simp only [] is unable to do any rewriting, only reductions like (fun x => x + 1) y ~> y + 1 and maybe proving a True goal... usually these are harmless