31:T83b,// this is just the initial value of the proof creator editor sqrtTwoIrratSrcEscaped = `--Let's import some magic import data.nat.prime import tactic.norm_num import tactic.ring --**Theorem:** For any coprime \$a,b\\in\\mathbb{N}\$, we have \$a^2 \\neq 2 * b^2\$. theorem sqrt_two_irrational {a b : ℕ} (co : nat.coprime a b) : a^2 ≠ 2*b^2 := begin --*Proof.* Assume that \$a^2 = 2 * b^2\$. assume hyp : a^2 = 2 * b^2, --Then 2 must divide \$a^2\$. have : 2 ∣ a^2, by simp [hyp], --So 2 must also divide \$a\$. have : 2 ∣ a, by { -- We know that 2 is prime. have : nat.prime 2, by norm_num, -- We know that, for any prime \$p\$ and \$a,n\\in\\mathbb{N}\$, if \$p \\mid a^n\$ then \$p \\mid a\$. have prime_divide_theorem := nat.prime.dvd_of_dvd_pow, --Putting it together, we have \$2 \\mid a\$. exact (prime_divide_theorem this ‹2 ∣ a^2›) }, --Hence, there is \$c\$ such that \$a = 2 * c\$. obtain ⟨c, aeq⟩ : ∃ c, a = 2 * c, from this, --Hence, \$2 * (2 * c^2) = 2 * b^2\$ since \$2 * (2 * c^2) = (2 * c)^2 = a^2 = 2 * b^2\$. have : 2 * (2 * c^2) = 2 * b^2, by { rw [hyp.symm, aeq], ring }, --Thus, \$2 * c^2 = b^2\$, have : 2 * c^2 = b^2, from nat.eq_of_mul_eq_mul_left (by norm_num) this, --and hence, \$2 \\mid b^2\$. have : 2 ∣ b^2, by simp[eq.symm this], --Since 2 is prime, we have \$2 \\mid b\$. have : 2 ∣ b,from nat.prime.dvd_of_dvd_pow nat.prime_two this, --Now, since \$2 \\mid a\$ and \$2 \\mid b\$, we have \$2 \\mid \\mathrm{gcd}(a, b)\$. have two_dvd_gcd : 2 ∣ nat.gcd a b, from nat.dvd_gcd ‹2 ∣ a› ‹2 ∣ b›, --But \$\\mathrm{gcd}(a, b) = 1\$ by assumption, and hence \$2 \\mid 1\$. have : 2 ∣ 1, by { -- We have \$a,b\$ are coprime if and only if \$\\mathrm{gcd}(a,b)=1\$ by definition. have : nat.gcd a b = 1, from co, -- Substituting \$\\mathrm{gcd}(a,b)\$ with 1, we have \$2\\mid 1\$. rwa this at two_dvd_gcd }, --However, 2 does not divide 1, a contradiction! \$\\square\$ show false, from absurd ‹2 ∣ 1› (by norm_num) end`32:T6bb,md`\`\`\`javascript proofView({proof, invalidation, unfoldLeanEntries, startIndex, endIndex, editorOpts}) \`\`\` where 1. \`proof\` is a proof object, an array consisting of objects with fields: 1. \`mathsEntry\`: object that will be displayed using Observable's \`html\` tag function. You can hence use pure HTML, ${tex`\LaTeX`}, markdown, etc. to write your proofs. 2. \`leanEntry\`: the Lean code that corresponds to the given \`mathsEntry\`. 3. \`unfoldLeanEntry\` (optional, default \`false\`): set to \`true\` if you want to unfold the Lean entry by default. 4. \`unfoldSubproof\` (optional, default \`false\`): set to \`true\` if you want to unfold the proof's subproof by default. 5. \`unfoldSubproofLeanEntries\` (optional, default \`false\`): set to \`true\` if you want to unfold the subproof's lean entries by default. If a subproof entry sets \`unfoldLeanEntry\`, then that value will be used instead. 2. \`invalidation\` is the invalidation promise of the cell, 3. \`unfoldLeanEntries\` (optional, default true): set to \`false\` if you want to fold the Lean entries by default. As for \`unfoldSubproofLeanEntries\`, this option can be overriden by a proof entry's \`unfoldLeanEntry\` option, 4. \`startIndex\` (optional, default 0): the index of the first proof entry to show (useful, for example, to skip imports at the beginning of the proof). 5. \`endIndex\` (optional, default \`proof.length\`): the index of the last proof entry (non-inclusive) to show (useful, for example, to split proofs into multiple proof views). 6. \`editorOpts\` (optional) contains options passed to the Lean editor (see [here](https://observablehq.com/@bryangingechen/hello-lean-prover#CMLeanEditorUsage)).`33:T7a8,proofView = ({ proof, invalidation, editorOpts = {}, unfoldLeanEntries = true, startIndex = 0, endIndex }) => { if (!(invalidation instanceof Promise)) throw Error("Need to pass an invalidation parameter"); addCSS(proofViewStyle); const infoView = new InfoView({}, invalidation); const docArray = createDocArray(proof); const editors = leanEditorFrom({ className: CSS_CLASSES.NO_EDITOR_BUTTONS, docArray, fileName: DOM.uid('lean').id.replace(/-/g, '_') + '.lean', height: '100%', readOnly: true, header: html``, infoView, ...editorOpts }); if (startIndex < 0 || (proof.length && startIndex >= proof.length)) { throw Error( `startIndex out of range. Must be between 0 and ${proof.length - 1}` ); } endIndex = endIndex || (proof.length ? proof.length : 1); if (endIndex <= startIndex || endIndex > proof.length) { throw Error( `endIndex out of range. Must be between ${startIndex + 1} and ${ proof.length }` ); } const slicedProof = proof.slice(startIndex, endIndex); startIndex = compInitEditorIndex({ proof, index: startIndex }); endIndex = compInitEditorIndex({ proof, index: endIndex }); const div = html`

