(** * Propositional logic *)
Section propositional_logic.
Variables A B C D: Prop.
(** explicit proofs, illustrating the Curry-Howard correspondence *)
Lemma id: A -> A.
Proof (fun x => x).
Lemma comp: (A -> B) -> (B -> C) -> (A -> C).
Proof (fun f g x => g (f x)).
Lemma Sc: (A -> B -> C) -> (A -> B) -> A -> C.
Proof (fun f g x => f x (g x)).
(** ** intro / apply *)
Lemma id': A -> A.
Proof.
intro H.
apply H.
Qed.
Lemma comp': (A -> B) -> (B -> C) -> (A -> C).
Proof.
(** backward reasoning *)
intros HAB HBC HA.
apply HBC.
apply HAB.
apply HA.
Qed.
Lemma comp'': (A -> B) -> (B -> C) -> (A -> C).
Proof.
(** forward reasoning *)
intros HAB HBC HA.
apply HAB in HA.
apply HBC in HA.
apply HA.
Qed.
Lemma comp''': (A -> B) -> (B -> C) -> (A -> C).
Proof.
(** intermediate style *)
intros HAB HBC HA.
apply HAB in HA.
apply (HBC HA).
Qed.
Lemma Sc': (A -> B -> C) -> (A -> B) -> A -> C.
Proof.
intros f g x.
apply f.
apply x.
apply g, x.
Qed.
(** ** conjunctions: destruct/split *)
Lemma and_build: A -> B -> A /\ B.
Proof.
intros a b.
split.
apply a.
apply b.
Qed.
Lemma and_build': A -> B -> A /\ B.
Proof.
intros.
split.
assumption.
assumption.
Qed.
Lemma and_build'': A -> B -> A /\ B.
Proof.
intros.
split; assumption.
Qed.
Lemma and_exploit_l: A /\ B -> A.
Proof.
intro H.
destruct H as [HA HB].
apply HA.
Qed.
Lemma and_exploit_r: A /\ B -> B.
Proof.
intros [HA HB].
assumption.
Qed.
Lemma and_comm: A /\ B -> (B /\ A).
Proof.
intros [? ?].
split; assumption.
Qed.
Lemma and_assoc: A /\ (B /\ C) -> (A /\ B) /\ C.
Proof.
intro H.
destruct H as [HA HBC].
destruct HBC as [HB HC].
split.
split.
apply HA.
apply HB.
apply HC.
Qed.
Lemma and_assoc': A /\ (B /\ C) -> (A /\ B) /\ C.
Proof.
intros [HA [HB HC]].
repeat split; assumption.
Qed.
(** ** disjunctions: destruct/left/right *)
Lemma or_build_l: A -> A \/ B.
Proof.
intro HA.
left.
apply HA.
Qed.
Lemma or_exploit: A \/ B -> (A -> C) -> (B -> C) -> C.
Proof.
intros H HAC HBC.
destruct H as [HA|HB].
apply HAC, HA.
apply HBC, HB.
Qed.
Lemma or_comm: A \/ B -> (B \/ A).
Proof.
intro H.
destruct H as [HA|HB].
right. apply HA.
left. apply HB.
Qed.
Lemma or_assoc: A \/ (B \/ C) -> (A \/ B) \/ C.
Proof.
intro H. destruct H as [HA|HBC].
left. left. apply HA.
destruct HBC as [HB|HC].
left. right. apply HB.
right. apply HC.
Qed.
Lemma or_assoc': A \/ (B \/ C) -> (A \/ B) \/ C.
Proof.
intros [HA|[HB|HC]].
left. left. assumption.
left. right. assumption.
right. assumption.
Qed.
Lemma or_and_distr: A /\ (B \/ C) <-> (A /\ B) \/ (A /\ C).
Proof.
split. (* <-> is a conjunction *)
intros [a [b|c]].
left. split; assumption.
right. split; assumption.
intros [[a b]|[a c]].
split. assumption. left. assumption.
split. assumption. right. assumption.
Qed.
Lemma and_or_distr: A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C).
Proof.
split.
intros [a|[b c]].
split; left; assumption.
split; right; assumption.
intros [[a|b] ac].
left. assumption.
destruct ac.
left. assumption.
right. split; assumption.
Qed.
(** ** efficiency: forward reasoning with assert *)
Lemma fwd: (A -> B) -> (B -> C) -> (B -> C -> D) -> A -> C/\D.
Proof.
intros ab bc bcd a.
assert(b: B). apply ab, a.
assert(c: C) by apply bc, b.
split. assumption.
now apply bcd.
Qed.
(** ** negation *)
(** negation is an abbreviation, use "unfold not" to unfold it *)
Lemma notnot: A -> ~(~A).
Proof.
unfold not.
intros HA HnA.
apply HnA, HA.
Qed.
Lemma consistent: ~(~A /\ A).
Proof. intros [HnA HA]. apply HnA, HA. Qed.
Lemma False_exploit: False -> A.
Proof.
(** use contradict or destruct to eliminate False assumptions *)
intro H. contradict H.
Restart.
intro H. destruct H.
Restart.
intros [].
Qed.
Lemma and_not: ~A /\ ~B <-> ~(A \/ B).
Proof.
split.
intros [HnA HnB] [HA|HB].
apply HnA, HA.
apply HnB, HB.
intros H. split; intro H'; apply H.
left. assumption.
right. assumption.
Qed.
Lemma or_not: ~A \/ ~B -> ~(A /\ B).
Proof.
intros [HnA|HnB] [HA HB].
apply HnA, HA.
apply HnB, HB.
Qed.
(** NB: the above proofs can all be solved using the tactic [tauto],
which solves precisely all the propositional intuitionistic
tautologies *)
(** * Classical logic *)
(** the converse of [or_not] does not hold in intuitionistic logic: we need the excluded middle *)
Axiom te: forall P, P \/ ~P.
Lemma or_not': ~(A /\ B) -> ~A \/ ~B.
Proof.
intro H.
destruct (te A).
destruct (te B).
contradict H.
split; assumption.
right. assumption.
left. assumption.
Qed.
(* x *)
Lemma nn_te: (forall P, P\/~P) <-> (forall P, ~~P -> P).
Proof.
split.
intros te' P HP. destruct (te' P).
assumption.
now contradict HP.
intros nn P. apply nn. intro E.
apply E. right. intro p. apply E. left. apply p.
Qed.
(* x *)
Lemma peirce: ((A -> B) -> A) -> A.
Proof.
intro H. destruct (te A) as [HA|HnA]. assumption.
apply H. intro a. destruct HnA. assumption.
Qed.
End propositional_logic.
(** * Predicate logic *)
(** now we introduce predicates (here, on natural numbers) *)
Section predicate_logic.
Variables P Q: nat -> Prop.
Variable R: nat -> nat -> Prop.
(** ** universal quantification: intro/apply *)
Goal (forall x, P (2*x) -> Q x) -> P 6 -> Q 3.
Proof. intros H H6. apply H, H6. Qed.
Goal (forall x, P x -> R x x) -> (forall x, P x) -> forall x, R x x.
Proof.
intros HPR HP x. (** note how we introduce x, like an hypothesis *)
apply HPR, HP.
Qed.
Goal (forall x, P x /\ Q x) -> (forall x, P x) /\ (forall x, Q x).
Proof.
intro H; split; intro x.
destruct (H x) as [Px Qx]. assumption.
destruct (H x) as [Px Qx]. assumption.
Qed.
Goal (forall x, P x) \/ (forall x, Q x) -> (forall x, P x \/ Q x).
Proof.
intros [H|H] x.
left. apply H.
right. apply H.
Qed.
(** ** existential quantification: destruct/exists *)
(** a proof of [exists x, P x] si a pair of an element x (the witness) and a proof that it satisfies P *)
Goal (exists x, P x /\ Q x) -> (exists x, P x).
Proof.
intro H. destruct H as [x Hx]. (* exists elimination *)
destruct Hx as [Px Qx].
exists x. (* exists introduction *)
apply Px.
Qed.
Goal (exists x, P (5+x)) -> exists x, P (2+x).
Proof.
intros [x Hx].
exists (3+x). assumption.
Qed.
Goal (exists x, exists y, R x y) <-> (exists y, exists x, R x y).
Proof.
split.
intros [x [y Rxy]]. exists y. exists x. assumption.
intros [y [x Rxy]]. exists x. exists y. assumption.
Qed.
Goal (forall x y, R x y -> R y x) ->
(forall x, exists y, R x y) ->
(forall y, exists x, R x y).
Proof.
intros HR H y.
destruct (H y) as [x Hx].
exists x. apply HR. assumption.
Qed.
Goal ~(exists x, P x) <-> forall x, ~P x.
Proof.
split.
intros H x Px. apply H. exists x. assumption.
intros H [x Px]. apply (H x). assumption.
Qed.
Goal
(exists x, P x \/ Q x) <->
(exists x, P x) \/ (exists x, Q x).
Proof.
split.
intros [x [Px|Qx]].
left. exists x. assumption.
right. exists x. assumption.
intros [[x Px]|[x Qx]]; exists x.
left. assumption.
right. assumption.
Qed.
Goal
(exists x, P x /\ Q x) ->
(exists x, P x) /\ (exists x, Q x).
Proof. intros [x [Px Qx]]. split; exists x; assumption. Qed.
(* xx *)
Goal (exists x, ~P x) <-> ~(forall x, P x).
Proof.
split.
intros [x nPx] H. apply nPx, H.
(* note that this second part is classical *)
intro H. apply nn_te. apply te.
intro H'. apply H. intro x.
destruct (te (P x)) as [Hx|Hnx].
assumption.
destruct H'. exists x. assumption.
Qed.
Variables A B C: Prop.
Goal
P 3 ->
(forall x, P x -> A) ->
(A -> exists x, R x x /\ B) ->
(forall x y, R x y -> Q (x+y)) ->
B /\ exists x, Q (x+x).
Proof.
intros P3 HA H HRQ. destruct H as [x [Rxx b]]. apply (HA 3), P3.
split. assumption.
exists x. apply HRQ, Rxx.
Qed.
Goal
P 3 ->
(forall x, P x -> A) ->
(A -> exists x, R x x \/ B) ->
(forall x y, R x y -> Q (x+y)) ->
B \/ exists x, Q (x+x).
Proof.
intros P3 HA H HRQ. destruct H as [x [Rxx|b]]. apply (HA 3), P3.
right. exists x. apply HRQ, Rxx.
left. assumption.
Qed.
End predicate_logic.
(* xxx *)
Goal ~(forall P Q: nat -> Prop,
(exists x, P x) /\ (exists x, Q x) ->
(exists x, P x /\ Q x)).
Proof.
intro H.
destruct (H (fun x => x=0) (fun x => x=1)) as [x [x0 x1]].
split.
exists 0. reflexivity.
exists 1. reflexivity.
rewrite x0 in x1. discriminate.
Qed.
Goal ~(forall P Q: nat -> Prop,
(forall x, P x \/ Q x) ->
(forall x, P x) \/ (forall x, Q x)).
Proof.
intro H.
destruct (H (fun x => x=0) (fun x => x<>0)) as [H'|H'].
intro x. destruct x. left. reflexivity. right. discriminate.
specialize (H' 1). discriminate.
destruct (H' 0). reflexivity.
Qed.