(** Homework Assignment 1 Checker#
# ##Interactive Computer Theorem Proving#
# CS294-9, Fall 2006#
# UC Berkeley *) (** Directions for using this file to check your solutions: - Have your solutions in a file named [Sol1.v]. - Run [coqc Sol1] from the command line. - With the file you're reading now in the same directory, run [coqc Check1]. - If you don't see any error messages, then you're done! (Actually, Coq will allow you to use the [Axiom] command and its synonyms to assert facts without justification, but just avoid using these and you can rely on this checker. [:-)]) *) Module Type HW1_SIG. Section propositional. Variables P Q R : Prop. Axiom truth : True. Axiom contradiction_P : False -> P. Axiom and_associates : (P /\ Q) /\ R -> P /\ (Q /\ R). Axiom cut_out_the_middle_man : P /\ Q /\ R -> P /\ R. Axiom make_up_your_mind : True \/ False. Axiom or_commutes : P \/ Q -> Q \/ P. Axiom or_associates : (P \/ Q) \/ R -> P \/ (Q \/ R). Axiom something_fishy : (P -> Q) -> P -> ~Q -> R. Axiom contrapositive : (P -> Q) -> ~Q -> ~P. End propositional. Axiom ofcourse : forall A : Set, A -> forall (f : A -> A) (P : A -> Prop), (forall x : A, P (f x)) -> exists y : A, P y. Section firstorder. Variable A : Set. Variable e : A. Variable f : A -> A. Variables P P' : A -> Prop. Variable Q : A -> A -> Prop. Axiom indeed : forall (A : Set) (e : A) (f : A -> A) (P : A -> Prop), (forall x : A, P x) -> P (f e). Axiom swap_quantifiers : (exists x : A, forall y : A, Q x y) -> (forall y : A, exists x : A, Q x y). Axiom nobody : (forall x : A, ~(P x)) -> ~(exists x : A, P x). Axiom coalesce1 : (forall x : A, P x) /\ (forall x : A, P' x) -> (forall x : A, P x /\ P' x). Axiom coalesce2 : (forall x : A, P x /\ P' x) -> (forall x : A, P x) /\ (forall x : A, P' x). Axiom one_or_the_other : (forall x : A, P x -> P' e) -> ((forall y : A, P' y) \/ (exists z : A, P z)) -> P' e. Axiom reverse_congruence : forall x : A, forall y : A, x = y -> f y = f x. Axiom small_world : (exists x : A, forall y : A, x = y) -> e = f e. Axiom nasty : forall x : A, forall y : A, forall z : A, f (f x) = x -> f z = f x -> f y = f z -> f (f (f (f (f x)))) = f y. End firstorder. End HW1_SIG. Require Sol1. Module Sol1_Verified : HW1_SIG := Sol1.