# Propositional logic

Section propositional_logic.

Variables A B C D: Prop.

explicit proofs, illustrating the Curry-Howard correspondence

Lemma id: AA.
Proof (fun xx).

Lemma comp: (AB) → (BC) → (AC).
Proof (fun f g xg (f x)).

Lemma Sc: (ABC) → (AB) → AC.
Proof (fun f g xf x (g x)).

## intro / apply

Lemma id': AA.
Proof.
intro H.
apply H.
Qed.

Lemma comp': (AB) → (BC) → (AC).
Proof.
backward reasoning
intros HAB HBC HA.
apply HBC.
apply HAB.
apply HA.
Qed.

Lemma comp'': (AB) → (BC) → (AC).
Proof.
forward reasoning
intros HAB HBC HA.
apply HAB in HA.
apply HBC in HA.
apply HA.
Qed.

Lemma comp''': (AB) → (BC) → (AC).
Proof.
intermediate style
intros HAB HBC HA.
apply HAB in HA.
apply (HBC HA).
Qed.

Lemma Sc': (ABC) → (AB) → AC.
Proof.
intros f g x.
apply f.
apply x.
apply g, x.
Qed.

## conjunctions: destruct/split

Lemma and_build: ABAB.
Proof.
intros a b.
split.
apply a.
apply b.
Qed.

Lemma and_build': ABAB.
Proof.
intros.
split.
assumption.
assumption.
Qed.

Lemma and_build'': ABAB.
Proof.
intros.
split; assumption.
Qed.

Lemma and_exploit_l: ABA.
Proof.
intro H.
destruct H as [HA HB].
apply HA.
Qed.

Lemma and_exploit_r: ABB.
Proof.
intros [HA HB].
assumption.
Qed.

Lemma and_comm: AB → (BA).
Proof.
intros [? ?].
split; assumption.
Qed.

Lemma and_assoc: A ∧ (BC) → (AB) ∧ 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 ∧ (BC) → (AB) ∧ C.
Proof.
intros [HA [HB HC]].
repeat split; assumption.
Qed.

## disjunctions: destruct/left/right

Lemma or_build_l: AAB.
Proof.
intro HA.
left.
apply HA.
Qed.

Lemma or_exploit: AB → (AC) → (BC) → C.
Proof.
intros H HAC HBC.
destruct H as [HA|HB].
apply HAC, HA.
apply HBC, HB.
Qed.

Lemma or_comm: AB → (BA).
Proof.
intro H.
destruct H as [HA|HB].
right. apply HA.
left. apply HB.
Qed.

Lemma or_assoc: A ∨ (BC) → (AB) ∨ 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 ∨ (BC) → (AB) ∨ C.
Proof.
intros [HA|[HB|HC]].
left. left. assumption.
left. right. assumption.
right. assumption.
Qed.

Lemma or_and_distr: A ∧ (BC) ↔ (AB) ∨ (AC).
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 ∨ (BC) ↔ (AB) ∧ (AC).
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: (AB) → (BC) → (BCD) → ACD.
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: ~(~AA).
Proof. intros [HnA HA]. apply HnA, HA. Qed.

Lemma False_exploit: FalseA.
Proof.
use contradict or destruct to eliminate False assumptions
Restart.
intro H. destruct H.
Restart.
intros [].
Qed.

Lemma and_not: ¬A ∧ ¬B ↔ ~(AB).
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 → ~(AB).
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: P, P ∨ ¬P.

Lemma or_not': ~(AB) → ¬A ∨ ¬B.
Proof.
intro H.
destruct (te A).
destruct (te B).
split; assumption.
right. assumption.
left. assumption.
Qed.

Lemma nn_te: ( P, P\/~P) ↔ ( P, ~~PP).
Proof.
split.
intros te' P HP. destruct (te' P).
assumption.
intros nn P. apply nn. intro E.
apply E. right. intro p. apply E. left. apply p.
Qed.

Lemma peirce: ((AB) → 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: natProp.
Variable R: natnatProp.

## universal quantification: intro/apply

Goal ( x, P (2*x) → Q x) → P 6 → Q 3.
Proof. intros H H6. apply H, H6. Qed.

Goal ( x, P xR 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 xQ 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) ∨ ( x, Q x) → ( x, P xQ 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 xQ 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 yR 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 xQ 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 xQ 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_te. apply te.
intro H'. apply H. intro x.
destruct (te (P x)) as [Hx|Hnx].
assumption.
destruct H'. x. assumption.
Qed.

Variables A B C: Prop.

Goal
P 3 →
( x, P xA) →
(A x, R x xB) →
( x y, R x yQ (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 xA) →
(A x, R x xB) →
( x y, R x yQ (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: natProp,
( x, P x) ∧ ( x, Q x) →
( x, P xQ x)).
Proof.
intro H.
destruct (H (fun xx=0) (fun xx=1)) as [x [x0 x1]].
split.
0. reflexivity.
1. reflexivity.
rewrite x0 in x1. discriminate.
Qed.

Goal ~( P Q: natProp,
( x, P xQ x) →
( x, P x) ∨ ( x, Q x)).
Proof.
intro H.
destruct (H (fun xx=0) (fun xx<>0)) as [H'|H'].
intro x. destruct x. left. reflexivity. right. discriminate.
specialize (H' 1). discriminate.
destruct (H' 0). reflexivity.
Qed.