blog/2023-07-08-rules-of-inference.md at c9f7af5f3d15c26d9e94ee06bcc4f00b804858c4

mirror of https://github.com/calofmijuck/blog.git synced 2025-12-06 14:53:50 +00:00

Files

Sungchan Yi 6960edd3d4 [PUBLISHER] upload files #170

* PUSH NOTE : 05. Lebesgue Integration.md

* PUSH NOTE : 04. Measurable Functions.md

* PUSH NOTE : 03. Measure Spaces.md

* PUSH NOTE : 02. Construction of Measure.md

* PUSH NOTE : Rules of Inference with Coq.md

* PUSH NOTE : 9. Public Key Encryption.md

* PUSH NOTE : 7. Key Exchange.md

* PUSH NOTE : 6. Hash Functions.md

* PUSH NOTE : 5. CCA-Security and Authenticated Encryption.md

* PUSH NOTE : 2. PRFs, PRPs and Block Ciphers.md

* PUSH NOTE : 14. Secure Multiparty Computation.md

* PUSH NOTE : 07. Public Key Cryptography.md

* PUSH NOTE : 06. RSA and ElGamal Encryption.md

* PUSH NOTE : 05. Modular Arithmetic (2).md

* PUSH NOTE : 03. Symmetric Key Cryptography (2).md

* PUSH NOTE : 02. Symmetric Key Cryptography (1).md

* DELETE FILE : _posts/Lecture Notes/Modern Cryptography/2023-10-19-public-key-encryption.md

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-10-09-public-key-cryptography.md

2024-11-13 10:49:03 +09:00

5.4 KiB

Raw Blame History

share, toc, math, categories, tags, title, date, github_title

toc

math

Rules for Negation

Lemma reductio_ad_absurdum : forall P Q : Prop,
  (P -> Q) -> (P -> ~Q) -> ~P.
Proof.
  intros. intros HP.
  apply H0 in HP as HNQ.
  apply H in HP as HQ.
  contradiction.
Qed.

Lemma ex_contradictione_quodlibet : forall P Q : Prop,
  P -> ~P -> Q.
Proof. intros. contradiction. Qed.

Lemma double_negation_introduction : forall P : Prop,
  P -> ~~P.
Proof. auto. Qed.

Rules for Conditionals

Lemma modus_ponens : forall P Q : Prop,
  (P -> Q) -> P -> Q.
Proof. auto. Qed.

Lemma modus_tollens : forall P Q : Prop,
  (P -> Q) -> ~Q -> ~P.
Proof. auto. Qed.

Rules for Conjunctions

Lemma conjuction_introduction : forall P Q : Prop,
  P -> Q -> P /\ Q.
Proof. auto. Qed.

Lemma conjunction_elimination_left : forall P Q : Prop,
  P /\ Q -> P.
Proof. intros P Q [HP HQ]; auto. Qed.

Lemma conjunction_elimination_right : forall P Q : Prop,
  P /\ Q -> Q.
Proof. intros P Q [HP HQ]; auto. Qed.

Lemma conjunction_commutative : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros. destruct H; split; auto.
Qed.

Lemma conjunction_associative : forall P Q R : Prop,
  (P /\ Q) /\ R -> P /\ (Q /\ R).
Proof.
  intros. destruct H as [H H1]; destruct H; split; auto.
Qed.

Rules for Disjunctions

Lemma disjunction_introduction_left : forall P Q : Prop,
  P -> P \/ Q.
Proof. auto. Qed.

Lemma disjunction_introduction_right : forall P Q : Prop,
  Q -> P \/ Q.
Proof. auto. Qed.

Lemma disjunction_elimination : forall P Q R : Prop,
  (P -> R) -> (Q -> R) -> (P \/ Q) -> R.
Proof.
  intros. destruct H1; auto.
Qed.

Lemma disjunctive_syllogism_left : forall P Q : Prop,
  (P \/ Q) -> ~P -> Q.