${ proofEntriesView({ editors, invalidation, proof: slicedProof, unfoldLeanEntries, editorIndex: startIndex, endIndex }).nodes }

${infoView.node}

`; const unstick = makeSticky(div, infoView.node, { offset: 50 }); // offset to 50px to avoid observable header to hide the info view invalidation.then(unstick); div.value = { docArray, startIndex, endIndex, infoView, proof, slicedProof }; return div; }34:Tde0,// creates the proof entries by recursively iterating through the passed proof object. function proofEntriesView({ editors, editorIndex = 0, endIndex = Number.MAX_SAFE_INTEGER, invalidation, proof = [], unfoldLeanEntries = false }) { let nodes = []; // collect the HTML nodes in an accumulator proof.forEach( ( { mathsEntry, proof: subproof = [], unfoldLeanEntry, unfoldSubproof = false, unfoldSubproofLeanEntries = false }, index ) => { if (editorIndex === endIndex) // we reached the end -> nothing to do return; // create the subproof const { nodes: subNodes, editorIndex: nextEditorIndex } = proofEntriesView({ editors, editorIndex: editorIndex + 1, invalidation, proof: subproof, unfoldLeanEntries: unfoldSubproofLeanEntries }); const hasSubproof = subNodes.length; const unfoldSubproofDiv = hasSubproof ? unfoldSubproofView({ unfold: !unfoldSubproof }) : html``; const subproofDiv = hasSubproof ? subproofView({ subNodes, hidden: !unfoldSubproof }) : html``; if (hasSubproof) { unfoldSubproofDiv.addEventListener('click', () => { // toggle subproof visibility subproofDiv.classList.toggle(CSS_CLASSES.HIDDEN); // update the unfoldDiv; not nice, but since I cannot really use React, that's what we get unfoldSubproofDiv.innerHTML = unfoldSubproofView({ unfold: subproofDiv.classList.contains(CSS_CLASSES.HIDDEN) }).innerHTML; }); } // add the new node to the nodes accumulator nodes = [ ...nodes, html`

