(** * 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).
Admitted. (* TODO *)
Lemma Sc: (A -> B -> C) -> (A -> B) -> A -> C.
Admitted. (* TODO *)
(* same proofs, using tactics *)
Lemma id': A -> A.
Proof.
intro H.
apply H.
Qed.
Lemma comp': (A -> B) -> (B -> C) -> (A -> C).
Admitted. (* TODO *)
Lemma Sc': (A -> B -> C) -> (A -> B) -> A -> C.
Admitted. (* TODO *)
(* conjunctions *)
Lemma and_build: A -> B -> A /\ B.
Proof.
intros a b.
split.
apply a.
apply b.
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.
Admitted. (* TODO *)
Lemma and_comm: A /\ B -> (B /\ A).
Admitted. (* TODO *)
Lemma and_assoc: A /\ (B /\ C) -> (A /\ B) /\ C.
Admitted. (* TODO *)
Lemma and_assoc': (A /\ B) /\ C -> A /\ (B /\ C).
Admitted. (* TODO *)
(* disjunctions *)
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).
Admitted. (* TODO *)
Lemma or_assoc: A \/ (B \/ C) -> (A \/ B) \/ C.
Admitted. (* TODO *)
Lemma or_assoc': (A \/ B) \/ C -> A \/ (B \/ C).
Admitted. (* TODO *)
Lemma or_and_distr: A /\ (B \/ C) <-> (A /\ B) \/ (A /\ C).
Proof.
split. (* <-> is a conjunction *)
Admitted. (* TODO *)
Lemma and_or_distr: A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C).
Admitted.
(* efficiency: forward reasoning *)
Lemma fwd: (A -> B) -> (B -> C) -> (B -> C -> D) -> A -> C/\D.
Proof.
intros ab bc bcd a.
assert(b: B).
Admitted. (* TODO *)
(* 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).
Admitted. (* TODO *)
Lemma False_exploit: False -> A.
Proof.
(* use destruct to eliminate False assumptions *)
intro H. destruct H.
Restart.
(* contradict does the same, and maybe more readable *)
intro H. contradict H.
Qed.
Lemma and_not: ~A /\ ~B <-> ~(A \/ B).
Admitted. (* TODO *)
Lemma or_not: ~A \/ ~B -> ~(A /\ B).
Admitted. (* TODO *)
(* NB: the above proofs can all be solved using the tactic [tauto],
which solves precisely all the propositional intuitionistic
tautologies *)
(** Classical logic *)
(* note that the converse 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).
Admitted. (* TODO (without te, of course) *)
(* x *)
Lemma peirce: ((A -> B) -> A) -> A.
Admitted. (* TODO (with or without te ?) *)
End propositional_logic.
(** Predicate logic (we'll resume from here next week, no need to finish this by Friday 18th) *)
(* now we introduce predicates (here, on natural numbers) *)
Section predicate_logic.
Variables P Q: nat -> Prop.
Variable R: nat -> nat -> Prop.
(* universal quantification *)
Goal (forall x, P (2*x) -> Q x) -> P 6 -> Q 3.
Admitted. (* TODO *)
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 *)
Admitted. (* TODO *)
Goal (forall x, P x /\ Q x) -> (forall x, P x) /\ (forall x, Q x).
Admitted. (* TODO *)
Goal (forall x, P x \/ Q x) -> (forall x, P x) \/ (forall x, Q x).
Abort. (* a trap, actually false! *)
(* existential quantification *)
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).
Admitted. (* TODO *)
Goal (exists x, exists y, R x y) <-> (exists y, exists x, R x y).
Admitted. (* TODO *)
Goal (forall x y, R x y -> R y x) ->
(forall x, exists y, R x y) ->
(forall y, exists x, R x y).
Admitted. (* TODO *)
Goal ~(exists x, P x) <-> forall x, ~P x.
Admitted. (* TODO *)
Goal
(exists x, P x \/ Q x) <->
(exists x, P x) \/ (exists x, Q x).
Admitted. (* TODO *)
Goal
(exists x, P x /\ Q x) ->
(exists x, P x) /\ (exists x, Q x).
Admitted. (* TODO *)
(* xx *)
Goal (exists x, ~P x) <-> ~(forall x, P x).
Admitted. (* OPTIONAL, requires excluded middle *)
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).
Admitted. (* TODO *)
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).
Admitted. (* TODO *)
End predicate_logic.
(* xxx *)
Goal ~(forall P Q: nat -> Prop,
(exists x, P x) /\ (exists x, Q x) ->
(exists x, P x /\ Q x)).
Admitted. (* OPTIONAL *)
Goal ~(forall P Q: nat -> Prop,
(forall x, P x \/ Q x) ->
(forall x, P x) \/ (forall x, Q x)).
Admitted. (* OPTIONAL *)