Library s1_prop
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)).
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.
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.
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.
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.
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.
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. 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.
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.
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.
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
the converse of or_not does not hold in intuitionistic logic: we need the excluded middle
Classical logic
Axiom EM: ∀ P, P ∨ ¬P.
Lemma or_not': ~(A ∧ B) → ¬A ∨ ¬B.
Proof.
intro H.
destruct (EM A).
destruct (EM B).
contradict H.
split; assumption.
right. assumption.
left. assumption.
Qed.
Lemma NN_EM: (∀ P, P\/~P) ↔ (∀ P, ~~P → P).
Proof.
split.
intros EM' P HP. destruct (EM' P).
assumption.
now contradict HP.
intros nn P. apply nn. intro E.
apply E. right. intro p. apply E. left. apply p.
Qed.
Lemma Peirce: ((A → B) → A) → A.
Proof.
intro H. destruct (EM A) as [HA|HnA]. assumption.
apply H. intro a. destruct HnA. assumption.
Qed.
End propositional_logic.
Section predicate_logic.
Variables P Q: nat → Prop.
Variable R: nat → nat → Prop.
Goal (∀ x, P (2*x) → Q x) → P 6 → Q 3.
Proof. intros H H6. apply H, H6. Qed.
Goal (∀ x, P x → R x x) → (∀ x, P x) → ∀ x, R x x.
Proof.
intros HPR HP x.
Proof. intros H H6. apply H, H6. Qed.
Goal (∀ x, P x → R x x) → (∀ x, P x) → ∀ x, R x x.
Proof.
intros HPR HP x.
note how we introduce x, like an hypothesis
apply HPR, HP.
Qed.
Goal (∀ x, P x ∧ Q x) → (∀ x, P x) ∧ (∀ 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 (∀ x, P x ∨ Q x) → (∀ x, P x) ∨ (∀ x, Q x).
Abort.
Goal (∀ x, P x) ∨ (∀ x, Q x) → (∀ x, P x ∨ Q x).
Proof.
intros [H|H] x.
left. apply H.
right. apply H.
Qed.
Qed.
Goal (∀ x, P x ∧ Q x) → (∀ x, P x) ∧ (∀ 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 (∀ x, P x ∨ Q x) → (∀ x, P x) ∨ (∀ x, Q x).
Abort.
Goal (∀ x, P x) ∨ (∀ x, Q x) → (∀ x, P x ∨ Q x).
Proof.
intros [H|H] x.
left. apply H.
right. apply H.
Qed.
existential quantification: destruct/exists
a proof of ∃ x, P x si a pair of an element x (the witness) and a proof that it satisfies P
Goal (∃ x, P x ∧ Q x) → (∃ x, P x).
Proof.
intro H. destruct H as [x Hx]. destruct Hx as [Px Qx].
∃ x. apply Px.
Qed.
Goal (∃ x, P (5+x)) → ∃ x, P (2+x).
Proof.
intros [x Hx].
∃ (3+x). assumption.
Qed.
Goal (∃ x, ∃ y, R x y) ↔ (∃ y, ∃ x, R x y).
Proof.
split.
intros [x [y Rxy]]. ∃ y. ∃ x. assumption.
intros [y [x Rxy]]. ∃ x. ∃ y. assumption.
Qed.
Goal (∀ x y, R x y → R y x) →
(∀ x, ∃ y, R x y) →
(∀ y, ∃ x, R x y).
Proof.
intros HR H y.
destruct (H y) as [x Hx].
∃ x. apply HR. assumption.
Qed.
Goal ~(∃ x, P x) ↔ ∀ x, ¬P x.
Proof.
split.
intros H x Px. apply H. ∃ x. assumption.
intros H [x Px]. apply (H x). assumption.
Qed.
Goal
(∃ x, P x ∨ Q x) ↔
(∃ x, P x) ∨ (∃ x, Q x).
Proof.
split.
intros [x [Px|Qx]].
left. ∃ x. assumption.
right. ∃ x. assumption.
intros [[x Px]|[x Qx]]; ∃ x.
left. assumption.
right. assumption.
Qed.
Goal
(∃ x, P x ∧ Q x) →
(∃ x, P x) ∧ (∃ x, Q x).
Proof. intros [x [Px Qx]]. split; ∃ x; assumption. Qed.
Goal (∃ x, ¬P x) ↔ ~(∀ x, P x).
Proof.
split.
intros [x nPx] H. apply nPx, H.
intro H. apply NN_EM. apply EM.
intro H'. apply H. intro x.
destruct (EM (P x)) as [Hx|Hnx].
assumption.
destruct H'. ∃ x. assumption.
Qed.
Variables A B C: Prop.
Goal
P 3 →
(∀ x, P x → A) →
(A → ∃ x, R x x ∧ B) →
(∀ x y, R x y → Q (x+y)) →
B ∧ ∃ x, Q (x+x).
Proof.
intros P3 HA H HRQ. destruct H as [x [Rxx b]]. apply (HA 3), P3.
split. assumption.
∃ x. apply HRQ, Rxx.
Qed.
Goal
P 3 →
(∀ x, P x → A) →
(A → ∃ x, R x x ∨ B) →
(∀ x y, R x y → Q (x+y)) →
B ∨ ∃ x, Q (x+x).
Proof.
intros P3 HA H HRQ. destruct H as [x [Rxx|b]]. apply (HA 3), P3.
right. ∃ x. apply HRQ, Rxx.
left. assumption.
Qed.
End predicate_logic.
Goal ~(∀ P Q: nat → Prop,
(∃ x, P x) ∧ (∃ x, Q x) →
(∃ x, P x ∧ Q x)).
Proof.
intro H.
destruct (H (fun x ⇒ x=0) (fun x ⇒ x=1)) as [x [x0 x1]].
split.
∃ 0. reflexivity.
∃ 1. reflexivity.
rewrite x0 in x1. discriminate.
Qed.
Goal ~(∀ P Q: nat → Prop,
(∀ x, P x ∨ Q x) →
(∀ x, P x) ∨ (∀ 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.
Proof.
intro H. destruct H as [x Hx]. destruct Hx as [Px Qx].
∃ x. apply Px.
Qed.
Goal (∃ x, P (5+x)) → ∃ x, P (2+x).
Proof.
intros [x Hx].
∃ (3+x). assumption.
Qed.
Goal (∃ x, ∃ y, R x y) ↔ (∃ y, ∃ x, R x y).
Proof.
split.
intros [x [y Rxy]]. ∃ y. ∃ x. assumption.
intros [y [x Rxy]]. ∃ x. ∃ y. assumption.
Qed.
Goal (∀ x y, R x y → R y x) →
(∀ x, ∃ y, R x y) →
(∀ y, ∃ x, R x y).
Proof.
intros HR H y.
destruct (H y) as [x Hx].
∃ x. apply HR. assumption.
Qed.
Goal ~(∃ x, P x) ↔ ∀ x, ¬P x.
Proof.
split.
intros H x Px. apply H. ∃ x. assumption.
intros H [x Px]. apply (H x). assumption.
Qed.
Goal
(∃ x, P x ∨ Q x) ↔
(∃ x, P x) ∨ (∃ x, Q x).
Proof.
split.
intros [x [Px|Qx]].
left. ∃ x. assumption.
right. ∃ x. assumption.
intros [[x Px]|[x Qx]]; ∃ x.
left. assumption.
right. assumption.
Qed.
Goal
(∃ x, P x ∧ Q x) →
(∃ x, P x) ∧ (∃ x, Q x).
Proof. intros [x [Px Qx]]. split; ∃ x; assumption. Qed.
Goal (∃ x, ¬P x) ↔ ~(∀ x, P x).
Proof.
split.
intros [x nPx] H. apply nPx, H.
intro H. apply NN_EM. apply EM.
intro H'. apply H. intro x.
destruct (EM (P x)) as [Hx|Hnx].
assumption.
destruct H'. ∃ x. assumption.
Qed.
Variables A B C: Prop.
Goal
P 3 →
(∀ x, P x → A) →
(A → ∃ x, R x x ∧ B) →
(∀ x y, R x y → Q (x+y)) →
B ∧ ∃ x, Q (x+x).
Proof.
intros P3 HA H HRQ. destruct H as [x [Rxx b]]. apply (HA 3), P3.
split. assumption.
∃ x. apply HRQ, Rxx.
Qed.
Goal
P 3 →
(∀ x, P x → A) →
(A → ∃ x, R x x ∨ B) →
(∀ x y, R x y → Q (x+y)) →
B ∨ ∃ x, Q (x+x).
Proof.
intros P3 HA H HRQ. destruct H as [x [Rxx|b]]. apply (HA 3), P3.
right. ∃ x. apply HRQ, Rxx.
left. assumption.
Qed.
End predicate_logic.
Goal ~(∀ P Q: nat → Prop,
(∃ x, P x) ∧ (∃ x, Q x) →
(∃ x, P x ∧ Q x)).
Proof.
intro H.
destruct (H (fun x ⇒ x=0) (fun x ⇒ x=1)) as [x [x0 x1]].
split.
∃ 0. reflexivity.
∃ 1. reflexivity.
rewrite x0 in x1. discriminate.
Qed.
Goal ~(∀ P Q: nat → Prop,
(∀ x, P x ∨ Q x) →
(∀ x, P x) ∨ (∀ 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.
This page has been generated by coqdoc