${proofEntryView({ editor: editors(editorIndex, invalidation), mathsEntry, unfoldLeanEntry: unfoldLeanEntry !== undefined ? unfoldLeanEntry : unfoldLeanEntries, showUnfoldLeanEntriesButton: index === 0 // show unfold lean button for the first element })}

${unfoldSubproofDiv} ${subproofDiv}

` ]; editorIndex = nextEditorIndex; // book keeping: we need to update to the right index for the passed editors object. } ); if (nodes.length) { // add listener for unfold lean entries button at the first proof entry const unfoldLeanEntriesButton = nodes[0].querySelector( `.${CSS_CLASSES.PROOF_ENTRIES_UNFOLD_LEAN_ENTRIES_BUTTON}` ); unfoldLeanEntriesButton.addEventListener('click', () => { // just take the first element to decide whether to fold or unfold the entries const unfold = nodes[0] .querySelector(`.${CSS_CLASSES.PROOF_ENTRY_LEAN}`) .classList.contains(CSS_CLASSES.HIDDEN); nodes.forEach(node => { const leanProofEntry = node.querySelector( `.${CSS_CLASSES.PROOF_ENTRY_LEAN}` ); if (unfold) { leanProofEntry.classList.remove(CSS_CLASSES.HIDDEN); } else { leanProofEntry.classList.add(CSS_CLASSES.HIDDEN); } }); // not nice, but since I cannot really use React, that's what we get unfoldLeanEntriesButton.innerHTML = unfoldLeanEntriesButtonView({ unfold: !unfold }).innerHTML; }); } return { nodes, editorIndex }; }35:Tc2f,proofEntryView = ({ editor, mathsEntry, unfoldLeanEntry = false, showUnfoldLeanEntriesButton = false }) => { const mathsEntryWrapper = mathsEntryWrapperView({ mathsEntry, unfoldLeanEntriesButton: { show: showUnfoldLeanEntriesButton, unfold: !unfoldLeanEntry } }); const leanEntryDiv = leanEntryView({editor, hidden: !unfoldLeanEntry}); // helper functions // upates the info view with the output of the cell const updateInfoView = () => { const doc = editor.value.editor.getDoc(); // set cursor to the end of the cell doc.setCursor(doc.lineCount(), 0); // update info view with information from cursor position editor.value.updateInfoView(); }; const activate = () => { // deactivate old selected maths entry const activeEntry = getActiveProofEntry(getProofParent(mathsEntryWrapper)); if (activeEntry) activeEntry.classList.remove(CSS_CLASSES.ACTIVE); // select the current entry mathsEntryWrapper.closest(`.${CSS_CLASSES.PROOF_ENTRY}`).classList.add(CSS_CLASSES.ACTIVE); }; // activate the entry when the pin button is pressed mathsEntryWrapper.querySelector(`.${CSS_CLASSES.PROOF_ENTRY_PIN_BUTTON}`).addEventListener('click', () => { activate(); updateInfoView({}); }); // listeners for maths entry const mathsEntryDiv = mathsEntryWrapper.querySelector(`.${CSS_CLASSES.PROOF_ENTRY_MATHS}`); mathsEntryDiv.addEventListener('click', () => { // toggle lean div visibility leanEntryDiv.classList.toggle(CSS_CLASSES.HIDDEN); // update unfold button; not nice, but since I cannot really use React, that's what we get const unfoldButton = mathsEntryWrapper.querySelector(`.${CSS_CLASSES.PROOF_ENTRIES_UNFOLD_LEAN_ENTRIES_BUTTON}`); if (unfoldButton) { const unfold = leanEntryDiv.classList.contains(CSS_CLASSES.HIDDEN); unfoldButton.innerHTML = unfoldLeanEntriesButtonView({unfold}).innerHTML; } // activate the clicked entry activate(); updateInfoView({}); }); mathsEntryDiv.addEventListener('mouseover', () => { const activeEntry = getActiveProofEntry(getProofParent(mathsEntryWrapper)); // only update info view if we are not hovering above the active entry if (!activeEntry || activeEntry !== getProofEntryParent(mathsEntryWrapper)) { updateInfoView({}); } }); // when leaving the entry, make sure the activated proof entry is shown in the info view again mathsEntryDiv.addEventListener('mouseleave', () => { const activeEntry = getActiveProofEntry(getProofParent(mathsEntryWrapper)); // only update to active entry if we are not hovering above it if (activeEntry && activeEntry !== getProofEntryParent(mathsEntryWrapper)) { activeEntry.querySelector(`.${CSS_CLASSES.LEAN_EDITOR_WRAPPER}`).value.updateInfoView(); } }); // listeners for lean entry leanEntryDiv.querySelector(`.${CSS_CLASSES.CODE_MIRROR_CONTAINER}`).addEventListener('click', () => { activate(); // info view will be updated by editor, so no need to call updateInfoview }); return [mathsEntryWrapper, leanEntryDiv]; }36:Tb34,/* This is badly designed but does the basic job.It parses the proof top down. Here are the different states: 1. Line starting with "/-": swich into maths mode and append each line to mathsEntry until "-/" is seen at the end of a line 2. Line starting with "--": append a single line to mathsEntry 3. Line ending with "{": recursively parse the subproof enclosed between this bracket and the first line ending with "}" 4. Otherwise, append the current line to leanEntry Each time the parser encounters the start of a maths comment, i.e. "/--?" or "--", it adds the so-far created proofEntry to the proof result and reset the proofEntry. */ function createProofObject({proofText, index = 0, mathsEntryNewline = '\n'}) { const proof = []; let proofEntry = {}; let state = STATE.LEAN; const addProofEntry = () => { proof.push(proofEntry); proofEntry = {}; // reset proof Entry }; const parseMathsLine = (line) => { const {mathsEntry} = proofEntry; proofEntry.mathsEntry = mathsEntry ? `${mathsEntry}${mathsEntryNewline}${line}` : line; }; const parseMathsBlock = (line) => { const match = BLOCK_COMMENT_END_REGEX.exec(line); if (match) { line = match[1].trim(); // cut off block comment end state = STATE.LEAN; } parseMathsLine(line); }; const parseLeanLine = (line) => { const {leanEntry} = proofEntry; proofEntry.leanEntry = leanEntry ? `${leanEntry}\n${line}` : line; }; const finish = () => { addProofEntry(); return { proof: proof.slice(1), // first element is rubbish index } }; for(; index < proofText.length; ++index) { let line = proofText[index].trim(); if (state === STATE.MATHS) { parseMathsBlock(line); continue; } let match = BLOCK_COMMENT_START_REGEX.exec(line); if (match) { addProofEntry(); state = STATE.MATHS; line = match[1].trim(); // cut off block comment start parseMathsBlock(line); continue; } match = LINE_COMMENT_REGEX.exec(line); if (match) { addProofEntry(); line = match[1].trim(); // cut off line comment start parseMathsLine(line); continue; } // we are parsing a lean line parseLeanLine(line); match = SUBPROOF_START_REGEX.exec(line); if (match) { const {proof: subProof, index: newIndex} = createProofObject({proofText, index: index + 1, mathsEntryNewline}); index = newIndex; proofEntry.proof = subProof; continue; } match = SUBPROOF_END_REGEX.exec(line); // to allow "by { ... }" statements, we count the number of '{' and '}' in the line; // they numbers should match if the line is not finishing a subproof if (match && (line.split("{").length !== line.split("}").length)) { return finish(); // first element is rubbish } } return finish(); }37:T7a4,proofCreatorFooter = ({ mathsEntryTag = "mdtex", mathsEntryNewline = "\n" }) => (leanEditorObj) => { const outputArea = html`

`;
  const createButton = html`<input type="button" value="Create proof object" style="flex: 1"/>`;
  const updateProof = () => {
    const { proof } = createProofObject({
      proofText: leanEditorObj.value.split("\n"),
      mathsEntryNewline
    });
    outputArea.innerHTML = JSON.stringify(
      proof,
      (key, value) => {
        if (typeof value !== "string") {
          return value;
        }
        if (key === "mathsEntry") {
          return `${mathsEntryTag}\`${value.slice(1, -1)}\``; // use the passed template
        }
        return value.replace(/\\"/g, '"'); // replace escaped double quotes
      },
      "  "
    );
    // rename mathsEntry to mathsEntryRaw since it contains the unprocessed strings
    const rename = (proof = []) =>
      proof.map(({ mathsEntry, proof: subproof = [], ...rest }) => ({
        mathsEntryRaw: mathsEntry,
        ...(subproof.length && { proof: rename(subproof) }),
        ...rest
      }));
    leanEditorObj.proofObject = rename(proof);
    // dispatch an input event so that proof object's observers can react to the update.
    leanEditorObj.node.dispatchEvent(new CustomEvent("input"));
  };
  createButton.addEventListener("click", updateProof);
  updateProof(); // initialise the proof object
  const copyButton = html`<input type="button" value="Copy proof to clipboard" style="flex: 1"/>`;
  copyButton.addEventListener("click", () => {
    /* Select the output */
    outputArea.select();
    /* Copy the text inside the output field */
    document.execCommand("copy");
  });
  return html`<div style="display: flex">
    <div style="display: flex; flex-direction: column;">
      ${createButton}
      ${copyButton}
    </div>
    ${outputArea}
  </div>`;
}38:Tb32,proofViewStyle = html`<style id="proof-view">

.${CSS_CLASSES.PROOF},
.${CSS_CLASSES.PROOF_ENTRY_MATHS_WRAPPER},
.${CSS_CLASSES.PROOF_ENTRY_SUBPROOF_WRAPPER} {
  display: flex;
  flex-direction: row;
}

.${CSS_CLASSES.PROOF_ENTRIES} {
  flex: 1 0 ${leanEditorConfig.editorPercentage*100}%;
}

.${CSS_CLASSES.PROOF_ENTRY} {
  padding: calc(${SPACING_BASELINE}) 0;
  border-top: 1px dotted black;
}

.${CSS_CLASSES.PROOF_ENTRY}:first-child {
  margin-top: 0;
  border: none;
}

.${CSS_CLASSES.PROOF_ENTRY}:last-child {
  margin-bottom: 0;
}

.${CSS_CLASSES.PROOF_ENTRY_MATHS},
.${CSS_CLASSES.PROOF_ENTRIES_UNFOLD_LEAN_ENTRIES_BUTTON},
.${CSS_CLASSES.PROOF_ENTRY_PIN_BUTTON},
.${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF} {
  cursor: pointer;
}

.${CSS_CLASSES.PROOF_ENTRY}.${CSS_CLASSES.ACTIVE} > .${CSS_CLASSES.PROOF_ENTRY_MATHS_WRAPPER} .${CSS_CLASSES.PROOF_ENTRY_MATHS} {
  background: ${COLOURS.ACTIVE};
}

.${CSS_CLASSES.PROOF_ENTRY_MATHS}:hover,
.${CSS_CLASSES.PROOF_ENTRIES_UNFOLD_LEAN_ENTRIES_BUTTON}:hover,
.${CSS_CLASSES.PROOF_ENTRY_PIN_BUTTON}:hover,
.${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF}:hover {
  background: ${COLOURS.HOVER};
}

.${CSS_CLASSES.PROOF_ENTRY_MATHS} {
  margin: ${SPACING_BASELINE} 0;
}

/* spread maths entry to the left and buttons to the right */
.${CSS_CLASSES.PROOF_ENTRY_MATHS_WRAPPER} {
  justify-content: space-between;
}

.${CSS_CLASSES.PROOF_ENTRY_MATHS_WRAPPER} .${CSS_CLASSES.PROOF_ENTRY_MATHS} {
  flex: 1;
}

.${CSS_CLASSES.PROOF_ENTRY_MATHS_BUTTONS} {
  margin: ${SPACING_BASELINE};
  margin-right: 0;
}

.${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF} {
  margin-top: ${SPACING_BASELINE};
  flex: 1; /* flex to stretch in case subproof is folded */
}

.${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF_BUTTON} {
  margin: ${SPACING_BASELINE};
  margin-left: 0;
}

.${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF_HINT} {
  color: ${COLOURS.HINT}
}

.${CSS_CLASSES.PROOF_ENTRY_SUBPROOF} {
  flex: 99999; /* not so nice: make the subproof take all the width if there is another element (i.e. the unfold button) */
}

.${CSS_CLASSES.PROOF_INFO_VIEW_WRAPPER} {
  flex-basis: ${(1-leanEditorConfig.editorPercentage)*100}%;;
  position: relative;
}

.${CSS_CLASSES.PROOF_INFO_VIEW_WRAPPER} .${CSS_CLASSES.INFO_VIEW} {
  /* Stretch the info view horizontally to full width */
  left: ${SPACING_BASELINE};
  right: 0;
}

.${CSS_CLASSES.FOLD_ICON}, .${CSS_CLASSES.UNFOLD_ICON}, .${CSS_CLASSES.PROOF_ENTRY_PIN_BUTTON} {
  border: solid black 1px;
  padding: calc(${SPACING_BASELINE} / 2);
}

@media (max-width: ${leanEditorConfig.stackWidth}) {
  .${CSS_CLASSES.PROOF} {
    /* stack info view and proof vertically */
    flex-direction: column;
  }

  .${CSS_CLASSES.PROOF_INFO_VIEW_WRAPPER} .${CSS_CLASSES.INFO_VIEW} {
    /* Unset the sticky position */
    position: inherit !important;
    top: inherit !important;
    left: 0;
  }
}
</style>`39:T57e,md`
- 22.08.2019: Initial release with proof view and footer to create proofs. (ID: @kappelmann/lean-proof-view@2436)
- 23.08.2019: Add possibility to pass tag parameter to \`proofCreatorFooter\'.
    - Breaking change: \`proofCreatorFooter\` is now a curried function expecting two optional parameters \`mathsEntryTag\` and \`mathsEntryNewline\`. (ID: @kappelmann/lean-proof-view@2603)
- 26.08.2019: Export certain values for \`proofView\` (e.g. \`docArray\` and \`infoView\`) (ID: @kappelmann/lean-proof-view@2605)
- 27.08.2019: Add utility functions \`observeProofObject\` and \`convertMathsEntryRaw\` that allow to interactively update a proof view based on an editor's value using \`proofCreatorFooter\`. Many thanks to [@bryangingechen](https://observablehq.com/@bryangingechen/) for this proposal and his help developing the feature. (ID: @kappelmann/lean-proof-view@2635)
- 10.09.2019: Add possibility to specify \`endIndex\` for the last proof entry that should be shown. Export \`startIndex\`, \`endIndex\`, and \`slicedProof\` in view.<br>
**BREAKING CHANGES**: \`indexOffset\` is renamed to \`startIndex\`. (ID: @kappelmann/lean-proof-view@2809)
- 11.09.2019: Change default newline character to \`'\\n'\`. (ID: @kappelmann/lean-proof-view@2838)
- 17.09.2021: Replace broken stringif-object reference by JSON.stringify. Thanks to @mootari for noticing! (ID: @kappelmann/lean-proof-view@@3027)
`3a:[]
2f:{"title":"Lean Proof View","cells":[{"id":0,"value":"md`# Lean Proof View`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1316,"value":"md`This notebook contains a proof view to explore a standard maths proof and the corresponding Lean proof.\n- Click on a maths cell to fold and unfold the corresponding Lean code and pin the cell's output to the info view.\n- Click on a pin icon (${activateProofEntryButtonView({})} on the top right of a cell) to pin the cell's output to the info view.\n- Click on a Lean unfold icon (${unfoldIconView({})},${foldIconView({})} on the top right of a (sub)proof) to fold or unfold the Lean proof.\n- Click on a subproof unfold cell (${unfoldIconView({})},${foldIconView({})}) to fold or unfold a subproof.\n- Hover above a maths cell to permanently see its output in the info view.\n- Click anywhere in a Lean cell to display the corresponding output in the info view.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2349,"value":"md`Moreover, this notebook contains a simple Lean editor footer that exports a proof to the format expected by the proof view so that you easily can build your own, interactive proof view.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2714,"value":"md`If you wanna start creating your own proof views, you might be interested in using [this template](https://observablehq.com/@kappelmann/proof-view-designer-template) for a quick start ⚡.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1191,"value":"md`## Example`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1209,"value":"viewof sqrtTwoIrratView = proofView({\n  proof: convertMathsEntryRaw({ proof: proofObject }),\n  invalidation,\n  startIndex: 1\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":2347,"value":"md`The proof object used for this example was created using the Lean editor footer provided below.\nThe proof is adapted from [Logic and Proof](https://leanprover.github.io/logic_and_proof/introduction.html#interactive-theorem-proving).\nClick the button in the footer to update the proof displayed above.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2217,"value":"viewof proofEditor = leanEditor({\n  fileName: 'sqrt_two_irrat.lean',\n  footer: proofCreatorFooter({}),\n  height: '350px',\n  value: sqrtTwoIrratSrcEscaped\n}, invalidation)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2630,"value":"md`The next cell contains the unprocessed proof object created by this editor.\nThe proof view at the beginning of this notebook converts this object using \\`convertMathsEntryRaw({proof: proofObject})\\` to obtain the processed proof object.\nSome caveats apply when using \\`convertMathsEntryRaw\\`, see [here](#convertMathsEntryRawCaveats).\nAlternatively, one can copy and paste the output of the footer manually to the proof object required by \\`proofView\\`.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2629,"value":"proofObject = observeProofObject(viewof proofEditor)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2628,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"id":2343,"value":"md` ## Usage`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2342,"value":"md`You can import the proof view and, if needed, the \\`proofCreatorFooter\\` like this:\n\\`\\`\\`js\nimport {proofView, proofCreatorFooter} from '@kappelmann/lean-proof-view'\n\\`\\`\\`\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2626,"value":"md`If you want to interactively develop your proof view, you might also want to include \\`observeProofObject\\` and \\`convertMathsEntryRaw\\` from this notebook.\nYou can use Observable's [import {...} with {...}](https://observablehq.com/@observablehq/introduction-to-imports) syntax if you want to override the used Lean editor objects, e.g. \\`leanEditorFrom\\` and \\`InfoView\\`.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2625,"value":"md`You can then create a proof view like this:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2341,"value":"$32","pinned":false,"hidden":false,"mode":"ojs"},{"id":2589,"value":"md`proofView exposes a number of values:\n1. \\`docArray\\`: the Lean document array used for the proof.\n2. \\`startIndex\\`: the first index of \\`docArray\\` that will be displayed.\n3. \\`endIndex\\`: the last index (non-inclusive) of \\`docArray\\` that will be displayed.\n4. \\`infoView\\`: the info view associated to the proof view.\n5. \\`proof\\`: the proof object of the proof view.\n6. \\`slicedProof\\`: the actual displayed, sliced proof object of the proof view.\n\nFor example, the next cell contains the value of the proof at the beginning of this notebook.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2590,"value":"sqrtTwoIrratView;","pinned":false,"hidden":false,"mode":"ojs"},{"id":2340,"value":"md`The simplest way to create a proof object is to use the \\`proofCreatorFooter\\`. \nJust open an instance by calling\n\\`\\`\\`javascript\nleanEditor({footer: proofCreatorFooter({mathsEntryTag, mathsEntryNewline})}, invalidation)\n\\`\\`\\`\nwhere\n\n1. \\`mathsEntryTag\\` (optional, default \\`'mdtex'\\`) is the name of a tag function, e.g. \\`'mdtex'\\`, \\`'md'\\`, \\`'html'\\`, \\`'tex'\\`, etc.\nThe default \\`'mdtex'\\` tag makes it easy to write markdown, html, and inline latex ($..$) as well as block latex ($$...$$).\n2. \\`mathsEntryNewline\\` (optional, default \\`'\\\\n'\\`) is the newline character that should be used by the passed \\`mathsEntryTag\\`.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2555,"value":"md`You can then paste your code into the editor, format it until you are happy, and then export the proof object by pressing the corresponding button in the footer.\nWe recommend to develop your code using a local installation of Lean and just fine-tune the code online.\nIf you catch yourself doing many modification online and you are afraid of loosing progress (e.g. by \naccidentally reloading the page), you might want to use \\`leanEditorWithStorage\\`:\n\\`\\`\\`javascript\nimport {leanEditorWithStorage} from \"@kappelmann/lean-editor-with-local-storage\"\n\\`\\`\\`\nand then call \n\\`\\`\\`javascript\nleanEditorWithStorage({\n  fileName: \"myFile.lean\",\n  footer: proofCreatorFooter({mathsEntryTag, mathsEntryNewline}),\n  invalidation\n})\n\\`\\`\\``","pinned":false,"hidden":false,"mode":"ojs"},{"id":2645,"value":"md`Note that the parsing is opinionated and expects a certain format (for display and easier parsing purposes):\n1. Subproofs need to start by ending a line with \"\\`{\\`\" and\n2. Subproofs need to finish by ending a line with \"\\`}\\`\".\nThat is, this\n<div>\n${leanHL`have : 1 + 1 = 2, by {\n  -- 1 + 1 = 2 is a simple computation.\n  have : 1 + 1 = 2, by norm_num,\n  -- and this is all we need.\n  exact this },`}\n</div>\nwill correctly be parsed as a subproof, whereas this\n<div>\n${leanHL`have : 1 + 1 = 2, by\n{ -- 1 + 1 = 2 is a simple computation.\n  have : 1 + 1 = 2, by norm_num,\n  -- and this is all we need.\n  exact this },`}\n</div>\nwill fail.\n3. Multiline comments need to be made using \"\\`\\\\-\\`\" (or \"\\`\\\\--\\`\") and \"\\`-/\\`\". Using multiple lines of \"\\`--\\`\" will fail.\n\nCheck out the example above for a comprehensive example usage. \nIf you are not completely happy with the output,\ne.g. you want to change some unfolds or the used tag for certain entries,\nyou can just adapt the corresponding entries manually.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2621,"value":"md`If you want to further automate this process, you can make use of the fact that the \\`proofCreatorFooter\\` stores the unprocessed proof object in the \\`proofObject\\` key of the associated editor.\nYou can use the utility function \\`observeProofObject(viewof proofEditor)\\`, where \\`proofEditor\\` is the name of the\neditor associated to the footer, to observe this value.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2620,"value":"md`You can then pass the unprocessed proof object to the proof view using the utility function \\`convertMathsEntryRaw({proof: proofObject, tag: mdtex})\\`, where\n1. \\`proofObject\\` is the name of the unprocessed proof object, and\n2. \\`tag\\` (optional, default \\`mdtex\\`) is the name of a tag function used to convert the raw maths entry to the processed output entry.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2619,"value":"convertMathsEntryRawCaveats = md`Note, however, that \\`convertMathsEntryRaw\\` will only be able to process top-level tex and md code. In particular, it will not be able to execute JavaScript code.\nFor example, the entry\n\\`\\`\\`javascript\n\"This finishes the proof. <span style='float: right'>$\\\\square$</span>\"\n\\`\\`\\`\nwill correctly be formatted to\n\n> ${mdtex`This finishes the proof. <span style='float: right'>$\\square$</span>`}\n\nwheras the entry\n\\`\\`\\`javascript\n\"We have 1 + 1 = \\$\\{1 + 1\\}\"\n\\`\\`\\`\nwill result in \"We have 1 + 1 = \\$\\{1 + 1\\}\" and not \"We have 1 + 1 = 2\".`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1194,"value":"md`## Implementation`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1675,"value":"md`### Variables`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2338,"value":"// text that will be displayed as a hint to unfold a subproof\nUNFOLD_SUBPROOF_HINT_VIEW_TEXT = \"Click to unfold the subproof\"","pinned":false,"hidden":false,"mode":"ojs"},{"id":2337,"value":"STATE = ({\n  MATHS: 0,\n  LEAN: 1\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":2336,"value":"md`#### RegEx`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2335,"value":"BLOCK_COMMENT_START_REGEX = /^\\/--?(.*)/","pinned":false,"hidden":false,"mode":"ojs"},{"id":2334,"value":"BLOCK_COMMENT_END_REGEX = /(.*)-\\/$/","pinned":false,"hidden":false,"mode":"ojs"},{"id":2333,"value":"LINE_COMMENT_REGEX = /^--(.*)/","pinned":false,"hidden":false,"mode":"ojs"},{"id":2332,"value":"SUBPROOF_START_REGEX = /{$/","pinned":false,"hidden":false,"mode":"ojs"},{"id":2331,"value":"SUBPROOF_END_REGEX = /},?$/","pinned":false,"hidden":false,"mode":"ojs"},{"id":1197,"value":"md`### Code`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2175,"value":"md`#### Proof View`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1220,"value":"$33","pinned":false,"hidden":false,"mode":"ojs"},{"id":2162,"value":"// creates a docArray as expected by `leanEditorFrom` by flattening the recursive proof structure\nfunction createDocArray(proof, initAcc = []) {\n  return proof.reduce((acc, { leanEntry, proof: subProof = []} ) => createDocArray(subProof, [...acc, leanEntry]),\n    initAcc);\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":2373,"value":"function compInitEditorIndex({ proof, index }) {\n  let counter = 0;\n  for (let i = 0; i < index; ++i) {\n    const { proof: subproof = [] } = proof[i];\n    counter +=\n      1 + compInitEditorIndex({ proof: subproof, index: subproof.length });\n  }\n  return counter;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1642,"value":"unfoldIconView = ({}) => html`<span class=\"${CSS_CLASSES.UNFOLD_ICON}\">➕</span>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1648,"value":"foldIconView = ({}) => html`<span class=\"${CSS_CLASSES.FOLD_ICON}\">➖</span>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1624,"value":"unfoldSubproofButtonView = ({unfold = true}) => html`\n  <span class=\"${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF_BUTTON}\"> \n    ${unfold ? unfoldIconView({}) : foldIconView({})}\n  </span>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1633,"value":"unfoldSubproofHintView = ({unfold = true, text = UNFOLD_SUBPROOF_HINT_VIEW_TEXT}) => html`\n  <span class=\"${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF_HINT} ${unfold ? \"\" : CSS_CLASSES.HIDDEN}\"> \n    ${text}\n  </span>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1595,"value":"// `unfold = true` shows the unfold button and hint\nunfoldSubproofView = ({unfold = true}) => html`\n  <div class=\"${CSS_CLASSES.PROOF_ENTRY_UNFOLD_SUBPROOF}\">\n    ${unfoldSubproofButtonView({unfold})}\n    ${unfoldSubproofHintView({unfold})}\n  </div>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1588,"value":"subproofView = ({ subNodes, hidden = true }) => html`\n  <div class=\"${`${CSS_CLASSES.PROOF_ENTRY_SUBPROOF} ${hidden ? CSS_CLASSES.HIDDEN : \"\"}`}\">\n    ${subNodes}\n  </div>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1752,"value":"unfoldLeanEntriesButtonView = ({unfold = true}) => html`\n  <span class=\"${CSS_CLASSES.PROOF_ENTRIES_UNFOLD_LEAN_ENTRIES_BUTTON}\"> \n    ${unfold ? unfoldIconView({}): foldIconView({})}\n  </span>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1435,"value":"$34","pinned":false,"hidden":false,"mode":"ojs"},{"id":1598,"value":"mathsEntryView = ({mathsEntry}) => html`\n  <div class=\"${CSS_CLASSES.PROOF_ENTRY_MATHS}\">\n    ${mathsEntry}\n  </div>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2051,"value":"activateProofEntryButtonView = ({}) => html`<span class=\"${CSS_CLASSES.PROOF_ENTRY_PIN_BUTTON}\">📌</span>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2054,"value":"mathsEntryButtonsView = ({unfoldLeanEntriesButton: {show = false, unfold}}) => html`\n  <div class=\"${CSS_CLASSES.PROOF_ENTRY_MATHS_BUTTONS}\">\n    ${show ? unfoldLeanEntriesButtonView({unfold}) : ``}\n    ${activateProofEntryButtonView({})}\n  </div>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2039,"value":"mathsEntryWrapperView = ({ mathsEntry, unfoldLeanEntriesButton = {} }) => html`\n  <div class=\"${CSS_CLASSES.PROOF_ENTRY_MATHS_WRAPPER}\">\n    ${mathsEntryView({mathsEntry})}\n    ${mathsEntryButtonsView({unfoldLeanEntriesButton})}\n  </div>`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1607,"value":"leanEntryView = ({editor, hidden = true}) => html`\n  <div class=\"${CSS_CLASSES.PROOF_ENTRY_LEAN} ${hidden ? CSS_CLASSES.HIDDEN : \"\"}\">\n    ${editor}\n  </div>`;","pinned":false,"hidden":false,"mode":"ojs"},{"id":2007,"value":"// get the proof parent of an element\ngetProofParent = (el) => el.closest(`.${CSS_CLASSES.PROOF}`)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2125,"value":"// the the proof entry parent of an element\ngetProofEntryParent = (el) => el.closest(`.${CSS_CLASSES.PROOF_ENTRY}`)","pinned":false,"hidden":false,"mode":"ojs"},{"id":2019,"value":"// get the active proof entry for a given proof element\ngetActiveProofEntry = (proof) => proof.querySelector(`.${CSS_CLASSES.PROOF_ENTRY}.${CSS_CLASSES.ACTIVE}`)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1226,"value":"$35","pinned":false,"hidden":false,"mode":"ojs"},{"id":2179,"value":"md`#### Proof Creator Footer`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2327,"value":"$36","pinned":false,"hidden":false,"mode":"ojs"},{"id":2219,"value":"$37","pinned":false,"hidden":false,"mode":"ojs"},{"id":2617,"value":"// observes the proof object of a Lean editor\nobserveProofObject = (editorView) => Generators.observe(change => {\n  let last = null;\n  const inputted = () => {\n    const {proofObject} = editorView.value;\n    if (JSON.stringify(proofObject) !== JSON.stringify(last)) {\n      last = proofObject;\n      change(proofObject);\n    }\n  };\n  \n  editorView.addEventListener(\"input\", inputted);\n  change(editorView.value.proofObject);\n  return () => editorView.removeEventListener(\"input\", inputted);\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":2616,"value":"// converts the raw strings from mathsEnryRaw to the processed output and stores it in mathsEntry\nconvertMathsEntryRaw = ({tag = mdtex, proof}) => {\n  const convert = (proof = []) => proof.map(({mathsEntryRaw, proof: subproof = [], ...rest}) => {\n    const mathsTemplate = [mathsEntryRaw];\n    mathsTemplate.raw = mathsTemplate;\n    return {\n      mathsEntry: tag(mathsTemplate),\n      ...(subproof.length && {proof: convert(subproof)}),\n      ...rest\n    }\n  });\n  return convert(proof);\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1334,"value":"md`### Styling`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1263,"value":"CSS_CLASSES = ({\n  FOLD_ICON: 'fold-icon',\n  UNFOLD_ICON: 'unfold-icon',\n  PROOF: 'proof',\n  PROOF_ENTRIES: 'proof-entries',\n  PROOF_ENTRIES_UNFOLD_LEAN_ENTRIES_BUTTON: 'proof-entries-unfold-lean-entries-button',\n  PROOF_ENTRY: 'proof-entry',\n  PROOF_ENTRY_MATHS: 'proof-entry-maths',\n  PROOF_ENTRY_MATHS_WRAPPER: 'proof-entry-maths-wrapper',\n  PROOF_ENTRY_MATHS_BUTTONS: 'proof-entry-maths-buttons',\n  PROOF_ENTRY_LEAN: 'proof-entry-lean',\n  PROOF_ENTRY_PIN_BUTTON: 'proof-entry-pin-button',\n  PROOF_ENTRY_SUBPROOF_WRAPPER: 'proof-entry-subproof-wrapper',\n  PROOF_ENTRY_SUBPROOF: 'proof-entry-subproof',\n  PROOF_ENTRY_UNFOLD_SUBPROOF: 'proof-entry-subproof-unfold',\n  PROOF_ENTRY_UNFOLD_SUBPROOF_BUTTON: 'proof-entry-unfold-subproof-button',\n  PROOF_ENTRY_UNFOLD_SUBPROOF_HINT: 'proof-entry-unfold-subproof-hint',\n  PROOF_INFO_VIEW_WRAPPER: 'proof-info-view-wrapper',\n  ...BASE_CSS_CLASSES\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":1281,"value":"$38","pinned":false,"hidden":false,"mode":"ojs"},{"id":1950,"value":"md`## Acknowledgements`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1953,"value":"md`\nThis work was created as part of the [Lean Forward Project](https://lean-forward.github.io/).\n\n1. Thanks to [@bryangingechen](https://observablehq.com/@bryangingechen/hello-lean-prover) for his awesome [Lean observable integration](https://observablehq.com/@bryangingechen/hello-lean-prover) and his help to make the hover functionality and sidebar work.\n2. Thanks to [@mootari](https://observablehq.com/@mootari/) for his awesome sticky positioning notebook created due to my [forum post](https://talk.observablehq.com/t/sticky-sidebar-in-cell/2268).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2323,"value":"LICENSE = md`## License:\n\nCopyright 2019 @ [Kevin Kappelmann](https://kappelmann.me)\n\nLicensed under the Apache License, Version 2.0 (the \"License\");\nyou may not use this file except in compliance with the License.\nYou may obtain a copy of the License at [http://www.apache.org/licenses/LICENSE-2.0](http://www.apache.org/licenses/LICENSE-2.0).\n\nUnless required by applicable law or agreed to in writing, software\ndistributed under the License is distributed on an \"AS IS\" BASIS,\nWITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\nSee the License for the specific language governing permissions and\nlimitations under the License.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2322,"value":"md`This work makes use of the following open-source projects using the given licenses:\n* [Apache License 2.0](https://www.apache.org/licenses/LICENSE-2.0.html)\n    * [Hello Lean Prover](https://observablehq.com/@bryangingechen/hello-lean-prover)\n* Without license\n    * [Sticky positioning](https://observablehq.com/@mootari/)\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1187,"value":"md`## Imports`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2729,"value":"import {\n  LEAN_LIBS,\n  leanEditorConfig,\n  INTERNAL_CSS,\n  CSS_CLASSES as BASE_CSS_CLASSES,\n  COLOURS,\n  SPACING_BASELINE\n} from '@kappelmann/lean-configuration'","pinned":false,"hidden":false,"mode":"ojs"},{"id":2733,"value":"leanLibName = LEAN_LIBS.MATHLIB","pinned":false,"hidden":false,"mode":"ojs"},{"id":2738,"value":"import { leanEditor, leanEditorFrom, leanHL, InfoView } with {\n  leanLibName,\n  INTERNAL_CSS,\n  leanEditorConfig as config\n} from '@bryangingechen/hello-lean-prover'","pinned":false,"hidden":false,"mode":"ojs"},{"id":2750,"value":"import { addCSS } from '@kappelmann/general-utilities'","pinned":false,"hidden":false,"mode":"ojs"},{"id":2758,"value":"import { mdtex } from '@kappelmann/tag-utilities'","pinned":false,"hidden":false,"mode":"ojs"},{"id":1364,"value":"import {makeSticky} from '@mootari/sticky-positioning'","pinned":false,"hidden":false,"mode":"ojs"},{"id":2319,"value":"md`## Version History`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2318,"value":"$39","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W3a","stdlib":"1","titling":"auto"}
</article></body></html>