(* First assignment for the course G54DTP. *) (* Venanzio Capretta, February 2011. *) (* Complete the proofs, 1 point each. *) Variables A B C D: Prop. Lemma ex1: (A->B->C) -> B -> A -> C. Proof. intros h b a. apply h. exact a. exact b. Qed. Lemma ex2: (A->B) -> (A-> B->C) -> A -> C. Proof. intros h1 h2 a. apply h2. exact a. apply h1. apply a. Qed. Lemma ex3: (A/\B -> C) -> (A->B) -> A -> C. Proof. intros h1 h2 a. apply h1. split. exact a. apply h2. exact a. Qed. Lemma ex4: (A->B) -> (C->D) -> A\/C -> B\/D. Proof. intros h1 h2 h3. elim h3. intro a. left. apply h1. exact a. intro c. right. apply h2. exact c. Qed. Lemma ex5: A\/(B/\C) -> (A\/B)/\(A\/C). Proof. intros h. elim h. intros a. split. left. exact a. left. exact a. intro bc. elim bc. intros b c. split. right. exact b. right. exact c. Qed. Lemma ex6: (A->~B) -> B -> ~A. Proof. intros h b a. apply h. exact a. exact b. Qed. Lemma ex7: ~(A\/B) -> ~A/\~B. Proof. intros h. split. intro a. apply h. left. exact a. intro b. apply h. right. exact b. Qed. Lemma ex8: ~A\/~B -> ~(A/\B). Proof. intros h1 h2. elim h2. intros a b. elim h1. intro na. apply na. exact a. intro nb. apply nb. exact b. Qed. Lemma ex9: ~(A->B) -> ~B. Proof. intros h b. apply h. intro a. exact b. Qed. Lemma ex10: ~~(A\/~A). Proof. intro h. apply h. right. intro a. apply h. left. exact a. Qed.