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

[PUBLISHER] upload files #169

Browse Source
This commit is contained in:
Sungchan Yi
2024-11-12 22:42:25 +09:00
committed by GitHub
parent 7a6e58dac5
commit e1b1ec6fc5
1 changed files with 11 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
_posts/Mathematics/Coq/2023-07-08-rules-of-inference.md
View File

@@ -2,11 +2,16 @@
share: true share: true
toc: true toc: true
math: true math: true
categories: [Mathematics, Coq] categories:
tags: [math, coq, proof-verification] - Mathematics
title: "Rules of Inference with Coq" - Coq
date: "2023-07-08" tags:
github_title: "2023-07-08-rules-of-inference" - 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) 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)
@@ -188,7 +193,7 @@ Lemma distributive_conjunction : forall P Q R : Prop,
Proof. Proof.
split; intros. split; intros.
- destruct H as [H [H1 | H1]]; auto. - destruct H as [H [H1 | H1]]; auto.
- destruct H as [ [H1 H2](H1%20H2.md); auto. - destruct H as [[H1 H2] | [H1 H2]]; auto.
Qed. Qed.
Lemma material_implication_converse : forall P Q : Prop, Lemma material_implication_converse : forall P Q : Prop,