Section Basic.
(*Basic Logical Reasoning *)
Variables A B : Prop.
Goal A /\ B -> B /\ A.
Proof.
intro H.
destruct H.
apply conj.
assumption.
assumption.
Qed.
Goal A /\ B -> B /\ A.
Proof.
intros (H1,H2); split; assumption.
Qed.
Goal A /\ B -> B /\ A.
Proof.
tauto.
Qed.
(* Coq basic theory implements an intuitionistic logic which does not prove
Pierce law but a weaker version of it (not not P => P) is not a basic axiom *)
Variables P Q : Prop.
Lemma PierceI : ((P->Q)->P)-> ~ ~ P.
Proof.
(* tauto. *)
intros H1 H2.
apply H2.
apply H1.
intro H3.
case H2.
assumption.
Qed.
(* A special library can be loaded to add classical reasoning *)
Require Import Classical.
Lemma Pierce : ((P->Q)->P)->P.
(* Excursion: this is actually known under the name "Pierce Law".
It is not a theorem in Pure (since Pure is intuitionistic),
but a theorem in HOL: *)
(* solution *)
(* tauto. *)
intro.
apply NNPP.
apply PierceI.
assumption.
Qed.
End Basic.
Section Equational.
(* Very Basic Equational Reasoning *)
(* no automation at all: the example from the course *)
Variable E : Type.
Variables a b c:E.
Variable f : E*E -> E.
Variable g : E -> E.
Lemma A: f(a,b) = a -> f(f(a,b),b) = c -> g a = g c.
intros H1 H2.
assert (a = c).
transitivity (f(a,b)).
rewrite H1.
reflexivity.
transitivity (f (f (a, b), b)).
f_equal.
f_equal.
symmetry.
assumption.
assumption.
rewrite H.
reflexivity.
Qed.
End Equational.
Section Xor.
Definition xor (A B :Prop) : Prop := (A /\ ~ B) \/ (~ A /\ B).
Lemma xor_refl A : xor A (~A).
Proof. (* requires classical reasoning, use lemme classic*)
unfold xor.
destruct (classic A).
left; auto.
right; auto.
Qed.
End Xor.
Section Sets.
Variable E : Type.
Definition incl A B := forall x : E, A x -> B x.
Variable A B C : E -> Prop.
Lemma incl_trans : incl A B -> incl B C -> incl A C.
Proof.
unfold incl; intros.
(* auto. solves the goal *)
apply H0.
apply H.
assumption.
Qed.
Ens Sets.
Section FirstOrder.
Variable E : Type.
Variable A : Prop.
Variable B : E -> Prop.
Lemma all_istr:
(forall x, A -> B x) <-> (A -> forall x, B x).
Proof.
split.
intros H1 H2 x.
apply H1.
assumption.
intros H1 x H2.
apply H1.
assumption.
Qed.
Lemma all_istr':
(forall x, A -> B x) <-> (A -> forall x, B x).
Proof.
(* intuition. *)
split; intros.
apply H.
assumption.
apply H.
assumption.
Qed.
Variable P : E -> E -> Prop.
Lemma ex_all : (forall x, exists y, P x y) -> forall y, exists x, P x y.
(* Possible to prove ? *)
Abort.
(* Coq does not assume that Type are non-empty *)
Variable e:E.
Lemma ex_all2 : (forall x, forall y, P x y) -> exists y, forall x, P x y.
(* firstorder. *)
intro H.
exists e.
intro x.
apply H.
Qed.
(* Possible to prove ? *)
End FirstOrder.