mirror of
https://github.com/calofmijuck/blog.git
synced 2025-12-06 14:53:50 +00:00
fix: long descriptions appearing in meta tag (#42)
* fix: delete all posts * chore: Pull-Request [blog-7-12-2023] from Obsidian (#41) * PUSH NOTE : 수학 공부에 대한 고찰.md * PUSH NOTE : Rules of Inference with Coq.md * PUSH NOTE : 블로그 이주 이야기.md * PUSH ATTACHMENT : blog-logo.png * PUSH ATTACHMENT : github-publisher.png * PUSH NOTE : 10. StatefulSets - Deploying Replicated Stateful Applications.md * PUSH ATTACHMENT : k8s-10.jpeg * PUSH NOTE : 09. Deployments - Updating Applications Declaratively.md * PUSH ATTACHMENT : k8s-09.jpeg * PUSH NOTE : 08. Accessing Pod Metadata and Other Resources from Applications.md * PUSH ATTACHMENT : k8s-08.jpeg * PUSH NOTE : 07. ConfigMaps and Secrets - Configuring Applications.md * PUSH ATTACHMENT : k8s-07.jpeg * PUSH NOTE : 06. Volumes - Attaching Disk Storage to Containers.md * PUSH ATTACHMENT : k8s-06.jpeg * PUSH NOTE : 05. Services - Enabling Clients to Discover and Talk to Pods.md * PUSH ATTACHMENT : k8s-05.jpeg * PUSH NOTE : 04. Replication and Other Controllers - Deploying Managed Pods.md * PUSH ATTACHMENT : k8s-04.jpeg * PUSH NOTE : 03. Pods - Running Containers in Kubernetes.md * PUSH ATTACHMENT : k8s-03.jpeg * PUSH NOTE : 02. First Steps with Docker and Kubernetes.md * PUSH ATTACHMENT : k8s-02.jpeg * PUSH NOTE : 01. Introducing Kubernetes.md * PUSH ATTACHMENT : k8s-01.jpeg * DELETE FILE : _posts/Development/Kubernetes/2021-02-28-01-introducing-kubernetes.md * DELETE FILE : _posts/Development/Kubernetes/2021-03-07-02-first-steps-with-docker-and-kubernetes.md * DELETE FILE : _posts/Development/Kubernetes/2021-03-21-04-replication-and-other-controllers.md * DELETE FILE : _posts/Development/Kubernetes/2021-04-18-08-accessing-pod-metadata-and-other-resources-from-applications.md * DELETE FILE : _posts/Mathematics/Coq/2023-07-08-rules-of-inference-with-coq.md
This commit is contained in:
GitHub
@@ -5,7 +5,7 @@ categories: [Development, Kubernetes]
|
||||
tags: [kubernetes, sre, devops, docker]
|
||||
title: "01. Introducing Kubernetes"
|
||||
date: "2021-02-28"
|
||||
github_title: "2021-02-28-01-introducing-kubernetes"
|
||||
github_title: "2021-02-28-01-introducing-k8s"
|
||||
image:
|
||||
path: /assets/img/posts/k8s-01.jpeg
|
||||
---
|
||||
@@ -5,7 +5,7 @@ categories: [Development, Kubernetes]
|
||||
tags: [kubernetes, sre, devops, docker]
|
||||
title: "02. First Steps with Docker and Kubernetes"
|
||||
date: "2021-03-07"
|
||||
github_title: "2021-03-07-02-first-steps-with-docker-and-kubernetes"
|
||||
github_title: "2021-03-07-02-first-steps"
|
||||
image:
|
||||
path: /assets/img/posts/k8s-02.jpeg
|
||||
---
|
||||
@@ -5,7 +5,7 @@ categories: [Development, Kubernetes]
|
||||
tags: [kubernetes, sre, devops]
|
||||
title: "04. Replication and Other Controllers: Deploying Managed Pods"
|
||||
date: "2021-03-21"
|
||||
github_title: "2021-03-21-04-replication-and-other-controllers"
|
||||
github_title: "2021-03-21-04-replication-and-controllers"
|
||||
image:
|
||||
path: /assets/img/posts/k8s-04.jpeg
|
||||
---
|
||||
@@ -17,6 +17,7 @@ image:
|
||||
Pod 들은 스케쥴링 되고 스케일링 되기 때문에 IP 주소가 자주 바뀔 수 있으며, pod 가 시작된 후 IP 주소가 할당될 뿐만 아니라, 하나의 서비스를 위해 pod 를 여러 개 사용하는 경우 하나의 IP 를 사용하여 여러 개의 pod 에 접근할 방법이 필요하다. (쿠버네티스를 사용하지 않으면 고정 IP 등을 사용하거나 따로 설정된 주소로 요청이 가도록 했을 것이다)
|
||||
|
||||
## 5.1 Services 소개
|
||||
---
|
||||
|
||||
Service 를 이용하면 같은 일을 하는 여러 개의 pod 에 하나의 entrypoint 를 제공할 수 있다.
|
||||
|
||||
@@ -142,6 +143,7 @@ FQDN 은 대략 이런 모양이다.
|
||||
정확히는, `ping` 명령어는 ICMP 위에서 동작한다. 그런데 service 의 클러스터 내부에서 특정 포트만 사용하기 때문에 ICMP request 에 응답하지 않으므로 `ping` 이 불가능하다.
|
||||
|
||||
## 5.2 클러스터 외부의 service 에 접속하기
|
||||
---
|
||||
|
||||
### 5.2.1 Service endpoints
|
||||
|
||||
@@ -168,6 +170,7 @@ Label selector 를 지정하면 endpoints 가 자동으로 관리되고, label s
|
||||
`ExternalName` service 들은 DNS 레벨에서 구현되어 있어서 `CNAME` record 가 생성된다. 이 service 에 접속을 시도하는 client 들은 외부 서비스에 직접 접속하며, service 에는 IP 가 할당 되지 않는다.
|
||||
|
||||
## 5.3 Service 를 외부에 공개하기
|
||||
---
|
||||
|
||||
프론트엔드의 경우 외부로 공개할 필요가 있다. 공개하는 방법에는 세 가지 방법이 있다.
|
||||
|
||||
@@ -220,6 +223,7 @@ Service 타입을 `LoadBalancer` 로 설정하면 된다. 다만 cloud infrastru
|
||||
`NodePort` service 를 통해 외부에서 접근하게 되면 SNAT 로 인해 source IP 가 변경된다. (내부에서는 무관) 그런데 만약 애플리케이션이 source IP 를 필요로 한다면 문제가 될 수도 있다.
|
||||
|
||||
## 5.4 Ingress resource
|
||||
---
|
||||
|
||||
### Ingress 가 필요한 이유
|
||||
|
||||
@@ -325,6 +329,7 @@ spec:
|
||||
```
|
||||
|
||||
## 5.5 연결을 받을 준비가 되었을 때 신호 보내기
|
||||
---
|
||||
|
||||
Service 나 Ingress 를 사용하면 pod 가 생성되자마자 요청이 전달될 수 있다. (label 만 검사하므로) 한편 startup 이 오래걸리는 애플리케이션의 경우 아직 pod 는 준비가 안되었는데 요청을 받게 되어 요청을 정상적으로 처리 못하게 될 수 있다.
|
||||
|
||||
@@ -369,6 +374,7 @@ ReplicationController 의 pod template 을 수정하면 현재 존재하는 pod
|
||||
Shutdown 이 시작되었음을 감지하고 readiness probe 가 실패하도록 로직을 짤 필요는 없다. Pod 가 삭제되면 쿠버네티스가 자동으로 service endpoints 에서 제거한다.
|
||||
|
||||
## 5.6 Headless service for discovering individual pods
|
||||
---
|
||||
|
||||
Client 가 모든 pod 에 접근해야 한다면? (어떤 경우에 이러한가? - 아래 Discussion 참고)
|
||||
|
||||
@@ -395,6 +401,7 @@ $ kubectl run <POD_NAME> --image=<IMAGE_NAME> --generator=run-pod/v1
|
||||
Service 에서 `publishNotReadyAddresses=True` 로 설정하면 된다.
|
||||
|
||||
## 5.7 Troubleshooting
|
||||
---
|
||||
|
||||
순서대로 해보면 좋을 것이다!
|
||||
|
||||
|
||||
@@ -15,6 +15,7 @@ image:
|
||||
컨테이너가 재시작되면 기존 작업 내역이 모두 사라지게 될 수 있으므로, 컨테이너의 작업 내역을 저장하고 같은 pod 내의 다른 컨테이너가 함께 사용하는 저장 공간이다.
|
||||
|
||||
## 6.1 Introducing volumes
|
||||
---
|
||||
|
||||
Pod 의 한 구성 부분으로 pod spec 에 정의되어 있다. 또 standalone Kubernetes object 가 아니라서 독립적으로 생성되거나 삭제될 수 없다.
|
||||
|
||||
@@ -37,6 +38,7 @@ Pod 내의 모든 컨테이너로부터 접근이 가능하지만, 그렇게 하
|
||||
- `persistentVolumeClaim`: pre- or dynamically provisioned persistent storage
|
||||
|
||||
## 6.2 Volume 을 이용한 컨테이너간 데이터 공유
|
||||
---
|
||||
|
||||
### 6.2.1 `emptyDir` volume
|
||||
|
||||
@@ -132,6 +134,7 @@ Docker Hub 에서 `git sync` 를 검색하면 많은 이미지들이 나올 것
|
||||
(어쩐지, 위 예시 코드 작동 안하더라.)
|
||||
|
||||
## 6.3 노드의 파일 시스템에 접근하기
|
||||
---
|
||||
|
||||
보통 pod 들은 자신이 어떤 노드 위에서 돌아가고 있는지 알 필요가 없기 때문에 노드의 파일 시스템에 접근할 일이 없다. 하지만 시스템 레벨의 pod 들은 (DaemonSet 이라던가) 노드의 파일을 읽어야 하는 경우가 생길 수도 있다. 이런 경우에는 `hostPath` 볼륨을 사용한다.
|
||||
|
||||
@@ -150,6 +153,7 @@ Docker Hub 에서 `git sync` 를 검색하면 많은 이미지들이 나올 것
|
||||
Single-node 클러스터에서는 `hostPath` volume 을 persistent storage 로 사용할 수 있다. (Minikube) 아무튼 multi-node 클러스터에서는 여러 pod 들 간에 데이터를 공유하거나 persistent storage 로 사용해서는 안된다.
|
||||
|
||||
## 6.4 Persistent storage
|
||||
---
|
||||
|
||||
Pod 들 간에 데이터를 공유해야 한다면, 위에서 언급한 volume type 들은 사용할 수 없다. 클러스터 내의 임의의 노드에서 접근이 가능해야하기 때문에 NAS (network attached storage) 급의 저장장치가 필요하다.
|
||||
|
||||
@@ -168,6 +172,7 @@ GCE Persistent Disk 를 생성하고, 이를 mount 한 pod 에서 DB 에 뭔가
|
||||
|
||||
|
||||
## 6.5 스토리지 기술과 pod 를 분리하기
|
||||
---
|
||||
|
||||
개발자는 물리적 저장소에 대한 정보를 몰라야 한다! 그것은 클러스터 관리자가 할 일이다.
|
||||
|
||||
@@ -277,6 +282,7 @@ Pod 과 PVC 를 지우고 `kubectl get pv` 를 해보면 `Released` 상태로
|
||||
다른 reclaim policy 로는 `Recycle`, `Delete` 가 있다. `Recycle` 은 지우고 새로 만들어서 다른 PVC 가 사용할 수 있도록 한다. `Delete` 는 그냥 지워버린다.
|
||||
|
||||
## 6.6 Dynamic provisioning of PersistentVolumes
|
||||
---
|
||||
|
||||
위에서 살펴본 방식대로 PVC 를 사용하는 것도 편하지만, 여전히 클러스터 관리자가 PV 를 생성해야한다는 점에서 불편하다. 쿠버네티스는 PV 의 dynamic provisioning 을 제공하여 스토리지를 자동으로 만들어준다.
|
||||
|
||||
|
||||
@@ -5,7 +5,7 @@ categories: [Development, Kubernetes]
|
||||
tags: [kubernetes, sre, devops]
|
||||
title: "08. Accessing Pod Metadata and Other Resources from Applications"
|
||||
date: "2021-04-18"
|
||||
github_title: "2021-04-18-08-accessing-pod-metadata-and-other-resources-from-applications"
|
||||
github_title: "2021-04-18-08-accessing-pod-metadata"
|
||||
image:
|
||||
path: /assets/img/posts/k8s-08.jpeg
|
||||
---
|
||||
@@ -1,238 +0,0 @@
|
||||
---
|
||||
share: true
|
||||
toc: true
|
||||
math: true
|
||||
categories: [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-with-coq"
|
||||
---
|
||||
|
||||
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%20H2.md); 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...
|
||||
238
_posts/Mathematics/Coq/2023-07-08-rules-of-inference.md
Normal file
238
_posts/Mathematics/Coq/2023-07-08-rules-of-inference.md
Normal file
@@ -0,0 +1,238 @@
|
||||
---
|
||||
share: true
|
||||
toc: true
|
||||
math: true
|
||||
categories: [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%20H2.md); 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
Block a user