Parameter A B C : Prop.
Lemma AimpA : A -> A.
intros.
assumption.
Qed.
Lemma imp_trans : (A -> B) -> (B -> C) -> A -> C.
intros AimpB BimpC c.
apply BimpC.
apply AimpB.
assumption.
Qed.
Lemma and_comm : A /\ B -> B /\ A.
intros H.
split.
destruct H.
assumption.
destruct H.
assumption.
Qed. (* We could also destruct H before spliting *)
Lemma or_comm : A \/ B -> B \/ A.
intros.
destruct H. (* Here we need to first break the conjunction H *)
right.
assumption.
left.
assumption.
Qed.
Print AimpA. (* identity *)
Print imp_trans. (* function composition *)
(** Discussion:
In Coq, a proof of A->B is a function that transforms any proof of A into
a proof of B. (A->B is not equivalent, as in classical logic, to the disjunction
~A \/ B.)
The proof of A->A is the identity, returning the proof of A given as input
The proof imp_trans produces of proof of C from a proof of A by applying
the function of type (A->B) to get a proof of B, which is given to the proof
of (B->C). imp_trans is just function composition .
This is why arrow types are the types representing logical implication.
This is an instance of a more general result called Curry-Howard isomorphism
(more details in module 2-7-1)
*)
Lemma A_imp_nnA : A -> ~~A.
intros a na.
apply na.
assumption.
Qed.
Lemma distr_and_or : (A\/B)/\C -> A/\C \/ B/\C.
intros.
destruct H.
destruct H.
left.
split.
assumption.
assumption.
right.
split.
assumption.
assumption.
Qed.
Print iff. (* iff is a conjunction of implications *)
Lemma equiv_refl : A <-> A.
split.
intros.
assumption.
intros.
assumption.
Qed.
(** 2.2 Classical logic *)
(** Beware: forall P, (P \/ ~P) <-> (~~P -> P) is *not* provable *)
Lemma equiv_classic :
(forall P, P \/ ~P) <-> (forall P, ~~P -> P).
split.
intros.
destruct H with (P:=P).
assumption.
exfalso.
apply H0.
assumption.
intros.
apply H.
intro.
apply H0. (* Back to a previous goal? No. Now, by H0, we now P cannot be true *)
right.
intro.
apply H0.
left.
assumption.
Qed.
(* In fact this formulation of excluded-middle is more convenient to use.
In the logic of Coq, which is said to be intuitionistic, there is no
equivalences like ~(A/\B) <-> ~A\/~B or (~ forall x.~ P x) <-> exists x, P x
Disjunction A\/B means that we can determine which of A or B is true,
and existential exists x, P(x) can exhibit a witness, which their equivalent
negated counterpart do not imply.
The aboce equivalence are just implications (from right to left).
In other words, disjunctions and existentials are harder to prove.
The negated form of excluded middle allow to replace a strong proposition
(for instance a disjunction or an existential) into a weaker one (its negated
form).
This form an easy way of doing classical reasoning in Coq.
Whenever a goal is too hard, use nnPP below and you are left with an
easier subgoal. This is easier than thinking hard the proposition
on which we apply the usual excluded-middle.
*)
Parameter nnPP : forall P, ~~P->P.
(* 3.1 Socrates *)
Parameter person : Type. (* Introducing the type of persons *)
Parameter socrates : person. (* Socrates is a person *)
Parameter man : person -> Prop. (* The predicate of person that are men *)
Parameter mortal : person -> Prop. (* The predicate of mortal persons *)
Lemma syllogism : man socrates -> (forall p, man p -> mortal p) -> mortal socrates.
intros socr_m m_m.
apply m_m.
assumption.
Qed.
(* 3.2 Drinkers paradox *)
Lemma drinker : exists p:person, ~ mortal p -> forall q:person, ~ mortal q.
(* Cannot guess a witness -> use classical reasoning *)
apply nnPP.
intro.
apply H.
(* H implies that any person is mortal
So is Socrates and thus the conclusion holds vacuously *)
exists socrates.
intros.
intro.
apply H.
exists q.
intros.
contradiction.
Qed.
Lemma drinker2 : exists p:person, mortal p -> forall q:person, mortal q.
(* Cannot guess a witness -> use classical reasoning *)
apply nnPP.
intro.
apply H.
(* H implies that any person is immortal
So is Socrates and thus the conclusion holds vacuously *)
exists socrates.
intros.
(* Now we are stuck because the mortality of q (which can be not Socrates)
can only be obtained by H which is negated -> need classical reasoning again. *)
apply nnPP.
(* and now the proof goes as before. *)
intro.
apply H.
exists q.
intros.
contradiction.
Qed.
(* 3.4 Groups *)
Parameter elt : Type. (* The type of elements of the group *)
Parameter op : elt -> elt -> elt. (* a binary operation *)
Parameter op_assoc : forall x y z, op (op x y) z = op x (op y z).
Parameter e : elt. (* the neutral *)
Parameter inv : elt -> elt. (* the inverse *)
Parameter neutral_l : forall x, op e x = x.
Parameter neutral_r : forall x, op x e = x.
Parameter inv_l : forall x, op (inv x) x = e.
Parameter inv_r : forall x, op x (inv x) = e.
Lemma op_inv : forall x y,
inv (op x y) = op (inv y) (inv x).
intros.
transitivity (op (op (inv y) (inv x)) (op (op x y) (inv (op x y)))).
rewrite op_assoc.
rewrite op_assoc.
rewrite <- op_assoc with (x:=inv x) (y:=x).
rewrite inv_l.
rewrite neutral_l.
rewrite <- op_assoc with (x:=inv y) (y:=y).
rewrite inv_l.
rewrite neutral_l.
reflexivity.
rewrite inv_r.
rewrite neutral_r.
reflexivity.
Qed.