(** * Proofs are Programs *) (* Pick a few of these propositions, and prove them by directly writing down the Coq program that is the proof, rather than using tactics to help construct the proof. (A -> B) -> ((B -> C) -> (A -> C)) A -> (A \/ B) B -> (A \/ B) (A -> C) -> ((B -> C) -> ((A \/ B) -> C)) A /\ B -> A A /\ B -> B (C -> A) -> ((C -> B) -> (C -> (A /\ B))) (A -> (B -> C)) -> ((A /\ B) -> C) ((A /\ B) -> C) -> (A -> (B -> C)) (A /\ ~A) -> B (A -> (A /\ ~A)) -> ~A A -> (A -> B) -> B Here's an example of what we mean, using the first proposition from above: *) Definition example : forall A B C : Prop, (A -> B) -> ((B -> C) -> (A -> C)) := fun (A B C : Prop) (ab : A -> B) (bc : B -> C) (a : A) => bc (ab a). (* You will need to use pattern matching for proofs/programs involving conjunction, disjunction, and negation. Specifically, [conj] will be useful for conjunction, [or_introl] and [or_intror] for disjunction, and [not] and [False_rect] for negation. You can review those by examing the output of these: *) Print and. Print or. Print not. Print False_rect.