🧾 Add support for proofs (#609)

* Add support for the basic proof envs. However cross references to theorems are not working
* Add myst-to-tex to dev deps of jats-to-myst
* Add ruleid

---------

Co-authored-by: Rowan Cockett <rowanc1@gmail.com>
Co-authored-by: Franklin Koch <franklin@curvenote.com>

.changeset/quiet-taxis-grab.md

@@ -0,0 +1,8 @@
+---
+'myst-transforms': patch
+'myst-ext-proof': patch
+'jats-to-myst': patch
+'myst-to-tex': patch
+---
+
+Add support for proofs in LaTeX

packages/jats-to-myst/package.json

@@ -49,5 +49,8 @@
     "unist-util-remove": "^3.1.0",
     "vfile": "^5.0.0",
     "vfile-reporter": "^7.0.4"
+  },
+  "devDependencies": {
+    "myst-to-tex": "^1.0.7"
   }
 }

packages/myst-ext-proof/package.json

@@ -32,6 +32,7 @@
     "url": "https://github.com/executablebooks/mystmd/issues"
   },
   "dependencies": {
+    "myst-spec": "^0.0.4",
     "myst-common": "^1.1.7"
   },
   "devDependencies": {

packages/myst-ext-proof/src/index.ts

@@ -1,2 +1,2 @@
 export { proofDirective } from './proof.js';
-export { ProofKind } from './types.js';
+export type { ProofKind, ProofContainer } from './types.js';

packages/myst-ext-proof/src/types.ts

@@ -1,17 +1,26 @@
-export enum ProofKind {
-  proof = 'proof',
-  axiom = 'axiom',
-  lemma = 'lemma',
-  definition = 'definition',
-  criterion = 'criterion',
-  remark = 'remark',
-  conjecture = 'conjecture',
-  corollary = 'corollary',
-  algorithm = 'algorithm',
-  example = 'example',
-  property = 'property',
-  observation = 'observation',
-  proposition = 'proposition',
-  assumption = 'assumption',
-  theorem = 'theorem',
-}
+import type { Container } from 'myst-spec';
+
+const PROOF_KINDS = [
+  'proof',
+  'axiom',
+  'lemma',
+  'definition',
+  'criterion',
+  'remark',
+  'conjecture',
+  'corollary',
+  'algorithm',
+  'example',
+  'property',
+  'observation',
+  'proposition',
+  'assumption',
+  'theorem',
+] as const;
+type ProofKinds = typeof PROOF_KINDS;
+
+export type ProofKind = ProofKinds[number];
+
+export type ProofContainer = Omit<Container, 'kind'> & {
+  kind: ProofKind;
+};

packages/myst-to-tex/package.json

@@ -40,6 +40,7 @@
     "myst-common": "^1.1.8",
     "myst-frontmatter": "^1.1.8",
     "myst-spec-ext": "^1.1.8",
+    "myst-ext-proof": "^1.0.3",
     "unist-util-remove": "^3.1.0",
     "unist-util-select": "^4.0.3",
     "vfile-reporter": "^7.0.4"

packages/myst-to-tex/src/index.ts

@@ -17,6 +17,7 @@ import MATH_HANDLERS, { withRecursiveCommands } from './math.js';
 import { selectAll } from 'unist-util-select';
 import type { FootnoteDefinition } from 'myst-spec-ext';
 import { transformLegends } from './legends.js';
+import { TexProofSerializer, proofHandler } from './proof.js';
 
 export type { LatexResult } from './types.js';
 
@@ -332,6 +333,7 @@ const handlers: Record<string, Handler> = {
     state.closeBlock(node);
   },
   container: containerHandler,
+  proof: proofHandler,
   caption: captionHandler,
   captionNumber: () => undefined,
   crossReference(node, state, parent) {
@@ -598,14 +600,20 @@ const plugin: Plugin<[Options?], Root, VFile> = function (opts) {
     transformLegends(node);
 
     const state = new TexSerializer(file, node, opts ?? { handlers });
-    let tex = (file.result as string).trim();
-
     const glossaryState = new TexGlossaryAndAcronymSerializer(state.glossary, state.abbreviations);
+
+    const preamble: string[] = [];
+    if (state.data.hasProofs) {
+      preamble.push(new TexProofSerializer().preamble);
+    }
+    preamble.push(opts?.printGlossaries ? glossaryState.preamble : '');
+
+    let tex = (file.result as string).trim();
     tex += opts?.printGlossaries ? '\n' + glossaryState.printedDefinitions : '';
 
     const result: LatexResult = {
       imports: [...state.data.imports],
-      preamble: opts?.printGlossaries ? glossaryState.preamble : '',
+      preamble: preamble.join('\n\n'),
       commands: withRecursiveCommands(state),
       value: tex,
     };

packages/myst-to-tex/src/proof.ts

@@ -0,0 +1,108 @@
+import { fileError, writeTexLabelledComment, RuleId } from 'myst-common';
+import type { GenericNode } from 'myst-common';
+import type { Text } from 'myst-spec';
+import type { ProofContainer, ProofKind } from 'myst-ext-proof';
+import { select } from 'unist-util-select';
+import { remove } from 'unist-util-remove';
+import type { Handler } from './types.js';
+
+function kindToEnvironment(kind: ProofKind): string {
+  switch (kind) {
+    case 'theorem':
+      return 'theorem';
+    case 'proof':
+      return 'proof';
+    case 'proposition':
+      return 'proposition';
+    case 'definition':
+      return 'definition';
+    case 'example':
+      return 'example';
+    case 'remark':
+      return 'remark';
+    case 'axiom':
+      return 'axiom';
+    case 'conjecture':
+      return 'conjecture';
+    case 'lemma':
+      return 'lemma';
+    case 'observation':
+      return 'observation';
+    default:
+      return '';
+  }
+}
+
+export const proofHandler: Handler = (node, state) => {
+  state.usePackages('amsthm');
+
+  const p = node as ProofContainer;
+  const env = kindToEnvironment(p.kind);
+  if (!env) {
+    fileError(state.file, `Unhandled LaTeX proof environment "${p.kind}"`, {
+      node,
+      source: 'myst-to-tex',
+      ruleId: RuleId.texRenders,
+    });
+    return;
+  }
+
+  const t = select('admonitionTitle > text', node);
+  if (t) {
+    // Do not render the title twice
+    t.type = '__delete__';
+  }
+  const newNode = remove(node, '__delete__') as GenericNode;
+
+  state.write('\\begin{');
+  state.write(env);
+  state.write('}');
+  if (t) {
+    state.write('[');
+    state.write((t as Text).value);
+    state.write(']');
+  }
+  if (newNode.identifier && newNode.identifier.length > 0) {
+    state.write('\\label{');
+    state.write(newNode.identifier);
+    state.write('}');
+  }
+  state.renderChildren(newNode, true);
+  state.write('\\end{');
+  state.write(env);
+  state.write('}');
+
+  state.data.hasProofs = true;
+};
+
+export class TexProofSerializer {
+  static COMMENT_LENGTH = 50;
+
+  preamble: string;
+
+  constructor() {
+    this.preamble = this.renderThmDefinitions();
+  }
+
+  private renderThmDefinitions(): string {
+    const definitions = [
+      '\\newtheorem{theorem}{Theorem}[section]',
+      '\\newtheorem{corollary}{Corollary}[theorem]',
+      '\\newtheorem{lemma}[theorem]{Lemma}',
+      '\\newtheorem{proposition}{Proposition}[section]',
+      '\\newtheorem{definition}{Definition}[section]',
+      '\\newtheorem{example}{Example}[section]',
+      '\\newtheorem{remark}{Remark}[section]',
+      '\\newtheorem{axiom}{Axiom}[section]',
+      '\\newtheorem{conjecture}{Conjecture}[section]',
+      '\\newtheorem{observation}{Observation}[section]',
+    ];
+    const block = writeTexLabelledComment(
+      'theorem',
+      definitions,
+      TexProofSerializer.COMMENT_LENGTH,
+    );
+    const percents = ''.padEnd(TexProofSerializer.COMMENT_LENGTH, '%');
+    return `${percents}\n${block}${percents}`;
+  }
+}

packages/myst-to-tex/src/types.ts

@@ -33,6 +33,7 @@ export type StateData = {
   nextCaptionNumbered?: boolean;
   nextHeadingIsFrameTitle?: boolean;
   nextCaptionId?: string;
+  hasProofs?: boolean;
   mathPlugins: Required<PageFrontmatter>['math'];
   imports: Set<string>;
 };