Proof.
  intros. destruct H; auto. contradiction.
Qed.

Lemma disjunctive_syllogism_right : forall P Q : Prop,
  (P \/ Q) -> ~Q -> P.
Proof.
  intros. destruct H; auto. contradiction.
Qed.

Lemma constructive_dilemma : forall P Q R S : Prop,
  (P -> R) -> (Q -> S) -> (P \/ Q) -> (R \/ S).
Proof.
  intros. destruct H1; auto.
Qed.

Lemma disjunction_commutative : forall P Q : Prop,
  P \/ Q -> Q \/ P.
Proof. intros. destruct H; auto. Qed.

Lemma disunction_associative : forall P Q R : Prop,
  (P \/ Q) \/ R -> P \/ (Q \/ R).
Proof.
  intros. destruct H as [H | H]; auto.
  destruct H; auto.
Qed.

Rules for Biconditionals

Lemma biconditional_introduction : forall P Q : Prop,
  (P -> Q) -> (Q -> P) -> (P <-> Q).
Proof. split; auto. Qed.

Lemma biconditional_elimination_left_mp : forall P Q : Prop,
  (P <-> Q) -> P -> Q.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_right_mp : forall P Q : Prop,
  (P <-> Q) -> Q -> P.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_left_mt : forall P Q : Prop,
  (P <-> Q) -> ~P -> ~Q.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_right_mt : forall P Q : Prop,
  (P <-> Q) -> ~Q -> ~P.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_disjunction : forall P Q : Prop,
  (P <-> Q) -> (P \/ Q) -> (P /\ Q).
Proof.
  intros. destruct H, H0; auto.
Qed.

Lemma biconditional_elimination_disjunction_not : forall P Q : Prop,
  (P <-> Q) -> (~P \/ ~Q) -> (~P /\ ~Q).
Proof.
  intros. destruct H, H0; auto.
Qed.

Other Rules

Lemma exportation : forall P Q R : Prop,
  (P /\ Q) -> R <-> (P -> Q -> R).
Proof.
  split; auto.
  destruct H; auto.
Qed.

Lemma distributive_disjunction : forall P Q R : Prop,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  split; intros.
  - destruct H as [H | [H1 H2]]; split; auto.
  - destruct H as [H1 H2]; destruct H1, H2; auto.
Qed.

Lemma distributive_conjunction : forall P Q R : Prop,
  P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
Proof.
  split; intros.
  - destruct H as [H [H1 | H1]]; auto.
  - destruct H as [[H1 H2] | [H1 H2]]; auto.
Qed.

Lemma material_implication_converse : forall P Q : Prop,
  (~P \/ Q) -> (P -> Q).
Proof.
  intros. destruct H; auto. contradiction.
Qed.

Lemma resolution : forall P Q R : Prop,
  (P \/ Q) -> (~P \/ R) -> (Q \/ R).
Proof.
  intros. destruct H, H0; auto. contradiction.
Qed.

Rules that require Excluded Middle

We declare the law of excluded middle as an axiom.

Axiom excluded_middle : forall P : Prop, P \/ ~P.

Lemma double_negation_elimination : forall P : Prop,
  ~~P -> P.
Proof.
  intros. destruct (excluded_middle P); auto. contradiction.
Qed.

Lemma material_implication : forall P Q : Prop,
  (P -> Q) -> (~P \/ Q).
Proof.
  intros. destruct (excluded_middle P); auto.
Qed.

Lemma reductio_ad_absurdum_neg : forall P Q : Prop,
  (~P -> Q) -> (~P -> ~Q) -> P.
Proof.
  intros. destruct (excluded_middle P); auto.
  apply H in H1 as HQ.
  apply H0 in H1 as HNQ.
  contradiction.
Qed.

I was supposed to be reading the source for the paper Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency but I got carried away...

5.4 KiB Raw Blame History