calofmijuck/blog
1
0
Fork 0
mirror of https://github.com/calofmijuck/blog.git synced 2025-12-06 22:53:51 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
3c4ace39b2eb887a410b53dbf27a6cb9c464b13a
blog/_posts/Mathematics/Coq/2023-07-08-rules-of-inference.md
Sungchan Yi 6be7f42f68 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
2023-07-13 10:36:00 +09:00

5.4 KiB
Raw Blame History

share, toc, math, categories, tags, title, date, github_title
share toc math categories tags title date github_title
true true true
Mathematics
Coq
math
coq
proof-verification
Rules of Inference with Coq 2023-07-08 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)

Some rules that need the law of excluded middle are at the end of the section.

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%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.

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...