calofmijuck/blog
1
0
Fork 0
mirror of https://github.com/calofmijuck/blog.git synced 2025-12-06 14:53:50 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
23aeb29ad8948526999d5213f0a19feff8ecedd3
blog/_posts/Mathematics/coq/2023-07-08-rules-of-inference.md
Sungchan Yi 23aeb29ad8 feat: breaking change (unstable) (#198) 
* [PUBLISHER] upload files #175

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-19-symmetric-key-encryption.md

* [PUBLISHER] upload files #177

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-19-symmetric-key-encryptio.md

* [PUBLISHER] upload files #178

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #179

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #180

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #181

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #182

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* [PUBLISHER] upload files #183

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #184

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #185

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #186

* PUSH NOTE : 3. Symmetric Key Encryption.md

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

* [PUBLISHER] upload files #187

* PUSH NOTE : 3. Symmetric Key Encryption.md

* PUSH NOTE : 14. Secure Multiparty Computation.md

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

* DELETE FILE : _posts/lecture-notes/modern-cryptography/2023-09-18-symmetric-key-cryptography-2.md

* [PUBLISHER] upload files #188

* PUSH NOTE : 3. Symmetric Key Encryption.md

* PUSH NOTE : 14. Secure Multiparty Computation.md

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

* chore: remove files

* [PUBLISHER] upload files #197

* PUSH NOTE : 수학 공부에 대한 고찰.md

* PUSH NOTE : 09. Lp Functions.md

* PUSH ATTACHMENT : mt-09.png

* PUSH NOTE : 08. Comparison with the Riemann Integral.md

* PUSH ATTACHMENT : mt-08.png

* PUSH NOTE : 04. Measurable Functions.md

* PUSH ATTACHMENT : mt-04.png

* PUSH NOTE : 06. Convergence Theorems.md

* PUSH ATTACHMENT : mt-06.png

* PUSH NOTE : 07. Dominated Convergence Theorem.md

* PUSH ATTACHMENT : mt-07.png

* PUSH NOTE : 05. Lebesgue Integration.md

* PUSH ATTACHMENT : mt-05.png

* PUSH NOTE : 03. Measure Spaces.md

* PUSH ATTACHMENT : mt-03.png

* PUSH NOTE : 02. Construction of Measure.md

* PUSH ATTACHMENT : mt-02.png

* PUSH NOTE : 01. Algebra of Sets and Set Functions.md

* PUSH ATTACHMENT : mt-01.png

* PUSH NOTE : Rules of Inference with Coq.md

* PUSH NOTE : 블로그 이주 이야기.md

* PUSH NOTE : Secure IAM on AWS with Multi-Account Strategy.md

* PUSH ATTACHMENT : separation-by-product.png

* PUSH NOTE : You and Your Research, Richard Hamming.md

* PUSH NOTE : 10. Digital Signatures.md

* PUSH ATTACHMENT : mc-10-dsig-security.png

* PUSH ATTACHMENT : mc-10-schnorr-identification.png

* PUSH NOTE : 9. Public Key Encryption.md

* PUSH ATTACHMENT : mc-09-ss-pke.png

* PUSH NOTE : 8. Number Theory.md

* PUSH NOTE : 7. Key Exchange.md

* PUSH ATTACHMENT : mc-07-dhke.png

* PUSH ATTACHMENT : mc-07-dhke-mitm.png

* PUSH ATTACHMENT : mc-07-merkle-puzzles.png

* PUSH NOTE : 6. Hash Functions.md

* PUSH ATTACHMENT : mc-06-merkle-damgard.png

* PUSH ATTACHMENT : mc-06-davies-meyer.png

* PUSH ATTACHMENT : mc-06-hmac.png

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

* PUSH ATTACHMENT : mc-05-ci.png

* PUSH ATTACHMENT : mc-05-etm-mte.png

* PUSH NOTE : 1. OTP, Stream Ciphers and PRGs.md

* PUSH ATTACHMENT : mc-01-prg-game.png

* PUSH ATTACHMENT : mc-01-ss.png

* PUSH NOTE : 4. Message Authentication Codes.md

* PUSH ATTACHMENT : mc-04-mac.png

* PUSH ATTACHMENT : mc-04-mac-security.png

* PUSH ATTACHMENT : mc-04-cbc-mac.png

* PUSH ATTACHMENT : mc-04-ecbc-mac.png

* PUSH NOTE : 3. Symmetric Key Encryption.md

* PUSH ATTACHMENT : is-03-ecb-encryption.png

* PUSH ATTACHMENT : is-03-cbc-encryption.png

* PUSH ATTACHMENT : is-03-ctr-encryption.png

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

* PUSH ATTACHMENT : mc-02-block-cipher.png

* PUSH ATTACHMENT : mc-02-feistel-network.png

* PUSH ATTACHMENT : mc-02-des-round.png

* PUSH ATTACHMENT : mc-02-DES.png

* PUSH ATTACHMENT : mc-02-aes-128.png

* PUSH ATTACHMENT : mc-02-2des-mitm.png

* PUSH NOTE : 18. Bootstrapping & CKKS.md

* PUSH NOTE : 17. BGV Scheme.md

* PUSH NOTE : 16. The GMW Protocol.md

* PUSH ATTACHMENT : mc-16-beaver-triple.png

* PUSH NOTE : 15. Garbled Circuits.md

* PUSH NOTE : 14. Secure Multiparty Computation.md

* PUSH NOTE : 13. Sigma Protocols.md

* PUSH ATTACHMENT : mc-13-sigma-protocol.png

* PUSH ATTACHMENT : mc-13-okamoto.png

* PUSH ATTACHMENT : mc-13-chaum-pedersen.png

* PUSH ATTACHMENT : mc-13-gq-protocol.png

* PUSH NOTE : 12. Zero-Knowledge Proofs (Introduction).md

* PUSH ATTACHMENT : mc-12-id-protocol.png

* PUSH NOTE : 11. Advanced Topics.md

* PUSH NOTE : 0. Introduction.md

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

* PUSH NOTE : 09. Transport Layer Security.md

* PUSH ATTACHMENT : is-09-tls-handshake.png

* PUSH NOTE : 08. Public Key Infrastructure.md

* PUSH ATTACHMENT : is-08-certificate-validation.png

* 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 ATTACHMENT : is-03-feistel-function.png

* PUSH ATTACHMENT : is-03-cfb-encryption.png

* PUSH ATTACHMENT : is-03-ofb-encryption.png

* PUSH NOTE : 04. Modular Arithmetic (1).md

* PUSH NOTE : 01. Security Introduction.md

* PUSH ATTACHMENT : is-01-cryptosystem.png

* PUSH NOTE : Search Time in Hash Tables.md

* PUSH NOTE : 랜덤 PS일지 (1).md

* chore: rearrange articles

* feat: fix paths

* feat: fix all broken links

* feat: title font to palatino
2024-11-13 14:28:45 +09:00

245 lines
5.4 KiB
Markdown
Raw Blame History

---
share: true
toc: true
math: true
categories:
- Mathematics
- Coq
path: _posts/mathematics/coq
tags:
- math
- coq
- proof-verification
title: Rules of Inference with Coq
date: 2023-07-08
github_title: 2023-07-08-rules-of-inference
---
This is a list of proofs with Coq, for each rule of inference stated in [List of Rules of Inference (Wikipedia)](https://en.wikipedia.org/wiki/List_of_rules_of_inference)
Some rules that need [the law of excluded middle](https://en.wikipedia.org/wiki/Law_of_excluded_middle) are at the end of the section.
## Rules for Negation
```coq
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
```coq
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
```coq
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
```coq
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
```coq
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
```coq
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.
```coq
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](https://github.com/snu-sf/promising-seq-coq) for the paper [Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency](https://dl.acm.org/doi/abs/10.1145/3519939.3523718) but I got carried away...
Reference in New Issue View Git Blame Copy Permalink