Load CS3202. (* look it's a comment *) (* look it goes over several lines *) (* I now declare some propositional variables/atoms *) Variable A B C:Prop. (* Now I prove A |- A *) Hypothesis H:A. (* Checkout my proof-term for A! It uses H *) Check H. (* Checkout my other proof-term for A! It also uses H*) Check copy A H. (* Now I prove A/\B |- B/\A *) Hypothesis H_AB : A /\ B. (* I am now going to build a proof-term for B/\A. It will use H_AB. *) Check H_AB. Check and_el A B H_AB. Check and_er A B H_AB. (* Here it is! *) Check and_i B A (and_er A B H_AB) (and_el A B H_AB) . (* Now I prove A\/B |- B\/A *) Hypothesis H0:A\/B. (* I am now going to build a term proving B\/A. It will use H_0. *) Check fun H1:A => or_ir B A H1. Check fun H2:B => or_il B A H2. Check or_e A B (B\/A) H0 (fun H1:A => or_ir B A H1) (fun H2:B => or_il B A H2). (* Now YOU prove (A/\B)/\C |- A/\(B/\C) *) Hypothesis H1:(A/\B)/\C. (* I want you to build a proof-term for A/\(B/\C). It will use H1. First, notice that coqide's pretty print of A/\(B/\C) is A/\B/\C The right associativity of /\ is built-in! *) Check A/\(B/\C). (* Now you prove A,A->B,B->C |- C *) Hypothesis H2:A. Hypothesis H3:A->B. Hypothesis H4:B->C. (* I want you to build a proof-term for C. It will use H2, H3, H4. *) (* Now you prove A->B,B->C |- A->C *) Hypothesis H5:A->B. Hypothesis H6:B->C. (* I want you to build a proof-term for A->C. It will use H5, H6. *) (* Now you prove (A\/B)\/C |- A\/(B\/C) *) Hypothesis H8:(A\/B)\/C. (* I want you to build a proof-term for A\/(B\/C). It will use H8. Checkout the inbuilt associativity of \/ *) Check A\/(B\/C). (* Now you prove A->bot |- not A *) Hypothesis H9:(A->bot). (* I want you to build a proof-term for not A. It will use H9. *) (* Now you prove not A |- A->bot *) Hypothesis H10:(not A). (* I want you to build a proof-term for A->bot. It will use H9. *)