LOGIC: A Coq Library for Logics

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.

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