(* week-03_proving-logical-properties.v *) (* LPP 2025 - CS3234 2024-2025, Sem2 *) (* Olivier Danvy *) (* Version of 02 Feb 2025, with renumbered exercises *) (* was: *) (* Version of 31 Jan 2025 *) (* ********** *) Lemma identity : forall A : Prop, A -> A. Proof. intro A. intro H_A. exact H_A. Qed. (* ********** *) Lemma proving_a_conjunction : forall A B : Prop, A -> B -> A /\ B. Proof. intros A B H_A H_B. split. exact H_A. exact H_B. Restart. intros A B H_A H_B. split. { exact H_A. } { exact H_B. } Restart. intros A B H_A H_B. split. - exact H_A. - exact H_B. Restart. intros A B H_A H_B. Check (conj H_A H_B). exact (conj H_A H_B). Qed. (* ********** *) Lemma proving_a_nested_conjunction : forall A B C D : Prop, A -> B -> C -> D -> (A /\ B) /\ (C /\ D). Proof. intros A B C D H_A H_B H_C H_D. split. - split. + exact H_A. + exact H_B. - split. + exact H_C. + exact H_D. Restart. intros A B C D H_A H_B H_C H_D. exact (conj (conj H_A H_B) (conj H_C H_D)). Qed. (* ***** *) Lemma proving_another_nested_conjunction : forall A B C D E F G H : Prop, A -> B -> C -> D -> E -> F -> G -> H -> ((A /\ B) /\ (C /\ D)) /\ ((E /\ F) /\ (G /\ H)). Proof. intros A B C D E F G H H_A H_B H_C H_D H_E H_F H_G H_H. split. - split. + split. * exact H_A. * exact H_B. + split. * exact H_C. * exact H_D. - split. + split. * exact H_E. * exact H_F. + split. * exact H_G. * exact H_H. Restart. intros A B C D E F G H H_A H_B H_C H_D H_E H_F H_G H_H. exact (conj (conj (conj H_A H_B) (conj H_C H_D)) (conj (conj H_E H_F) (conj H_G H_H))). Qed. (* ********** *) Lemma proving_a_ternary_conjunction : forall A B C : Prop, A -> B -> C -> A /\ B /\ C. Proof. intros A B C. intros H_A H_B H_C. split. - exact H_A. - split. + exact H_B. + exact H_C. Restart. intros A B C. intros H_A H_B H_C. exact (conj H_A (conj H_B H_C)). Qed. (* ***** *) Lemma proving_a_quaternary_conjunction : forall A B C D : Prop, A -> B -> C -> D -> A /\ B /\ C /\ D. Proof. intros A B C D. intros H_A H_B H_C H_C. split. - exact H_A. - split. + exact H_B. + split. * exact H_C. * exact H_D. Restart. intros A B C D. intros H_A H_B H_C H_C. exact (conj H_A (conj H_B (conj H_C H_D))). Qed. (* ********** *) Lemma example_for_Anton : forall A B C D : Prop, A /\ B /\ C /\ D. Proof. intros A B C D. split. - admit. - split. + admit. + split. * admit. * admit. Restart. intros A B C D. split. { admit. } { split. { admit. } { split. { admit. } { admit. } } } Restart. intros A B C D. split. { admit. } split. { admit. } split. { admit. } admit. Abort. (* ********** *) Lemma proving_a_disjunction : forall A B : Prop, A -> B -> A \/ B. Proof. intros A B H_A H_B. left. exact H_A. Restart. intros A B H_A H_B. right. exact H_B. Qed. (* ********** *) (* Exercise 07 *) Lemma conjunction_is_commutative : forall A B : Prop, A /\ B <-> B /\ A. Proof. intros A B. split. - intros [H_A H_B]. exact (conj H_B H_A). - intros [H_B H_A]. exact (conj H_A H_B). Qed. Lemma conjunction_is_commutative_aux : forall A B : Prop, A /\ B -> B /\ A. Proof. intros A B [H_A H_B]. exact (conj H_B H_A). Qed. Lemma conjunction_is_commutative_revisited : forall A B : Prop, A /\ B <-> B /\ A. Proof. intros A B. split. - exact (conjunction_is_commutative_aux A B). - exact (conjunction_is_commutative_aux B A). Qed. (* ********** *) (* Exercise 08 *) Lemma conjunction_is_associative : forall A B C : Prop, A /\ (B /\ C) <-> (A /\ B) /\ C. Proof. Abort. (* ********** *) (* Exercise 09 *) Lemma disjunction_is_commutative : forall A B : Prop, A \/ B <-> B \/ A. Proof. Abort. (* ********** *) (* Exercise 10 *) Lemma disjunction_is_associative : forall A B C : Prop, A \/ (B \/ C) <-> (A \/ B) \/ C. Proof. Abort. (* ********** *) (* Exercise 11 *) (* Prove whether disjunction distribute over conjunction on the left and on the right. *) Proposition disjunction_distributes_over_conjunction_on_the_left : forall A B C : Prop, A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C). Proof. intros A B C. split. - intros [H_A | [H_B H_C]]. + split. * left. exact H_A. * left. exact H_A. + split. * right. exact H_B. * right. exact H_C. - intros [[H_A | H_B] [H_A' | H_C]]. (* etc. *) Abort. (* Proposition disjunction_distributes_over_conjunction_on_the_right : ... *) (* ********** *) (* Exercise 12 *) (* Does conjunction distribute over disjunction on the left? And what about on the right? *) (* ********** *) Proposition modus_ponens : forall A B : Prop, A -> (A -> B) -> B. Proof. intros A B. intros H_A H_A_implies_B. Check (H_A_implies_B H_A). exact (H_A_implies_B H_A). Restart. intros A B. intros H_A H_A_implies_B. apply H_A_implies_B. exact H_A. Qed. (* ********** *) (* Exercise 13 *) Proposition following : forall A B : Prop, (A -> B) -> A -> B. Proof. Abort. (* ********** *) Proposition modus_tollens : forall A B : Prop, ~B -> (A -> B) -> ~A. Proof. intros A B. unfold not. intros H_B_implies_False H_A_implies_B H_A. apply H_B_implies_False. apply H_A_implies_B. exact H_A. Restart. intros A B. unfold not. intros H_B_implies_False H_A_implies_B H_A. Check (H_A_implies_B H_A). Check (H_B_implies_False (H_A_implies_B H_A)). exact (H_B_implies_False (H_A_implies_B H_A)). Restart. intros A B. unfold not. intros H_B_implies_False H_A_implies_B H_A. Check (modus_ponens A B). Check (modus_ponens A B H_A). Check (modus_ponens A B H_A H_A_implies_B). Check (H_B_implies_False (modus_ponens A B H_A H_A_implies_B)). exact (H_B_implies_False (modus_ponens A B H_A H_A_implies_B)). Qed. (* ********** *) (* Exercise 14 *) Proposition implication_distributes_over_conjunction_on_the_left : forall A B C : Prop, (A -> B /\ C) <-> ((A -> B) /\ (A -> C)). Proof. intros A B C. split. - intros H_A_implies_B_and_C. split. * intro H_A. Check (H_A_implies_B_and_C H_A). destruct (H_A_implies_B_and_C H_A) as [H_B _]. exact H_B. * intro H_A. destruct (H_A_implies_B_and_C H_A) as [_ H_C]. exact H_C. - intros [H_A_implies_B H_A_implies_C] H_A. Check (H_A_implies_B H_A). Check (H_A_implies_C H_A). Check (conj (H_A_implies_B H_A) (H_A_implies_C H_A)). exact (conj (H_A_implies_B H_A) (H_A_implies_C H_A)). Qed. (* ********** *) (* Exercise 15 *) Proposition implication_distributes_over_disjunction_on_the_right_and_with_a_twist : forall A B C : Prop, ((A \/ B) -> C) <-> ((A -> C) /\ (B -> C)). Proof. intros A B C. split. - intros H_A_or_B_implies_C. split. + intro H_A. apply H_A_or_B_implies_C. left. exact H_A. + intro H_B. apply H_A_or_B_implies_C. right. exact H_B. - intros [H_A_implies_C H_B_implies_C] [H_A | H_B]. + Check (H_A_implies_C H_A). exact (H_A_implies_C H_A). + exact (H_B_implies_C H_B). Qed. (* ********** *) (* Exercise 16 *) Proposition contrapositive_of_implication : forall A B : Prop, (A -> B) -> ~B -> ~A. Proof. intros A B. intros H_A_implies_B H_not_B. Check (modus_tollens A B H_not_B H_A_implies_B). exact (modus_tollens A B H_not_B H_A_implies_B). Qed. (* ********** *) (* Exercise 17 *) Proposition contrapositive_of_contrapositive_of_implication : forall A B : Prop, (~B -> ~A) -> ~~A -> ~~B. Proof. Abort. (* ********** *) (* Exercise 18 *) Proposition double_negation : forall A : Prop, A -> ~~A. Proof. Abort. (* ********** *) (* Postlude *) Fixpoint foo (n : nat) : nat := match n with O => O | S n' => S (S (foo n')) end. Theorem about_foo_v1 : forall x y : nat, foo x = y -> y = 2 * x. Admitted. Theorem about_foo_v2 : forall x y : nat, foo x = y -> 2 * x = y. Admitted. Theorem equivalence_of_about_foo_v1_and_about_foo_v2 : (forall x y : nat, foo x = y -> y = 2 * x) <-> (forall x y : nat, foo x = y -> 2 * x = y). Proof. split. - intros X x y H_foo. symmetry. Check (X x y H_foo). exact (X x y H_foo). - intros X x y H_foo. symmetry. exact (X x y H_foo). Qed. (* ********** *) (* end of week-03_proving-logical-properties.v *)