(**
* 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.