I’ve been told the best way to learn is to do so let’s do some propositional logic with Coq. I got these exercises from the first two sessions of “The Incredible Proof Machine“.

I’m not sure how to translate contexts in sequent calculus other than making everything above the bar an input and everything below the bar an output so some of the exercises did not have analogs (like flipping the order of the premises). I either skipped those or made a best effort translation.