Dimensional analysis is absolutely an instance of what I’m talking about!
As for only being able to do constructive stuff, you actually can do classical stuff as well, but you have to explicitly assume the law of the excluded middle. For example, if in Lean I write
axiom lem (P: Prop): P ∨ ¬P
then I can start doing classical reasoning.
Also, you’re totally right that you could also do h(h(fxx)) and so on as much as you want, but there’s no real reason to do so, since if you start from the simplest possible way to do it you’ll solve the problem by the time you get to h(fxx).
Ah, cool thanks! I also realised that if you were just using the type checker in your head, once you got to (P → ⊥) → ⊥, you could consider your proof done by your (outside of the type checker) assumption of LEM. But I see no we don’t need to assume it outside of the type checker!
Dimensional analysis is absolutely an instance of what I’m talking about!
As for only being able to do constructive stuff, you actually can do classical stuff as well, but you have to explicitly assume the law of the excluded middle. For example, if in Lean I write
then I can start doing classical reasoning.
Also, you’re totally right that you could also do h(h(fxx)) and so on as much as you want, but there’s no real reason to do so, since if you start from the simplest possible way to do it you’ll solve the problem by the time you get to h(fxx).
Ah, cool thanks! I also realised that if you were just using the type checker in your head, once you got to (P → ⊥) → ⊥, you could consider your proof done by your (outside of the type checker) assumption of LEM. But I see no we don’t need to assume it outside of the type checker!