Seems like my main problem with proof assistants is that I have to go down to the elementary expressions (with which programmers deal usually) very often, and there is just too many variables to track / keep in mind.
OTOH, maybe it's just the lack of experience, IDK. And I need to learn "surfing" at high level.
There aren't enough reusable abstractions. I think it's a combination of 1: the ecosystem is too small by lack of manpower and 2: we still don't know how to build interfaces in a way that works well with proofs; typeclasses vs canonical structures is an ongoing debate.
@lyxia As a rule of thumb, I try to match the depth of destruction and construction, and do the reduction and expansion consistently, in particular, unfold the definitions in * |- *, so the level of consideration is "even" across all the premises and conclusions.
I am actually wondering if #SSReflect could help with that, but frankly I doubt it.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!