Abstract
LOGIC is a Coq library for formalizing logic studies, concerning both logics’ applications and logics themselves (meta-theories). For applications, users can port derived rules and efficient proof automation tactics from LOGIC to their own program-logic-based verification projects. For meta-theories, users can easily formalize a standard soundness proof or a Henkin-style completeness proof for logics like classical/intuitionistic propositional logic, separation logic and modal logic with LOGIC’s help. In this paper, we present how compositional and portable proof engineering is possible in LOGIC.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A link to the repository of LOGIC: https://github.com/QinxiangCao/LOGIC.
- 2.
References
Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1
Appel, A.W.: Verifiable C, chap. 5–17, 21, 35–39 (2016)
Barras, B., et al.: The coq Proof Assistant reference manual. Technical report, INRIA (1998)
Benzmüller, C., Claus, M., Sultana, N.: Systematic verification of the modal logic cube in Isabelle/Hol. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, 2–3 August 2015. EPTCS, vol. 186, pp. 27–41 (2015), https://doi.org/10.4204/EPTCS.186.5
Benzmüller, C., Woltzenlogel Paleo, B.: Interacting with modal logics in the coq proof assistant. In: Beklemishev, L.D., Musatov, D.V. (eds.) CSR 2015. LNCS, vol. 9139, pp. 398–411. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20297-6_25
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5
Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-FLOYD: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1–4), 367–422 (2018). https://doi.org/10.1007/s10817-018-9457-5
Cao, Q., Cuellar, S., Appel, A.W.: Bringing order to the separation logic jungle. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 190–211. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-71237-6_10
Chlipala, A.: The bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: Morrisett, G., Uustalu, T. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, USA - 25–27 September 2013, pp. 391–402. ACM (2013). https://doi.org/10.1145/2500365.2500592
Ebbinghaus, H., Flum, J., Thomas, W.: Mathematical Logic. Undergraduate Texts in Mathematics, vol. 291, 2nd edn. Springer, Cham (1994). https://doi.org/10.1007/978-3-030-73839-6
Forster, Y., Kirst, D., Wehr, D.: Completeness theorems for first-order logic analysed in constructive type theory. J. Log. Comput. 31(1), 112–151 (2021). https://doi.org/10.1093/logcom/exaa073
Forster, Y., Larchey-Wendling, D.: Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14–15 January 2019, pp. 104–117. ACM (2019). https://doi.org/10.1145/3293880.3294096
Henz, M., Hobor, A.: Teaching experience: logic and formal methods with coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 199–215. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_16
Jensen, J.B.: Techniques for model construction in separation logic. Ph.D. thesis, IT University of Copenhagen, March 2014. https://public.knef.dk.s3-website-us-east-1.amazonaws.com/research/sltut.pdf
Jung, R., Jourdan, J., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL), 66:1–66:34 (2018). https://doi.org/10.1145/3158154
Jung, R., et al.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15–17 January 2015, pp. 637–650. ACM (2015). https://doi.org/10.1145/2676726.2676980
Krebbers, R., et al.: Mosel: a general, extensible modal framework for interactive proofs in separation logic. PACMPL. 2(ICFP), 77:1–77:30 (2018). https://doi.org/10.1145/3236772
Mendelson, E.: Introduction to Mathematical Logic, 3rd edn. Chapman and Hall, London (1987)
Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0030541
Pierce, B.C., et al.: Software foundations. Webpage: https://wwwcis.upenn.edu/bcpierce/sf/current/index.html (2010)
Sieczkowski, F., Bizjak, A., Birkedal, L.: ModuRes: a COQ library for modular reasoning about concurrent higher-order imperative programming languages. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 375–390. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_25
Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_23
Tews, H.: Formalizing cut elimination of coalgebraic logics in COQ. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 257–272. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40537-2_22
Acknowledgement
This research is sponsored by National Natural Science foundation of China (NSFC) Grant No. 61902240.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Sample Use Cases of Logic Generator
A Sample Use Cases of Logic Generator
1.1 A.1 Demo1: Intuitionistic Propositional Logic
Primitive connectives: \(\rightarrow , \wedge , \vee , \bot \).
Syntactic sugar for connectives: \(\varphi \leftrightarrow \psi \triangleq (\varphi \rightarrow \psi )\wedge (\psi \rightarrow \varphi )\), \(\lnot \varphi \triangleq \varphi \rightarrow \bot \), \(\top \triangleq \bot \rightarrow \bot \).
Primitive judgements: provable (\(\vdash \varphi \)).
Syntactic sugar for judgements: \(\text {for any }\varPhi \ \varphi ,\ \varPhi \vdash \varphi \ \text {iff. }\text {exists} \ \varphi _1, \varphi _2, \dots , \varphi _n \in \varPhi , \ \text {s.t.} \ \vdash \varphi _1 \rightarrow \varphi _2 \rightarrow \dots \rightarrow \varphi _n \rightarrow \varphi \).
Primary rules:
-
PeirceLaw: \(\text {for any }\varphi \ \psi ,\ \vdash ((\varphi \rightarrow \psi )\rightarrow \psi )\rightarrow \psi \);
-
FalsepElim: \(\text {for any }\varphi ,\ \vdash \bot \rightarrow \varphi \);
-
OrpIntros1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\varphi \vee \psi )\);
-
OrpIntros2: \(\text {for any }\varphi \ \psi ,\ \vdash \psi \rightarrow (\varphi \vee \psi )\);
-
OprElim: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \chi )\rightarrow (\psi \rightarrow \chi )\rightarrow ((\varphi \vee \psi )\rightarrow \chi )\);
-
AndpIntros: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow \psi \rightarrow (\varphi \wedge \psi )\);
-
AndpElim1: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \varphi \);
-
AndpElim2: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \psi \);
-
ModusPones: \(\text {for any }\varphi \ \psi ,\ \text {if }\vdash \varphi \rightarrow \psi \text { and }\vdash \varphi ,\text { then }\vdash \psi \);
-
Axiom1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\psi \rightarrow \varphi )\);
-
Axiom2: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \chi )\).
1.2 A.2 Demo2: A Very Small Logic
Primitive connectives: \(\rightarrow \).
Primitive judgements: provable (\(\vdash \varphi \)).
Primary rules:
-
ModusPones: \(\text {for any }\varphi \ \psi ,\ \text {if }\vdash \varphi \rightarrow \psi \text { and }\vdash \varphi ,\text { then }\vdash \psi \);
-
Axiom1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\psi \rightarrow \varphi )\);
-
Axiom2: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \chi )\).
1.3 A.3 Demo3: Intuitionistic Propositional Logic
Primitive connectives: \(\rightarrow , \wedge , \vee , \bot \).
Syntactic sugar for connectives: \(\varphi \leftrightarrow \psi \triangleq (\varphi \rightarrow \psi )\wedge (\psi \rightarrow \varphi )\), \(\lnot \varphi \triangleq \varphi \rightarrow \bot \), \(\top \triangleq \bot \rightarrow \bot \), \(\bigwedge _{i=1}^n\varphi _i\triangleq \varphi _1\wedge \ldots \wedge \varphi _n\).
Primitive judgements: derivable \(\varPhi \vdash \varphi \).
Syntactic sugar for judgements: \(\text {for any }\varphi ,\ \vdash \varphi \text { iff. }\emptyset \vdash \varphi \).
Primary rules:
-
DedFalsepElim: \(\text {for any }\varPhi \ \varphi , \text { if }\varPhi \vdash \bot ,\text { then }\varPhi \vdash \varphi \);
-
DedOrpIntros1: \(\text {for any }\varPhi \ \varphi \ \psi ,\text { if }\varPhi \vdash \varphi ,\text { then }\varPhi \vdash \varphi \vee \psi \);
-
DedOrpIntros1: \(\text {for any }\varPhi \ \varphi \ \psi ,\text { if }\varPhi \vdash \psi ,\text { then }\varPhi \vdash \varphi \vee \psi \);
-
DedOrpElim: \(\text {for any }\varPhi \ \varphi \ \psi \ \chi , \text { if }\varPhi \cup \varphi \vdash \chi \text { and }\varPhi \cup \psi \vdash \chi ,\text { then }\varPhi \cup (\varphi \vee \psi )\vdash \chi \);
-
DedAndpIntros: \(\text {for any }\varPhi \ \varphi \ \psi ,\text { if }\varPhi \vdash \varphi \text { and }\varPhi \vdash \psi ,\text { then }\varPhi \vdash \varphi \wedge \psi \);
-
DedAndpElim1: \(\text {for any }\varPhi \ \varphi \ \psi ,\text { if }\varPhi \vdash \varphi \wedge \psi ,\text { then }\varPhi \vdash \varphi \);
-
DedAndpElim2: \(\text {for any }\varPhi \ \varphi \ \psi ,\text { if }\varPhi \vdash \varphi \wedge \psi ,\text { then }\varPhi \vdash \psi \);
-
DedModusPonens: \(\text {for any }\varPhi \ \varphi \ \psi ,\text { if }\varPhi \vdash \varphi \text { and }\varPhi \vdash \varphi \rightarrow \psi ,\text { then }\varPhi \vdash \psi \);
-
DedImppIntros: \(\text {for any }\varPhi \ \varphi \ \psi ,\text { if }\varPhi \cup \varphi \vdash \psi ,\text { then }\varPhi \vdash \varphi \rightarrow \psi \);
-
DedWeaken: \(\text {for any }\varPhi \ \varPsi \ \varphi , \text { if } \varPhi \text { is included in } \varPsi \text { and }\varPhi \vdash \varphi ,\text { then }\varPsi \vdash \varphi \);
-
DedAssum: \(\text {for any }\varPhi \ \varphi , \text { if } \varphi \text { belongs to } \varPhi , \text { then }\varPhi \vdash \varphi \);
-
DedSubst: \(\text {for any }\varPhi \ \varPsi \ \psi , \text { if }(\text {for any } \varphi , \text { if } \varphi \text { belongs to } \varPsi , \text { then } \varPhi \vdash \varphi )\text { and }\varPhi \cup \varPsi \vdash \psi ,\text { then }\varPhi \vdash \psi \).
1.4 A.4 Demo4: Separation Logic, Without Separation Conjunction
Primitive connectives: \(\wedge , \vee , \bot , \top , *, \textbf{emp}\).
Syntactic sugar for connectives: \(\bigwedge _{i=1}^n\varphi _i\triangleq \varphi _1\wedge \ldots \wedge \varphi _n\), \(*_{i=1}^n\varphi _i\triangleq \varphi _1*\ldots *\varphi _n\).
Primitive judgements: derivable1 \(\varphi \vdash \psi \).
Primary rules:
-
FalsepSepconLeft: \(\text {for any }\varphi ,\ \bot *\varphi \vdash \bot \);
-
OrpSepconLeft: \(\text {for any }\varphi \ \psi \ \chi ,\ (\varphi \vee \psi )*\chi \vdash (\varphi *\chi )\vee (\psi *\chi )\);
-
SepconEmpLeft: \(\text {for any }\varphi ,\ \varphi *\textbf{emp}\vdash \varphi \);
-
SepconEmpRight: \(\text {for any }\varphi ,\ \varphi \vdash \varphi *\textbf{emp}\);
-
Der1SepconComm: \(\text {for any }\varphi \ \psi ,\ \varphi *\psi \vdash \psi *\varphi \);
-
Der1SepconAssoc1: \(\text {for any }\varphi \ \psi \ \chi ,\ \varphi *(\psi *\chi )\vdash (\varphi *\psi )*\chi \);
-
Der1SepconMono: \(\text {for any }\varphi _1\ \varphi _2\ \psi _1\ \psi _2,\ \text {if }\varphi _1\vdash \varphi _2\text { and }\psi _1\vdash \psi _2,\text { then }(\varphi _1*\psi _1)\vdash (\varphi _2*\psi _2)\);
-
Der1TruepIntros: \(\text {for any }\varphi ,\ \varphi \vdash \top \);
-
Der1FalsepElim: \(\text {for any }\varphi , \bot \vdash \varphi \);
-
Der1OrpIntros1: \(\text {for any }\varphi \ \psi ,\ \varphi \vdash \varphi \vee \psi \);
-
Der1OrpIntros2: \(\text {for any }\varphi \ \psi ,\ \psi \vdash \varphi \vee \psi \);
-
Der1OrpElim: \(\text {for any }\varphi \ \psi \ \chi ,\text { if }\varphi \vdash \chi \text { and }\psi \vdash \chi ,\text { then }\varphi \vee \psi \vdash \chi \);
-
Der1AndpIntros: \(\text {for any }\varphi \ \psi \ \chi ,\text { if }\varphi \vdash \psi \text { and }\varphi \vdash \chi ,\text { then }\varphi \vdash \psi \wedge \chi \);
-
Der1AndpElim1: \(\text {for any }\varphi \ \psi ,\ \varphi \wedge \psi \vdash \varphi \);
-
Der1AndpElim2: \(\text {for any }\varphi \ \psi ,\ \varphi \wedge \psi \vdash \psi \).
1.5 A.5 Demo5: Separation Logic, with Separating Conjunction
Primary connectives: \(\rightarrow ,\wedge ,\vee ,\bot ,*,\mathrel {-*},\textbf{emp}\).
Syntactic sugar for connectives: \(\varphi \leftrightarrow \psi \triangleq (\varphi \rightarrow \psi )\wedge (\psi \rightarrow \varphi )\), \(\lnot \varphi \triangleq \varphi \rightarrow \bot \), \(\top \triangleq \bot \rightarrow \bot \), \(\bigwedge _{i=1}^n\varphi _i\triangleq \varphi _1\wedge \ldots \wedge \varphi _n\), \(*_{i=1}^n\varphi _i\triangleq \varphi _1*\ldots *\varphi _n\).
Primitive judgements: provable (\(\vdash \varphi \)).
Syntactic sugar for judgements: \(\text {for any }\varPhi \ \varphi ,\ \varPhi \vdash \varphi \ \text {iff. }\text {exists} \ \varphi _1, \varphi _2, \dots , \varphi _n \in \varPhi , \ \text {s.t.} \ \vdash \varphi _1 \rightarrow \varphi _2 \rightarrow \dots \rightarrow \varphi _n \rightarrow \varphi \).
Primary rules:
-
SepconEmp: \(\text {for any }\varphi ,\ \vdash (\varphi *\textbf{emp})\leftrightarrow \varphi \);
-
SepconComm: \(\text {for any } \varphi \ \psi ,\ \vdash (\varphi *\psi )\leftrightarrow (\psi *\varphi )\);
-
SepconAssoc: \(\text {for any }\varphi \ \psi \ \chi , \ \vdash ((\varphi *\psi )*\chi )\leftrightarrow (\varphi *(\psi *\chi ))\);
-
WandSepconAdjoint: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash ((\varphi *\psi )\rightarrow \chi )\leftrightarrow (\varphi \rightarrow (\psi \mathrel {-*}\chi ))\);
-
PeirceLaw: \(\text {for any }\varphi \ \psi ,\ \vdash ((\varphi \rightarrow \psi )\rightarrow \psi )\rightarrow \psi \);
-
FalsepElim: \(\text {for any }\varphi ,\ \vdash \bot \rightarrow \varphi \);
-
OrpIntros1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\varphi \vee \psi )\);
-
OrpIntros2: \(\text {for any }\varphi \ \psi ,\ \vdash \psi \rightarrow (\varphi \vee \psi )\);
-
OprElim: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \chi )\rightarrow (\psi \rightarrow \chi )\rightarrow ((\varphi \vee \psi )\rightarrow \chi )\);
-
AndpIntros: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow \psi \rightarrow (\varphi \wedge \psi )\);
-
AndpElim1: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \varphi \);
-
AndpElim2: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \psi \);
-
ModusPones: \(\text {for any }\varphi \ \psi ,\ \text {if }\vdash \varphi \rightarrow \psi \text { and }\vdash \varphi ,\text { then }\vdash \psi \);
-
Axiom1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\psi \rightarrow \varphi )\);
-
Axiom2: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \chi )\).
1.6 A.6 Demo6: Separation Logic, Without Separating Implication
Primitive connectives: \(\rightarrow , \wedge , *,\textbf{emp}\).
Syntactic sugar for connectives: \(\varphi \leftrightarrow \psi \triangleq (\varphi \rightarrow \psi )\wedge (\psi \rightarrow \varphi )\).
Primitive judgement: provable (\(\vdash \varphi \)).
Syntactic sugar for judgements: \(\text {for any }\varPhi \ \varphi ,\ \varPhi \vdash \varphi \ \text {iff. }\text {exists} \ \varphi _1, \varphi _2, \dots , \varphi _n \in \varPhi , \ \text {s.t.} \ \vdash \varphi _1 \rightarrow \varphi _2 \rightarrow \dots \rightarrow \varphi _n \rightarrow \varphi \);
\(\text {for any }\psi \ \varphi , \ \psi \dashv \vdash \varphi \text { iff. }\vdash \psi \rightarrow \varphi \text { and }\vdash \varphi \rightarrow \psi \).
Primary rules:
-
SepconEmp: \(\text {for any }\varphi ,\ \vdash (\varphi *\textbf{emp})\leftrightarrow \varphi \);
-
SepconComm: \(\text {for any } \varphi \ \psi ,\ \vdash (\varphi *\psi )\leftrightarrow (\psi *\varphi )\);
-
SepconAssoc: \(\text {for any }\varphi \ \psi \ \chi , \ \vdash ((\varphi *\psi )*\chi )\leftrightarrow (\varphi *(\psi *\chi ))\);
-
SepconMono: \(\text {for any }\varphi _1\ \varphi _2\ \psi _1\ \psi _2,\text { if }\vdash \varphi _1\rightarrow \varphi _2\text { and }\vdash \psi _1\rightarrow \psi _2,\text { then }\vdash (\varphi _1*\psi _1)\rightarrow (\varphi _2*\psi _2)\);
-
AndpIntros: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow \psi \rightarrow (\varphi \wedge \psi )\);
-
AndpElim1: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \varphi \);
-
AndpElim2: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \psi \);
-
ModusPones: \(\text {for any }\varphi \ \psi ,\ \text {if }\vdash \varphi \rightarrow \psi \text { and }\vdash \varphi ,\text { then }\vdash \psi \);
-
Axiom1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\psi \rightarrow \varphi )\);
-
Axiom2: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \chi )\).
1.7 A.7 Demo7: Separation Logic, Constructed from Model Level
Primitive connectives: \(\oplus , \textbf{unit}\).
Syntactic sugar for connectives: define \(\rightarrow , \wedge , \vee \) directly from model level, using Coq’s meta-logic; \((\varphi * \psi )\ m\triangleq \text { exists }m_1\ m_2,\ \oplus (m_1,m_2,m)\text { and }\varphi \ m\text { and }\psi \ m\); \(\textbf{emp}\ m\triangleq \textbf{unit}\ m\).
Syntactic sugar for judgements: define provable (\(\vdash \varphi \)) and derivable1 (\(\varphi \vdash \psi \)) with Coq’s meta-logic.
Primary rules:
-
JoinComm: \(\text {for any }m_1\ m_2\ m,\ \text {if }\oplus (m_1,m_2,m),\text { then }\oplus (m_2,m_1,m)\);
-
JoinAssoc: \(\text {for any }m_1\ m_2\ m_3\ m_{12}\ m_{123},\text { if }\oplus (m_1,m_2,m_{12})\text { and }\oplus (m_{12},m_3,\) \(m_{123}),\text { then }(\text {there exists }m_{23},\ \oplus (m_2,m_3,m_{23})\text { and }\oplus (m_1,m_{23},m_{123}))\).
1.8 A.8 Mendelson’s Propositional Logic
Primitive connectives: \(\rightarrow , \lnot , \top \).
Syntactic sugar for connectives: \(\varphi \vee \psi \triangleq \lnot \varphi \rightarrow \psi \), \(\bot \triangleq \lnot \top \).
Primitive judgements: provable (\(\vdash \varphi \)).
Syntactic sugar for judgements: \(\text {for any }\varPhi \ \varphi ,\ \varPhi \vdash \varphi \ \text {iff. }\text {exists} \ \varphi _1, \varphi _2, \dots , \varphi _n \in \varPhi , \ \text {s.t.} \ \vdash \varphi _1 \rightarrow \varphi _2 \rightarrow \dots \rightarrow \varphi _n \rightarrow \varphi \).
Primary rules:
-
ByContradiction: \(\text {for any }\varphi \ \psi ,\ \vdash (\lnot \varphi \rightarrow \psi )\rightarrow (\lnot \varphi \rightarrow \lnot \psi )\rightarrow \varphi \).
-
ModusPones: \(\text {for any }\varphi \ \psi ,\ \text {if }\vdash \varphi \rightarrow \psi \text { and }\vdash \varphi ,\text { then }\vdash \psi \);
-
Axiom1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\psi \rightarrow \varphi )\);
-
Axiom2: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \chi )\).
We have proved in Coq the completeness of this logic.
1.9 A.9 Minimum Separation Logic
Primitive connectives: \(\rightarrow , \wedge , *\).
Primitive judgements: provable (\(\vdash \varphi \)).
Syntactic sugar for judgements: \(\text {for any }\varPhi \ \varphi ,\ \varPhi \vdash \varphi \ \text {iff. }\text {exists} \ \varphi _1, \varphi _2, \dots , \varphi _n \in \varPhi , \ \text {s.t.} \ \vdash \varphi _1 \rightarrow \varphi _2 \rightarrow \dots \rightarrow \varphi _n \rightarrow \varphi \).
Primary rules:
-
SepconCommImpp: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi *\psi )\rightarrow (\psi *\varphi )\);
-
SepconAssoc1: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi *(\psi *\chi ))\rightarrow ((\varphi *\psi )*\chi )\);
-
SepconMono: \(\text {for any }\varphi _1\ \varphi _2\ \psi _1\ \psi _2,\text { if }\vdash \varphi _1\rightarrow \varphi _2\text { and }\vdash \psi _1\rightarrow \psi _2,\text { then }\vdash (\varphi _1*\psi _1)\rightarrow (\varphi _2*\psi _2)\);
-
AndpIntros: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow \psi \rightarrow (\varphi \wedge \psi )\);
-
AndpElim1: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \varphi \);
-
AndpElim2: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \psi \);
-
ModusPones: \(\text {for any }\varphi \ \psi ,\ \text {if }\vdash \varphi \rightarrow \psi \text { and }\vdash \varphi ,\text { then }\vdash \psi \);
-
Axiom1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\psi \rightarrow \varphi )\);
-
Axiom2: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \chi )\).
We have proved in Coq the completeness of this logic.
1.10 A.10 Demo for Bedrock2’s Separation Logic
Primitive connectives: \(\rightarrow , \wedge , *, \textbf{emp}\).
Syntactic sugar for connectives: \(\varphi \leftrightarrow \psi \triangleq (\varphi \rightarrow \psi )\leftrightarrow (\psi \rightarrow \varphi )\).
Primitive judgements: provable (\(\vdash \varphi \)).
Syntactic sugar for judgements: \(\text {for any }\psi \ \varphi , \ \psi \vdash \varphi \text { iff. }\vdash \psi \rightarrow \varphi \);
\(\text {for any }\psi \ \varphi , \ \psi \dashv \vdash \varphi \text { iff. }\vdash \psi \rightarrow \varphi \text { and }\vdash \varphi \rightarrow \psi \).
Primary rules:
-
SepconEmp: \(\text {for any }\varphi ,\ \vdash (\varphi *\textbf{emp})\leftrightarrow \varphi \);
-
SepconComm: \(\text {for any } \varphi \ \psi ,\ \vdash (\varphi *\psi )\leftrightarrow (\psi *\varphi )\);
-
SepconAssoc: \(\text {for any }\varphi \ \psi \ \chi , \ \vdash ((\varphi *\psi )*\chi )\leftrightarrow (\varphi *(\psi *\chi ))\);
-
SepconMono: \(\text {for any }\varphi _1\ \varphi _2\ \psi _1\ \psi _2,\text { if }\vdash \varphi _1\rightarrow \varphi _2\text { and }\vdash \psi _1\rightarrow \psi _2,\text { then }\vdash (\varphi _1*\psi _1)\rightarrow (\varphi _2*\psi _2)\);
-
AndpIntros: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow \psi \rightarrow (\varphi \wedge \psi )\);
-
AndpElim1: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \varphi \);
-
AndpElim2: \(\text {for any }\varphi \ \psi ,\ \vdash (\varphi \wedge \psi )\rightarrow \psi \);
-
ModusPones: \(\text {for any }\varphi \ \psi ,\ \text {if }\vdash \varphi \rightarrow \psi \text { and }\vdash \varphi ,\text { then }\vdash \psi \);
-
Axiom1: \(\text {for any }\varphi \ \psi ,\ \vdash \varphi \rightarrow (\psi \rightarrow \varphi )\);
-
Axiom2: \(\text {for any }\varphi \ \psi \ \chi ,\ \vdash (\varphi \rightarrow \psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \psi )\rightarrow (\varphi \rightarrow \chi )\).
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Tao, Y., Cao, Q. (2022). LOGIC: A Coq Library for Logics. In: Dong, W., Talpin, JP. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2022. Lecture Notes in Computer Science, vol 13649. Springer, Cham. https://doi.org/10.1007/978-3-031-21213-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-031-21213-0_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-21212-3
Online ISBN: 978-3-031-21213-0
eBook Packages: Computer ScienceComputer Science (R0)