A Constructive and Synthetic Theory of Reducibility: Myhill's Isomorphism Theorem and Post's Problem for Many-One and Truth-Table Reducibility in Coq (Full Version)