Library s1_prop

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.    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 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.

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 (∀ 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.
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.

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.
This page has been generated by coqdoc