Library s1_prop

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
  intro H. contradict H.
  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).
    contradict H.
     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.
    now contradict HP.
   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.

This page has been generated by coqdoc