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). Check and_er (A/\B) C H1. Check and_el (A/\B) C H1. Check and_el A B (and_el (A/\B) C H1). Check and_er A B (and_el (A/\B) C H1). Check and_i B C (and_er A B (and_el (A/\B) C H1)) (and_er (A/\B) C H1). Check and_i A (B/\C) (and_el A B (and_el (A/\B) C H1)) (and_i B C (and_er A B (and_el (A/\B) C H1)) (and_er (A/\B) C H1)). (* 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. *) Check imp_e B C H4 (imp_e A B H3 H2). (* 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. *) Check imp_i A C (fun ASS:A =>imp_e B C H6 (imp_e A B H5 ASS)). (* 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 (fun ASS:B=>or_ir A (B \/ C) (or_il B C ASS)). Check (fun ASS:A=>or_il A (B\/C) ASS). Check (fun ASSA:(A\/B)=>or_e A B (A\/B\/C) ASSA (fun ASS:A=>or_il A (B\/C) ASS) (fun ASS:B=>or_ir A (B \/ C) (or_il B C ASS))). Check (fun ASS:C=>or_ir A (B \/ C) (or_ir B C ASS)). Check or_e (A\/B) C (A\/(B\/C)) H8 (fun ASSA:(A\/B)=>or_e A B (A\/B\/C) ASSA (fun ASS:A=>or_il A (B\/C) ASS) (fun ASS:B=>or_ir A (B \/ C) (or_il B C ASS))) (fun ASS:C=>or_ir A (B \/ C) (or_ir B C ASS)). (* 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. *) Check neg_i A (fun ASS:A => imp_e A bot H9 ASS). (* 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. *) Check imp_i A bot (fun ASS:A => neg_e A ASS H10).