Wondering how a proof assistant such as Coq proves forall or exists. For example:
- If you were to give it a huge set of items like a million, wondering if it would actually iterate through it 3x and compare all the values to prove the transitive relation holds.
- If not, then wondering if it doesn't even need such an "example" group, and instead it can just work on the definition itself, and how that would work.
- Or is this proof definition defining a set in advance, so it provably has the transitive relation from the start. If so, how that works.
Say you want to prove some set has the transitive property, wondering how the proof assistant goes about proving that, how it works under the hood.