From 47603486da5bfb84bd73c2e45ca9f1593c3add55 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Tue, 15 Feb 2022 12:56:13 +0100 Subject: [PATCH 01/30] import/export according to new specification --- src/io/compileToVO.js | 4 +- src/io/notebook.js | 164 ++++++++++++++++++++++------------------ src/io/specification.md | 43 +++++++++++ 3 files changed, 135 insertions(+), 76 deletions(-) create mode 100644 src/io/specification.md diff --git a/src/io/compileToVO.js b/src/io/compileToVO.js index 0aa09d33..6484e75e 100644 --- a/src/io/compileToVO.js +++ b/src/io/compileToVO.js @@ -5,7 +5,7 @@ const util = require('util'); const execFile = util.promisify(require('child_process').execFile); import {getAppdataPath, getResourcesPath} from './pathHelper'; import read, {deleteFile, doesFileExist, readFile} from './readfile'; -import {blockToCoqText} from './notebook'; +import {wpToCoq} from './notebook'; const extensions = ['wpn', 'v', 'vo']; @@ -105,7 +105,7 @@ class VOCompiler { return; } const notebook = await readFile(filepath); - const text = blockToCoqText(notebook.blocks); + const text = wpToCoq(notebook.blocks); return new Promise((resolve, reject) => { fs.writeFile(filepath.substring(0, filepath.length - 3) + 'v', text, diff --git a/src/io/notebook.js b/src/io/notebook.js index 3772f01c..9f0ef322 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -1,11 +1,5 @@ const fs = require('fs'); -const COQ_COMMENT_START = '(*'; -const COQ_SPECIAL_COMMENT_START = '(** '; -const COQ_COMMENT_END = '*)'; -const COQ_INPUT_START = '(* Start of input area *)'; -const COQ_INPUT_END = '(* End of input area *)'; - const DEFAULT_BLACKLIST = [ // commands that allow introducing theorems without proof 'Parameter', @@ -275,7 +269,7 @@ class Notebook { * @return {String} text that will be displayed */ parseToText(hints = true, textblocks = true, coqcode = true) { - return blockToCoqText(this.blocks); + return wpToCoq(this.blocks); } /** @@ -503,7 +497,7 @@ class Notebook { this.createCodeBlock(coqText), ]; } else { - this.blocks = this.coqToCodeAndText(coqText); + this.blocks = coqToWp(coqText); } }; @@ -535,88 +529,110 @@ class Notebook { return stringPieces; } +} - /** - * Converts coq code to a notebook format - * This does not convert back any waterproof things and just puts all - * special comments in text blocks and the rest in code blocks. - * @param {String} coqCode the input code - * @return {Array} the blocks from the code - */ - coqToCodeAndText(coqCode) { - const blocks = []; - let contentLeft = coqCode.replace(/\r/g, ''); - while (contentLeft.length > 0) { - let nextComment = contentLeft.indexOf(COQ_SPECIAL_COMMENT_START); - - if (nextComment < 0 || nextComment > 0) { - const codeBeforeComment = nextComment >= 0 ? - contentLeft.substring(0, nextComment) : contentLeft; - const codePieces = - this.cutStringBetweenKeywords(codeBeforeComment.trim()); - for (let i = 0; i < codePieces.length; i++) { - blocks.push(this.createCodeBlock(codePieces[i])); - } - if (nextComment < 0) { - break; - } - } +export default Notebook; - contentLeft = contentLeft.substring(nextComment) - .replace(COQ_SPECIAL_COMMENT_START, ''); +/** + * Convert text to never break a Coq comment + * @param {string} text + * @return {string} + */ +function createSafeCoqComment(text) { + return text.replaceAll('*)', '*💧)') + .replaceAll('(*', '(💧*') + .replaceAll('"', '""'); +} - let startPos = 0; - let endPos = 0; - nextComment = contentLeft.indexOf(COQ_COMMENT_START, startPos); - let commentEnd = contentLeft.indexOf(COQ_COMMENT_END, endPos); +/** + * Revert the changes made by createSafeCoqComment + * @param {string} text + * @return {string} + */ +function revertSafeCoqComment(text) { + return text.replaceAll('*💧)', '*)') + .replaceAll('(💧*', '(*') + .replaceAll('""', '"'); +} - while (commentEnd >= 0 && nextComment >=0 && nextComment < commentEnd) { - startPos = nextComment + 2; - endPos = commentEnd + 2; - nextComment = contentLeft.indexOf(COQ_COMMENT_START, startPos); - commentEnd = contentLeft.indexOf(COQ_COMMENT_END, endPos); - } +/** + * Small class to wrap errors + */ +class ImportError extends Error { + // eslint-disable-next-line require-jsdoc + constructor(message) { + super(message); + this.name = 'ImportError'; + } +} - if (commentEnd < 0) { - blocks.push(this.createTextBlock(contentLeft)); - break; +/** + * Converts coq code to a notebook format + * This does not convert back any waterproof things and just puts all + * special comments in text blocks and the rest in code blocks. + * @param {String} coqCode the input code + * @return {Array} the blocks from the code + */ +function coqToWp(coqCode) { + const blocks = []; // return array + const blockStrings = coqCode.split('(*💧'); // seperate block strings + // The first part after .split is the empty space before the first block start + if (blockStrings.shift().trim() !== '') { + throw new ImportError('Did not start with a block.'); + } + let inInputField = false; + for (let i = 0; i < blockStrings.length; i++) { + const blockString = blockStrings[i]; + const dataEnd = blockString.indexOf('*)'); + const dataString = blockString.substring(0, dataEnd); + // should contain type and possibly start and id + const block = JSON.parse(dataString); + Notebook.setDefaultBlockState(block, inInputField); + if (block.type !== 'input') { + // get text part, so skip '*)\n' which is 3 chars. + let textString = blockString.substring(dataEnd + 3); + if (i !== blockStrings.length - 1) { + // removing trailing \n, which was added by join. + textString = textString.substring(0, textString.length -1); } - - blocks.push(this.createTextBlock(contentLeft.substring(0, commentEnd))); - contentLeft = contentLeft.substring(commentEnd) - .replace(COQ_COMMENT_END, ''); + if (block.type !== 'code') { + // remove everything around [text] of (*[text]*) revert [text] + textString = textString.substring(2, textString.length -2); + textString = revertSafeCoqComment(textString); + } + block.text = textString; + } else { + inInputField = block.start; } - - return blocks; + blocks.push(block); } + return blocks; } -export default Notebook; - /** - * Convert blocks into a coq parsable text + * Convert blocks into coq parsable text, following specification.md * @param {[]} blocks the list of blocks - * @return {string} the coq valid text + * @return {string} the coq text */ -function blockToCoqText(blocks) { - let coqContent = ''; +function wpToCoq(blocks) { + const blockStrings = []; for (const block of blocks) { - if (block.type === 'code') { - coqContent += block.text; - } else if (block.type === 'input') { - if (block.start) { - coqContent += COQ_SPECIAL_COMMENT_START + COQ_INPUT_START - + COQ_COMMENT_END; - } else { - coqContent += COQ_SPECIAL_COMMENT_START + COQ_INPUT_END - + COQ_COMMENT_END; + let data = {type: block.type}; + if (block.type === 'input') { + data.start = block.start; + data.id = block.id; + } + data = '(*💧' + JSON.stringify(data) + '*)'; + if (block.type !== 'input') { + let text = block.text; + if (block.type !== 'code') { + text = '(*' + createSafeCoqComment(text) + '*)'; } - } else { - coqContent += COQ_SPECIAL_COMMENT_START + block.text + COQ_COMMENT_END; + data = data + '\n' + text; } - coqContent += '\n'; + blockStrings.push(data); } - return coqContent; + return blockStrings.join('\n'); } -export {blockToCoqText, COQ_SPECIAL_COMMENT_START}; +export {coqToWp, wpToCoq}; diff --git a/src/io/specification.md b/src/io/specification.md new file mode 100644 index 00000000..48a245ef --- /dev/null +++ b/src/io/specification.md @@ -0,0 +1,43 @@ +# Importing/exporting waterproof notebooks from/to vernacular file + +We aim to maintain consistent files when importing a previously exported file, with no loss of content. + + +## Block structure + +Waterproof notebooks are made out of a collection of text, code, input, and hint blocks. When exporting to a vernacular file, we do not want to lose this block information, so that the file can be imported again and the structure is maintained. Therefore, a waterproof block is translated to Coq as: +> `(*💧 [data]*)[text]` + +Here, `💧` is meant to be a rare enough unicode character. Additional json data contained in the waterproof notebook is stored in json-structure as `[data]`. Except text or code, which is then put in place of `[text]`. For non-code blocks, `[text]` is wrapped in `(*` and `*)`. + +## Unintentional comment start/end + +Coq uses `(*` and `*)` to denote comment start and end. +These can be used recursively. +Unfortunately, it is easy to unintentionally write these. +For example, the following waterproof text sentence: + +> (Water *proof*) text + +is syntactically `(Water *proof*) text`, which inadvertently contains a comment ending in Coq. Therefore, we will add a special character to remove any comment start or end non-code. The above sentence will become `(Water *proof*💧) text`. + +## String literals + +Moreover, Coq string literals in comments *must* be completed in order to be parsed correctly. Strings begin and end with double quotes (`"`). Hence, to avoid an odd number of double quotes, we duplicate every occurence of `"`. + +## Notebook or exercise sheet? + +Currently always import as notebook. So previously exported exercise sheet can become notebook. Should this be different? + +## Summary + +For every waterproof block, which is an object that looks like `{type: String, ?text: String, ?start: Boolean, ?id: String}`, the Coq equivalent will be: +- `(*💧type: [type]*)\n[text]` if type is `code`. +- `(*💧type: [type], start: [start], id: [id]*)` if type is `input`. +- `(*💧type: [type]*)\n(*[text]*)` for other types. + +We separate blocks by adding an extra newline. + +Moreover, for non code blocks, all text in `text` is filtered to replace `(*` and `*)` with `(💧*` and `*💧)` respectively, and double quotes (`"`) are duplicated. + +The inverse is done to import. \ No newline at end of file From d5c64904bbb043f4d4e12e88a8c98dd6cfa63b98 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Wed, 2 Mar 2022 22:03:53 +0100 Subject: [PATCH 02/30] changed specification and implementation to stay in coq(doc)-style --- src/io/notebook.js | 59 +++++++++++++++-------------------------- src/io/specification.md | 6 +++-- 2 files changed, 25 insertions(+), 40 deletions(-) diff --git a/src/io/notebook.js b/src/io/notebook.js index 9f0ef322..21098cdf 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -555,17 +555,6 @@ function revertSafeCoqComment(text) { .replaceAll('""', '"'); } -/** - * Small class to wrap errors - */ -class ImportError extends Error { - // eslint-disable-next-line require-jsdoc - constructor(message) { - super(message); - this.name = 'ImportError'; - } -} - /** * Converts coq code to a notebook format * This does not convert back any waterproof things and just puts all @@ -574,33 +563,24 @@ class ImportError extends Error { * @return {Array} the blocks from the code */ function coqToWp(coqCode) { + // eslint-disable-next-line max-len + const regexp = /\(\*\*\s+\(\*(?(?:(?!\*\))[\s\S])*)\*\)(?(?:(?!\*\))[\s\S])*)\s\*\)(?(?:(?!\(\*\*\s+\(\*)[\s\S])*)/g; + const blockMatches = [...coqCode.matchAll(regexp)]; const blocks = []; // return array - const blockStrings = coqCode.split('(*💧'); // seperate block strings - // The first part after .split is the empty space before the first block start - if (blockStrings.shift().trim() !== '') { - throw new ImportError('Did not start with a block.'); - } let inInputField = false; - for (let i = 0; i < blockStrings.length; i++) { - const blockString = blockStrings[i]; - const dataEnd = blockString.indexOf('*)'); - const dataString = blockString.substring(0, dataEnd); - // should contain type and possibly start and id - const block = JSON.parse(dataString); + for (let i = 0; i < blockMatches.length; i++) { + const blockMatch = blockMatches[i]; + const data = blockMatch.groups.data.trim(); + const text = blockMatch.groups.text.trim(); + const code = blockMatch.groups.code.trim(); + const block = JSON.parse(data); Notebook.setDefaultBlockState(block, inInputField); if (block.type !== 'input') { - // get text part, so skip '*)\n' which is 3 chars. - let textString = blockString.substring(dataEnd + 3); - if (i !== blockStrings.length - 1) { - // removing trailing \n, which was added by join. - textString = textString.substring(0, textString.length -1); - } if (block.type !== 'code') { - // remove everything around [text] of (*[text]*) revert [text] - textString = textString.substring(2, textString.length -2); - textString = revertSafeCoqComment(textString); + block.text = revertSafeCoqComment(text); + } else { + block.text = code; } - block.text = textString; } else { inInputField = block.start; } @@ -618,19 +598,22 @@ function wpToCoq(blocks) { const blockStrings = []; for (const block of blocks) { let data = {type: block.type}; + let text = ''; + let code = ''; if (block.type === 'input') { data.start = block.start; data.id = block.id; } - data = '(*💧' + JSON.stringify(data) + '*)'; + data = JSON.stringify(data); if (block.type !== 'input') { - let text = block.text; - if (block.type !== 'code') { - text = '(*' + createSafeCoqComment(text) + '*)'; + if (block.type === 'code') { + code = block.text; + } else { + text = createSafeCoqComment(block.text); } - data = data + '\n' + text; } - blockStrings.push(data); + const blockString = '(** (* ' + data + ' *) ' + text + ' *)' + code; + blockStrings.push(blockString); } return blockStrings.join('\n'); } diff --git a/src/io/specification.md b/src/io/specification.md index 48a245ef..2f3905b6 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -6,9 +6,11 @@ We aim to maintain consistent files when importing a previously exported file, w ## Block structure Waterproof notebooks are made out of a collection of text, code, input, and hint blocks. When exporting to a vernacular file, we do not want to lose this block information, so that the file can be imported again and the structure is maintained. Therefore, a waterproof block is translated to Coq as: -> `(*💧 [data]*)[text]` +> `(** (*[data]*)[text] *)[code]` -Here, `💧` is meant to be a rare enough unicode character. Additional json data contained in the waterproof notebook is stored in json-structure as `[data]`. Except text or code, which is then put in place of `[text]`. For non-code blocks, `[text]` is wrapped in `(*` and `*)`. +Where `[data]` is the json data contained in the waterproof notebook except the +text or code, and `[text]` and `[code]` are the text and code respectively. +We can accept some variability in terms of ## Unintentional comment start/end From be0842bc3ac21f5a0d6434ed93027f0d7dbf3428 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Thu, 3 Mar 2022 12:00:45 +0100 Subject: [PATCH 03/30] switch order of text and data in comment otherwise coqdoc would not render headers properly --- src/io/notebook.js | 4 ++-- src/io/specification.md | 15 +++++++++++++-- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/io/notebook.js b/src/io/notebook.js index 21098cdf..1552a624 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -564,7 +564,7 @@ function revertSafeCoqComment(text) { */ function coqToWp(coqCode) { // eslint-disable-next-line max-len - const regexp = /\(\*\*\s+\(\*(?(?:(?!\*\))[\s\S])*)\*\)(?(?:(?!\*\))[\s\S])*)\s\*\)(?(?:(?!\(\*\*\s+\(\*)[\s\S])*)/g; + const regexp = /\(\*\*\s(?(?:(?!\(\*)(?!\*\))[\s\S])*)\(\*(?(?:(?!\*\))[\s\S])*)\*\)\s\*\)(?(?:(?!\(\*\*\s)[\s\S])*)/g; const blockMatches = [...coqCode.matchAll(regexp)]; const blocks = []; // return array let inInputField = false; @@ -612,7 +612,7 @@ function wpToCoq(blocks) { text = createSafeCoqComment(block.text); } } - const blockString = '(** (* ' + data + ' *) ' + text + ' *)' + code; + const blockString = '(** ' + text + '(* ' + data + ' *) *)' + code; blockStrings.push(blockString); } return blockStrings.join('\n'); diff --git a/src/io/specification.md b/src/io/specification.md index 2f3905b6..f128c65b 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -6,11 +6,22 @@ We aim to maintain consistent files when importing a previously exported file, w ## Block structure Waterproof notebooks are made out of a collection of text, code, input, and hint blocks. When exporting to a vernacular file, we do not want to lose this block information, so that the file can be imported again and the structure is maintained. Therefore, a waterproof block is translated to Coq as: -> `(** (*[data]*)[text] *)[code]` +> `(** [text] (*[data]*) *)[code]` Where `[data]` is the json data contained in the waterproof notebook except the text or code, and `[text]` and `[code]` are the text and code respectively. -We can accept some variability in terms of +We can accept some variability in terms of spacing. + +To be precise, to import blocks, we match .v text using the following regular expression (javascript regexp in this case): +``` +/\(\*\*\s(?(?:(?!\(\*)(?!\*\))[\s\S])*)\(\*(?(?:(?!\*\))[\s\S])*)\*\)\s\*\)(?(?:(?!\(\*\*\s)[\s\S])*)/g +``` +Notice that we assume: +- `[text]` does not contain `(*` or `*)`, +- `[data]` does not contain `*)`, +- `[code]` does not contain `(** `. + +Perhaps the latter assumption is a bit strong, as we do not allow coqdoc comments inside of code blocks. ## Unintentional comment start/end From 41c4585f6fd5ae6b316883e23417bdfd2ca1f4c1 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 21 Mar 2022 11:48:36 +0100 Subject: [PATCH 04/30] incorporate suggestions from meeting 21-03 in specification, but not in implementation --- src/io/specification.md | 58 +++++++++++++++++------------------------ 1 file changed, 24 insertions(+), 34 deletions(-) diff --git a/src/io/specification.md b/src/io/specification.md index f128c65b..6c5304cf 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -1,34 +1,24 @@ # Importing/exporting waterproof notebooks from/to vernacular file - -We aim to maintain consistent files when importing a previously exported file, with no loss of content. +We aim to make the exported .v files easy to read, and adhering to coqdoc format for nice coqdoc rendering. We are a bit constrained as we like *exact reproducibility*, though we will settle for approximate reproducibility for the benefit of readability of .v files. ## Block structure -Waterproof notebooks are made out of a collection of text, code, input, and hint blocks. When exporting to a vernacular file, we do not want to lose this block information, so that the file can be imported again and the structure is maintained. Therefore, a waterproof block is translated to Coq as: -> `(** [text] (*[data]*) *)[code]` - -Where `[data]` is the json data contained in the waterproof notebook except the -text or code, and `[text]` and `[code]` are the text and code respectively. -We can accept some variability in terms of spacing. - -To be precise, to import blocks, we match .v text using the following regular expression (javascript regexp in this case): -``` -/\(\*\*\s(?(?:(?!\(\*)(?!\*\))[\s\S])*)\(\*(?(?:(?!\*\))[\s\S])*)\*\)\s\*\)(?(?:(?!\(\*\*\s)[\s\S])*)/g -``` -Notice that we assume: -- `[text]` does not contain `(*` or `*)`, -- `[data]` does not contain `*)`, -- `[code]` does not contain `(** `. +Waterproof notebooks are made out of a collection of blocks, and each has one of the following types of block: text, code, input, and hint block. We translate these blocks according to their type. We choose to get rid of unnecessary metadata, and infer this when re-importing the blocks. +Concretely, a block in waterproof is an object containing a `type` and `text`. If it is an input block, it also contains `start` and `id`. We translate this as follows: +- If it is a code block: simply return `text`. Note that we will not be able to interpret whether two code blocks should be separated. +- If it is a text block: return `(** text *)`. +- If it is a hint block: return `(** HINT text *)`. **And implement in waterproof that the hint-closed text is immutable** +- If it is an input block: + - with `start == True`: return `(** INPUT-START *)` + - with `start == False`: return `(** INPUT-END *)` **We could get away with only writing INPUT and inferring whether it is start or end, but this is more informative in .v files in my opinion** -Perhaps the latter assumption is a bit strong, as we do not allow coqdoc comments inside of code blocks. +For re-importing, everything we encounter that is not in a `(**` and `*)` is a code block. Originally contiguous code blocks will become one large code blocks. To split these up, you can input an empty text block `(** *)` or even `(***)` (the latter is not rendered in coqdoc, while the former is rendered as an empty line). ## Unintentional comment start/end -Coq uses `(*` and `*)` to denote comment start and end. -These can be used recursively. -Unfortunately, it is easy to unintentionally write these. -For example, the following waterproof text sentence: +Coq uses `(*` and `*)` to denote comment start and end. These can be used recursively. If they are in text and are exported inside a `(** *)`, it will interfere with the formatting. +Unfortunately, it is easy to unintentionally write these. For example, the following waterproof text sentence: > (Water *proof*) text @@ -36,21 +26,21 @@ is syntactically `(Water *proof*) text`, which inadvertently contains a comment ## String literals -Moreover, Coq string literals in comments *must* be completed in order to be parsed correctly. Strings begin and end with double quotes (`"`). Hence, to avoid an odd number of double quotes, we duplicate every occurence of `"`. +Moreover, Coq string literals in comments *must* be completed in order to be parsed correctly. Strings begin and end with double quotes (`"`). To avoid an odd number of double quotes, we add an `"` to the end of `text` if it contains only one. -## Notebook or exercise sheet? - -Currently always import as notebook. So previously exported exercise sheet can become notebook. Should this be different? +## Using \#{1-6} +In waterproof (markdown) we may start text with `# `, `## `, ..., `###### ` to indicate various levels of headings, but in coqdoc we must use `* `, `** `, `**** `. Hence, we translate `#{1-4} ` at the start of a block to `*{1-4} ` and back to `#{1-4}` again. **If there is `#{5,6}` I don't know what to do yet**. -## Summary +## Bold/italics +In waterproof (markdown) we may use `**text**` and `*text*` to write bold/italics respectively. In coq, we can do emphasis (italics) with `_text_`. Bold is a bit harder, but we can use `##text##`. -For every waterproof block, which is an object that looks like `{type: String, ?text: String, ?start: Boolean, ?id: String}`, the Coq equivalent will be: -- `(*💧type: [type]*)\n[text]` if type is `code`. -- `(*💧type: [type], start: [start], id: [id]*)` if type is `input`. -- `(*💧type: [type]*)\n(*[text]*)` for other types. +## Coqdoc escape characters +To simply output the characters $, % and # and escaping their escaping role in coqdoc, these characters are be doubled. In coqdoc, `$text$` would output text in latex math-mode. **However, this does not work for HTML-output, so it is quite useless.** +It is a little bit of a problem, because stuff in # is simply discarded in latex output actually. +https://coq.inria.fr/refman/using/tools/coqdoc.html#escaping-to-latex-and-html -We separate blocks by adding an extra newline. +## Notebook or exercise sheet? -Moreover, for non code blocks, all text in `text` is filtered to replace `(*` and `*)` with `(💧*` and `*💧)` respectively, and double quotes (`"`) are duplicated. +Always import as notebook. So previously exported exercise sheet can become notebook. -The inverse is done to import. \ No newline at end of file +***Should this be different? We could import exercise sheets as exercise sheets, but they are mutable as .v files anyways, and this will also complicate the UI*** From c7b257841f5df65278049466d60aa164d31e644b Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 4 Apr 2022 10:18:13 +0200 Subject: [PATCH 05/30] typo --- src/io/specification.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/io/specification.md b/src/io/specification.md index 6c5304cf..dcf2cef3 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -35,7 +35,7 @@ In waterproof (markdown) we may start text with `# `, `## `, ..., `###### ` to i In waterproof (markdown) we may use `**text**` and `*text*` to write bold/italics respectively. In coq, we can do emphasis (italics) with `_text_`. Bold is a bit harder, but we can use `##text##`. ## Coqdoc escape characters -To simply output the characters $, % and # and escaping their escaping role in coqdoc, these characters are be doubled. In coqdoc, `$text$` would output text in latex math-mode. **However, this does not work for HTML-output, so it is quite useless.** +To simply output the characters \$, % and # and escaping their escaping role in coqdoc, these characters are be doubled. In coqdoc, `$text$` would output text in latex math-mode. **However, this does not work for HTML-output, so it is quite useless.** It is a little bit of a problem, because stuff in # is simply discarded in latex output actually. https://coq.inria.fr/refman/using/tools/coqdoc.html#escaping-to-latex-and-html From 58e54331f68ba80b9bd1ab0efbd2e1f3bca703bc Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 4 Apr 2022 12:10:16 +0200 Subject: [PATCH 06/30] Update specification with inline code --- src/io/specification.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/io/specification.md b/src/io/specification.md index dcf2cef3..07954c63 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -8,7 +8,7 @@ Waterproof notebooks are made out of a collection of blocks, and each has one of Concretely, a block in waterproof is an object containing a `type` and `text`. If it is an input block, it also contains `start` and `id`. We translate this as follows: - If it is a code block: simply return `text`. Note that we will not be able to interpret whether two code blocks should be separated. - If it is a text block: return `(** text *)`. -- If it is a hint block: return `(** HINT text *)`. **And implement in waterproof that the hint-closed text is immutable** +- If it is a hint block: return `(** HINT text *)`. **And implement in waterproof that the hint-closed text is immutable. Or, alternative: **`(** HINT (* hint-title *) text *)` - If it is an input block: - with `start == True`: return `(** INPUT-START *)` - with `start == False`: return `(** INPUT-END *)` **We could get away with only writing INPUT and inferring whether it is start or end, but this is more informative in .v files in my opinion** @@ -24,6 +24,10 @@ Unfortunately, it is easy to unintentionally write these. For example, the follo is syntactically `(Water *proof*) text`, which inadvertently contains a comment ending in Coq. Therefore, we will add a special character to remove any comment start or end non-code. The above sentence will become `(Water *proof*💧) text`. +## Code + +In-line Coq material (code) is encased in markdown with \`. In Coq, we can use \[ and \]. We can directly translate \` to \[ and \] alternatingly. However, as Coq code can be recursive, there can be an already existing \[ or \] inside code, and we do not want to translate this to \` as well. **So how should we do this?** + ## String literals Moreover, Coq string literals in comments *must* be completed in order to be parsed correctly. Strings begin and end with double quotes (`"`). To avoid an odd number of double quotes, we add an `"` to the end of `text` if it contains only one. From 68b8298cfcf6267c9f4130f89d3d1d308773a310 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Sat, 16 Apr 2022 21:43:49 +0200 Subject: [PATCH 07/30] Upload new specification from Jim en Jelle --- src/io/specification.md | 79 ++++++++++++++++++++++++++++++++--------- 1 file changed, 63 insertions(+), 16 deletions(-) diff --git a/src/io/specification.md b/src/io/specification.md index 07954c63..ddb0536d 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -1,21 +1,67 @@ # Importing/exporting waterproof notebooks from/to vernacular file We aim to make the exported .v files easy to read, and adhering to coqdoc format for nice coqdoc rendering. We are a bit constrained as we like *exact reproducibility*, though we will settle for approximate reproducibility for the benefit of readability of .v files. +## Waterproof notebooks and exercise sheets -## Block structure +Waterproof notebooks and exercise sheets are practically `.json` files, but have extensions `.wpn` and `.wpe` respectively. The files have two attributes, `exerciseSheet` and `blocks`. For a notebook, `exerciseSheet : false` and for an exercise sheet, `exerciseSheet : true`. +The blocks attribute is a sequence of dictionaries. Every element in the sequence contains: -Waterproof notebooks are made out of a collection of blocks, and each has one of the following types of block: text, code, input, and hint block. We translate these blocks according to their type. We choose to get rid of unnecessary metadata, and infer this when re-importing the blocks. -Concretely, a block in waterproof is an object containing a `type` and `text`. If it is an input block, it also contains `start` and `id`. We translate this as follows: -- If it is a code block: simply return `text`. Note that we will not be able to interpret whether two code blocks should be separated. -- If it is a text block: return `(** text *)`. -- If it is a hint block: return `(** HINT text *)`. **And implement in waterproof that the hint-closed text is immutable. Or, alternative: **`(** HINT (* hint-title *) text *)` +- a field `type`, which is one of: `text`, `code`, `input` or `hint`. +- a field `text`, which contains the content of the block +- a field `id`, which is present if and only if the field is an input block, which contains a unique identifier for the block +- a field `start`, which is present if and only if the field is an input block, which encodes whether this is the start or the end of an input block + +## Exporting to `.v` file + +We export a notebook or exercisesheet to a `.v` file as follows: + +- If it is a code block: simply return the content stored in the field `text`. Between the output of two consecutive code blocks, we add `(***)`. +- If it is a text block: return `(** convert_to_valid(text) *)`. +- If it is a hint block: return `(** convert_to_valid(text_before_first_)\n\nconvert_to_valid(text_after_first_)*)`. - If it is an input block: - with `start == True`: return `(** INPUT-START *)` - with `start == False`: return `(** INPUT-END *)` **We could get away with only writing INPUT and inferring whether it is start or end, but this is more informative in .v files in my opinion** +- Make (separate) settings whether $, %, and/or # occurring in hint or text blocks need to be doubled on export For re-importing, everything we encounter that is not in a `(**` and `*)` is a code block. Originally contiguous code blocks will become one large code blocks. To split these up, you can input an empty text block `(** *)` or even `(***)` (the latter is not rendered in coqdoc, while the former is rendered as an empty line). -## Unintentional comment start/end +## Importing to `.v` file + +- The (outer-layer) coqdoc comments `(** INPUT-START *)` and `(** INPUT-END *)` are mapped to blocks with type `input` +- Outer-layer coqdoc comments that somewhere contain `` are converted to hint blocks. +- Every other outmost-layer coqdoc comment gets assigned an input block type `text` with contents of the coqdoc comment. +- The `id` of the `n`th imported input block is assigned `input-n` +- Open input blocks get closed before a next input block is opened, additional closures of input blocks are ignored +- If no text is present before `` in open hint block, then add standard text: Click to open hint. +- Note: text is not stripped +- Make (separate) settings whether $, %, and/or # occurring in hint or text blocks need to be halved on import + +## Conversion to valid text + +Decision/aim: stay as close as possible to coqdoc notation in the json file. Only in rendering go to the markdown dialect. + +The function `convert_to_valid` performs the following actions: + +- Close string literal at the end of the markdown block (if one is open at the end) +- Close all open comments at the end of the markdown block +- Open comments at the beginning of the markdown block + +### Waterproof conversions: + +Convert in rendering (in the `render` function in `WpBlock.vue`) + +- `(*` to `(💧` and `*)` to `💧)`, where precedence goes from left to right. +- Header-*'s to #'s +- `##` and `##` both to `**` +- Consecutive `[` and `]` both to backticks. +- \_arbitrary text\_ to \*arbitrary text\* +- If markdown lists with '*' don't work: Coqdoc lists (with '-') to markdown lists (with '*') + +--- + +Old stuff: + +### Unintentional comment start/end Coq uses `(*` and `*)` to denote comment start and end. These can be used recursively. If they are in text and are exported inside a `(** *)`, it will interfere with the formatting. Unfortunately, it is easy to unintentionally write these. For example, the following waterproof text sentence: @@ -24,26 +70,27 @@ Unfortunately, it is easy to unintentionally write these. For example, the follo is syntactically `(Water *proof*) text`, which inadvertently contains a comment ending in Coq. Therefore, we will add a special character to remove any comment start or end non-code. The above sentence will become `(Water *proof*💧) text`. -## Code +TODO: maybe need to start enforcing matching of comments in Waterproof -In-line Coq material (code) is encased in markdown with \`. In Coq, we can use \[ and \]. We can directly translate \` to \[ and \] alternatingly. However, as Coq code can be recursive, there can be an already existing \[ or \] inside code, and we do not want to translate this to \` as well. **So how should we do this?** +### String literals -## String literals +In CoQ, if a string literal is opened in a comment, everything that follows after it until the string literal is closed is considered part of the string and has no further syntactic interpretation. -Moreover, Coq string literals in comments *must* be completed in order to be parsed correctly. Strings begin and end with double quotes (`"`). To avoid an odd number of double quotes, we add an `"` to the end of `text` if it contains only one. +Moreover, Coq string literals in comments *must* be completed in order to be parsed correctly. Strings begin and end with double quotes (`"`). To avoid an odd number of double quotes, we add an `"` to the end of the open comment in `text` if it contains an odd number of quotes. -## Using \#{1-6} +### Using \#{1-6} +TODO: in principle we can ignore(?) this and tackle it in the Vue representation of blocks. In waterproof (markdown) we may start text with `# `, `## `, ..., `###### ` to indicate various levels of headings, but in coqdoc we must use `* `, `** `, `**** `. Hence, we translate `#{1-4} ` at the start of a block to `*{1-4} ` and back to `#{1-4}` again. **If there is `#{5,6}` I don't know what to do yet**. -## Bold/italics +### Bold/italics In waterproof (markdown) we may use `**text**` and `*text*` to write bold/italics respectively. In coq, we can do emphasis (italics) with `_text_`. Bold is a bit harder, but we can use `##text##`. -## Coqdoc escape characters -To simply output the characters \$, % and # and escaping their escaping role in coqdoc, these characters are be doubled. In coqdoc, `$text$` would output text in latex math-mode. **However, this does not work for HTML-output, so it is quite useless.** +### Coqdoc escape characters +To simply output the characters $, % and # and escaping their escaping role in coqdoc, these characters are be doubled. In coqdoc, `$text$` would output text in latex math-mode. **However, this does not work for HTML-output, so it is quite useless.** It is a little bit of a problem, because stuff in # is simply discarded in latex output actually. https://coq.inria.fr/refman/using/tools/coqdoc.html#escaping-to-latex-and-html -## Notebook or exercise sheet? +### Notebook or exercise sheet? Always import as notebook. So previously exported exercise sheet can become notebook. From 691d53199cadd293f362c1d28bdf368503288d4d Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Sat, 16 Apr 2022 21:44:08 +0200 Subject: [PATCH 08/30] Implement render changes from specification --- src/editpage/components/blocks/WpBlock.vue | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/editpage/components/blocks/WpBlock.vue b/src/editpage/components/blocks/WpBlock.vue index 51cae78b..2ef0bf92 100644 --- a/src/editpage/components/blocks/WpBlock.vue +++ b/src/editpage/components/blocks/WpBlock.vue @@ -50,6 +50,15 @@ export default { }); // Replace coqdoc-style lists (-) with markdown lists (*) converted = converted.replace(/^([ ]*)- /gm, '$1* '); + // Remove coq-comment start & end + converted = converted.replace(/\(\*/g, '(💧'); + converted = converted.replace(/\*\)/g, '💧)'); + // Translate bold to md + converted = converted.replace(/#<\/?strong>#/g, '**'); + // Translate italics to md + converted = converted.replace(/ _/g, ' *'); + converted = converted.replace(/_ /g, '* '); + return md.render(converted); }, renderToSpan: function(text) { From 2c01c9cbc69c60dbc81475414403feb3c9d306a0 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Sat, 16 Apr 2022 22:38:04 +0200 Subject: [PATCH 09/30] Implement new import/export. Needs testcases! --- src/io/notebook.js | 122 ++++++++++++++++++++++++++++++++------------- 1 file changed, 88 insertions(+), 34 deletions(-) diff --git a/src/io/notebook.js b/src/io/notebook.js index 1552a624..9c4235f3 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -1,3 +1,6 @@ +import { Pass } from 'codemirror'; +import { assert, error } from 'console'; + const fs = require('fs'); const DEFAULT_BLACKLIST = [ @@ -556,66 +559,117 @@ function revertSafeCoqComment(text) { } /** - * Converts coq code to a notebook format - * This does not convert back any waterproof things and just puts all - * special comments in text blocks and the rest in code blocks. + * Importing from .v file according to specification.md * @param {String} coqCode the input code * @return {Array} the blocks from the code */ function coqToWp(coqCode) { - // eslint-disable-next-line max-len - const regexp = /\(\*\*\s(?(?:(?!\(\*)(?!\*\))[\s\S])*)\(\*(?(?:(?!\*\))[\s\S])*)\*\)\s\*\)(?(?:(?!\(\*\*\s)[\s\S])*)/g; - const blockMatches = [...coqCode.matchAll(regexp)]; const blocks = []; // return array let inInputField = false; - for (let i = 0; i < blockMatches.length; i++) { - const blockMatch = blockMatches[i]; - const data = blockMatch.groups.data.trim(); - const text = blockMatch.groups.text.trim(); - const code = blockMatch.groups.code.trim(); - const block = JSON.parse(data); - Notebook.setDefaultBlockState(block, inInputField); - if (block.type !== 'input') { - if (block.type !== 'code') { - block.text = revertSafeCoqComment(text); + let inputFieldId = 0; + let i = 0; + while (i < coqCode.length) { + let next = coqCode.indexOf('(**', i+3); + if (next === -1) { + next = coqCode.length; + } + const block = coqCode.substring(i, next).trim(); + const finalCommentCloseIndex = block.lastIndexOf('*)'); + if (finalCommentCloseIndex !== -1) { + const coqdoc = block.substring(3, finalCommentCloseIndex).trim(); + if (coqdoc === '') { + // The block could have been (***) or an empty text block + } else if (coqdoc === 'INPUT-START') { + // FIXME: Open input blocks get closed before a next input + // block is opened, additional closures of input blocks are ignored + assert(inInputField === false, + 'INPUT-START encountered, but input section has already started.' + ); + blocks.push({type: 'input', start: true, id: inputFieldId}); + inInputField = true; + } else if (coqdoc === 'INPUT-END') { + assert(inInputField === true, + 'INPUT-END encountered, but not in an input section.' + ); + blocks.push({type: 'input', start: false, id: inputFieldId}); + inInputField = false; + inputFieldId++; + } else if (coqdoc.indexOf('') !== -1) { + blocks.push({type: 'hint', text: coqdoc, }) } else { - block.text = code; + blocks.push({type: 'text', text: coqdoc}); } + } + let startCode; + if (finalCommentCloseIndex === -1) { + startCode = 0; } else { - inInputField = block.start; + startCode = finalCommentCloseIndex + 2; + } + const code = block.substring(startCode).trim(); + if (code !== -1) { + blocks.push({type: 'code', text: code}); } - blocks.push(block); + i = next; } - return blocks; } /** - * Convert blocks into coq parsable text, following specification.md + * Exporting to .v file according to specification.md * @param {[]} blocks the list of blocks * @return {string} the coq text */ function wpToCoq(blocks) { const blockStrings = []; + let prevBlockType = null; for (const block of blocks) { - let data = {type: block.type}; - let text = ''; - let code = ''; - if (block.type === 'input') { - data.start = block.start; - data.id = block.id; + if (block.type === 'code') { + if (prevBlockType === 'code') { + blockStrings.push('(***)'); + } + blockStrings.push(block.text); } - data = JSON.stringify(data); - if (block.type !== 'input') { - if (block.type === 'code') { - code = block.text; + else if (block.type === 'text') { + blockStrings.push('(** ' + convert_to_valid(block.text) + ' *)'); + } + else if (block.type === 'hint') { + const hint = block.text.split(''); + if (hint.length == 2) { + blockStrings.push( + '(** ' + convert_to_valid(hint[0].trim()) + '\n\n' + + convert_to_valid(hint[1].trim()) + ' *)' + ); + } else { + throw Error('Unexpected hint block: ' + hint.text) + } + } + else if (block.type === 'input') { + if (block.start) { + blockStrings.push('(** INPUT-START *)') } else { - text = createSafeCoqComment(block.text); + blockStrings.push('(** INPUT-END *)') } } - const blockString = '(** ' + text + '(* ' + data + ' *) *)' + code; - blockStrings.push(blockString); + + prevBlockType = block.type; } return blockStrings.join('\n'); } +function convert_to_valid(text) { + // Close string literal + let converted = text; + + // Close all open comments + // Open comments at the beginning + const opens = (converted.match(/\(\*/g) || []).length; + const closes = (converted.match(/\*\)/g) || []).length; + if (opens > closes) { + converted = converted + ' *)' * (opens - closes); + } else if (closes > opens) { + converted = (closes - opens) * '(* ' + converted; + } + // Seperate setting for doubling $, %, # +} + export {coqToWp, wpToCoq}; From 4d34a895bee41ab900bf9ac9a7f34ceff948e21a Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 09:14:20 +0200 Subject: [PATCH 10/30] Remove unused functions --- src/io/notebook.js | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/src/io/notebook.js b/src/io/notebook.js index 9c4235f3..a3ebcd75 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -536,28 +536,6 @@ class Notebook { export default Notebook; -/** - * Convert text to never break a Coq comment - * @param {string} text - * @return {string} - */ -function createSafeCoqComment(text) { - return text.replaceAll('*)', '*💧)') - .replaceAll('(*', '(💧*') - .replaceAll('"', '""'); -} - -/** - * Revert the changes made by createSafeCoqComment - * @param {string} text - * @return {string} - */ -function revertSafeCoqComment(text) { - return text.replaceAll('*💧)', '*)') - .replaceAll('(💧*', '(*') - .replaceAll('""', '"'); -} - /** * Importing from .v file according to specification.md * @param {String} coqCode the input code From 2e52e1c4cfe35c0189f36eaad0993ba5c6beeda8 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 10:45:44 +0200 Subject: [PATCH 11/30] translate bold --- wrapper/assistance/Tutorial.wpe | 40 ++++++++++++++++----------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/wrapper/assistance/Tutorial.wpe b/wrapper/assistance/Tutorial.wpe index 59b5531e..bbcf96ab 100644 --- a/wrapper/assistance/Tutorial.wpe +++ b/wrapper/assistance/Tutorial.wpe @@ -3,7 +3,7 @@ "blocks": [ { "type": "text", - "text": "# Tutorial: Getting used to Waterproof\n\nThis tutorial explains how to get started with Waterproof. The aim of Waterproof is to help learning how to prove mathematical statements.\n\nThis tutorial is in the form of an **exercise sheet** (sometimes we will call it a **notebook**). It is a mix of explanations and exercises in which you can try proving mathematical statements yourself. \n\nThe exercise sheet contains **text cells** (white background) and **code cells** (gray background). So far, we have been writing text, in text cells. But now we will introduce the first code cell.\n" + "text": "* Tutorial: Getting used to Waterproof\n\nThis tutorial explains how to get started with Waterproof. The aim of Waterproof is to help learning how to prove mathematical statements.\n\nThis tutorial is in the form of an ##exercise sheet## (sometimes we will call it a ##notebook##). It is a mix of explanations and exercises in which you can try proving mathematical statements yourself. \n\nThe exercise sheet contains ##text cells## (white background) and ##code cells## (gray background). So far, we have been writing text, in text cells. But now we will introduce the first code cell.\n" }, { "type": "code", @@ -15,11 +15,11 @@ }, { "type": "text", - "text": "\nWe recommend that while you read this notebook, you execute the code sentence-by-sentence by pressing **Alt + ↓** (on MacOS: **Option + ↓** or **⌥ + ↓**). (Alternatively, you can use the buttons on the left, but it is typically much faster to work with keyboard shortcuts.)" + "text": "\nWe recommend that while you read this notebook, you execute the code sentence-by-sentence by pressing ##Alt + ↓## (on MacOS: ##Option + ↓## or ##⌥ + ↓##). (Alternatively, you can use the buttons on the left, but it is typically much faster to work with keyboard shortcuts.)" }, { "type": "text", - "text": "* 1. Prove a lemma\n\nIn the following code cell, we introduce a **lemma**. We called the lemma **example_reflexivity**." + "text": "* 1. Prove a lemma\n\nIn the following code cell, we introduce a ##lemma##. We called the lemma ##example_reflexivity##." }, { "type": "code", @@ -35,11 +35,11 @@ }, { "type": "text", - "text": "\nExecute the code sentence after sentence (press **Alt + ↓** or **Option + ↓**), until a blue checkmark appears in place of the period after `Proof.`. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under **Proof progress** (either on the right of the screen, or down below) appeared what we need to show, namely `(0=0)`. We will often refer to this as the current **goal**." + "text": "\nExecute the code sentence after sentence (press ##Alt + ↓## or ##Option + ↓##), until a blue checkmark appears in place of the period after `Proof.`. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under ##Proof progress## (either on the right of the screen, or down below) appeared what we need to show, namely `(0=0)`. We will often refer to this as the current ##goal##." }, { "type": "text", - "text": "\nNext, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence `\"We conclude that (0=0).\"` and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as **applying a tactic.**" + "text": "\nNext, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence `\"We conclude that (0=0).\"` and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as ##applying a tactic.##" }, { "type": "code", @@ -47,7 +47,7 @@ }, { "type": "text", - "text": "\nExecute the above sentence, with **Alt + ↓**, until the checkmark appears after the sentence. Note how under proof progress it says `Done.`. The lemma is proved! We close the proof by writing `Qed.`." + "text": "\nExecute the above sentence, with ##Alt + ↓##, until the checkmark appears after the sentence. Note how under proof progress it says `Done.`. The lemma is proved! We close the proof by writing `Qed.`." }, { "type": "code", @@ -55,11 +55,11 @@ }, { "type": "text", - "text": "\n**HINT:** When writing `We conclude that (...)`, it is important that at the place of the dots you write the current goal (which you can see under **Proof progress**), and not another statement.\n\n**HINT:** If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in." + "text": "\n##HINT:## When writing `We conclude that (...)`, it is important that at the place of the dots you write the current goal (which you can see under ##Proof progress##), and not another statement.\n\n##HINT:## If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in." }, { "type": "text", - "text": "** Try it yourself: prove a lemma\n\nYou can now try this for yourself. We prepared a lemma below, that we named **exercise_reflexivity**." + "text": "** Try it yourself: prove a lemma\n\nYou can now try this for yourself. We prepared a lemma below, that we named ##exercise_reflexivity##." }, { "type": "code", @@ -67,7 +67,7 @@ }, { "type": "text", - "text": "The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing **Alt + c** (On MacOS: **Ctrl + c**), and add a text cell by pressing **Alt + t** (On MacOS: **Ctrl + t**).\n\nYou can also change the text that is already there between the blue brackets by clicking on it.\n\nBelow we already added one code cell, which says `Admitted.`. Executing that code cell (**Alt + ↓**), will also make the proof progress turn to `Done.` **However,** in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise.\n\nAfter you have found a proof, replace the `Admitted.` by `Qed.` (click on the code cell and change the sentence)." + "text": "The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing ##Alt + c## (On MacOS: ##Ctrl + c##), and add a text cell by pressing ##Alt + t## (On MacOS: ##Ctrl + t##).\n\nYou can also change the text that is already there between the blue brackets by clicking on it.\n\nBelow we already added one code cell, which says `Admitted.`. Executing that code cell (##Alt + ↓##), will also make the proof progress turn to `Done.` ##However,## in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise.\n\nAfter you have found a proof, replace the `Admitted.` by `Qed.` (click on the code cell and change the sentence)." }, { "type": "input", @@ -97,7 +97,7 @@ }, { "type": "text", - "text": "> **NOTE:** the notation $x : ℝ$ means $x$ is in $\\mathbb{R}$ (or more accurately, $x$ is of type $\\mathbb{R}$) may be unfamiliar to you, and you may be more familiar with the notation $x ∈ \\reals$. This difference is due to the fact that Waterproof is built on **type theory** and not on set theory. \n\n**HINT:** You can insert characters such as ℝ either from the symbol menu that opens when clicking on 'Σ' in the top right corner, or you can write '\\reals' until a menu pops up and press enter. Make sure that the code reads 'ℝ' and not '\\reals' itself. For many other unicode characters you can use a backslash command as well." + "text": "> ##NOTE:## the notation $x : ℝ$ means $x$ is in $\\mathbb{R}$ (or more accurately, $x$ is of type $\\mathbb{R}$) may be unfamiliar to you, and you may be more familiar with the notation $x ∈ \\reals$. This difference is due to the fact that Waterproof is built on ##type theory## and not on set theory. \n\n##HINT:## You can insert characters such as ℝ either from the symbol menu that opens when clicking on 'Σ' in the top right corner, or you can write '\\reals' until a menu pops up and press enter. Make sure that the code reads 'ℝ' and not '\\reals' itself. For many other unicode characters you can use a backslash command as well." }, { "type": "code", @@ -105,7 +105,7 @@ }, { "type": "text", - "text": "\nTo show a statement like \"for all $x : \\mathbb{R}$, ...\", you first need to take an arbitrary $x : \\mathbb{R}$, and then continue showing ... . We do this by writing and executing the following sentence, i.e. by applying the following **tactic**." + "text": "\nTo show a statement like \"for all $x : \\mathbb{R}$, ...\", you first need to take an arbitrary $x : \\mathbb{R}$, and then continue showing ... . We do this by writing and executing the following sentence, i.e. by applying the following ##tactic##." }, { "type": "code", @@ -129,7 +129,7 @@ }, { "type": "text", - "text": "\n**HINT:** If you would like to get a hint on what you need to do, you can write and execute the sentence `Help.`" + "text": "\n##HINT:## If you would like to get a hint on what you need to do, you can write and execute the sentence `Help.`" }, { "type": "code", @@ -137,7 +137,7 @@ }, { "type": "text", - "text": "\n\n**HINT:** We recommend that always after you write down a sentence, you immediately execute it (**Alt + ↓**)." + "text": "\n\n##HINT:## We recommend that always after you write down a sentence, you immediately execute it (##Alt + ↓##)." }, { "type": "input", @@ -159,7 +159,7 @@ }, { "type": "text", - "text": "* 3. Show *there-exists* statements: choose values\n\nIf you want to show that *there exists* $y : \\mathbb{R}$ such that $(\\dots)$, you need to **choose** a candidate for $y$, and continue showing $(\\dots)$ with your choice." + "text": "* 3. Show *there-exists* statements: choose values\n\nIf you want to show that *there exists* $y : \\mathbb{R}$ such that $(\\dots)$, you need to ##choose## a candidate for $y$, and continue showing $(\\dots)$ with your choice." }, { "type": "code", @@ -179,7 +179,7 @@ }, { "type": "text", - "text": "\n(In this particular case we could also have written `Choose y := 2`, but in general the brackets are important.)\n\nWe now need to show that (y<3) (see **Proof progress** after executing the previous sentence). We can record this for our own convenience." + "text": "\n(In this particular case we could also have written `Choose y := 2`, but in general the brackets are important.)\n\nWe now need to show that (y<3) (see ##Proof progress## after executing the previous sentence). We can record this for our own convenience." }, { "type": "code", @@ -319,7 +319,7 @@ }, { "type": "text", - "text": "\nIf you now execute the code up to previous sentence, you can see in the **Proof progress** that we need to show `a < 0 ⇒ -a > 0.` Remembering the rules for brackets, this means:" + "text": "\nIf you now execute the code up to previous sentence, you can see in the ##Proof progress## that we need to show `a < 0 ⇒ -a > 0.` Remembering the rules for brackets, this means:" }, { "type": "code", @@ -335,7 +335,7 @@ }, { "type": "text", - "text": "\nThe **name** of this assumption is in this case **a_lt_0**. What you are actually assuming is written after the colon, namely **a < 0**. Note how after executing the sentence, the assumption $a < 0$ is added under **Proof progress** with the name **a_lt_0**.\n\nWe finish the proof." + "text": "\nThe ##name## of this assumption is in this case ##a_lt_0##. What you are actually assuming is written after the colon, namely ##a < 0##. Note how after executing the sentence, the assumption $a < 0$ is added under ##Proof progress## with the name ##a_lt_0##.\n\nWe finish the proof." }, { "type": "code", @@ -381,7 +381,7 @@ }, { "type": "text", - "text": "\nNote how we used special notation for the chain of inequalities\n\n``\n(& Rmin ε 1 &≤ 1\n &< 2).\n``\n\nWe think of this statement that **and** `Rmin ε 1 ≤ 1` **and** `1 < 2`. \n\n\n**IMPORTANT**: Here are a few issues to pay attention to:\n- After opening the first parenthesis, you need to write a '&' sign.\n- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign.\n- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported." + "text": "\nNote how we used special notation for the chain of inequalities\n\n``\n(& Rmin ε 1 &≤ 1\n &< 2).\n``\n\nWe think of this statement that ##and## `Rmin ε 1 ≤ 1` ##and## `1 < 2`. \n\n\n##IMPORTANT##: Here are a few issues to pay attention to:\n- After opening the first parenthesis, you need to write a '&' sign.\n- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign.\n- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported." }, { "type": "text", @@ -539,7 +539,7 @@ }, { "type": "text", - "text": "We can now **use** the statement that we called `del_cond` with $δ = 1/2$. We can do this by substituting $\\delta = 1/2$ as follows." + "text": "We can now ##use## the statement that we called `del_cond` with $δ = 1/2$. We can do this by substituting $\\delta = 1/2$ as follows." }, { "type": "code", @@ -581,7 +581,7 @@ }, { "type": "text", - "text": "* 10. Use a *there-exists* statement\n\nIn this example we show how to **use** a there-exists statement (when you know it holds)." + "text": "* 10. Use a *there-exists* statement\n\nIn this example we show how to ##use## a there-exists statement (when you know it holds)." }, { "type": "code", From 7c9926e5ec9c07c26c881bfef087cc46d1e04bce Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 10:48:52 +0200 Subject: [PATCH 12/30] translate italics --- wrapper/assistance/Tutorial.wpe | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/wrapper/assistance/Tutorial.wpe b/wrapper/assistance/Tutorial.wpe index bbcf96ab..44061d63 100644 --- a/wrapper/assistance/Tutorial.wpe +++ b/wrapper/assistance/Tutorial.wpe @@ -11,7 +11,7 @@ }, { "type": "text", - "text": "The code consists of several *sentences*. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." + "text": "The code consists of several _sentences_. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." }, { "type": "text", @@ -497,7 +497,7 @@ }, { "type": "text", - "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called `Rmax_r`.\n\n```\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n```\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n```\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n (* proof of claim *)\n}\n```" + "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called `Rmax_r`.\n\n```\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n```\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n```\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n ( _proof of claim_ )\n}\n```" }, { "type": "text", @@ -527,7 +527,7 @@ }, { "type": "text", - "text": "* 9. Use a *for-all* statement\n\nA special case of the above is when you would like to *use* a for-all statement, as in the example below." + "text": "* 9. Use a _for-all_ statement\n\nA special case of the above is when you would like to _use_ a for-all statement, as in the example below." }, { "type": "code", @@ -581,7 +581,7 @@ }, { "type": "text", - "text": "* 10. Use a *there-exists* statement\n\nIn this example we show how to ##use## a there-exists statement (when you know it holds)." + "text": "* 10. Use a _there-exists_ statement\n\nIn this example we show how to ##use## a there-exists statement (when you know it holds)." }, { "type": "code", @@ -605,7 +605,7 @@ }, { "type": "text", - "text": "** Try it yourself: use a *there-exists* statement" + "text": "** Try it yourself: use a _there-exists_ statement" }, { "type": "code", From 14545e29a5fb55a426fdcb3d6ffdba53cc39ecd1 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 10:50:00 +0200 Subject: [PATCH 13/30] Improved italics translation to match coqdoc --- src/editpage/components/blocks/WpBlock.vue | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/editpage/components/blocks/WpBlock.vue b/src/editpage/components/blocks/WpBlock.vue index 2ef0bf92..21657624 100644 --- a/src/editpage/components/blocks/WpBlock.vue +++ b/src/editpage/components/blocks/WpBlock.vue @@ -56,8 +56,8 @@ export default { // Translate bold to md converted = converted.replace(/#<\/?strong>#/g, '**'); // Translate italics to md - converted = converted.replace(/ _/g, ' *'); - converted = converted.replace(/_ /g, '* '); + converted = converted.replace(/[\s*]_/g, ' *'); + converted = converted.replace(/_[\s*]/g, '* '); return md.render(converted); }, From 589113cb6b587a551049da1a8506fabf9b2b8c7b Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 10:52:44 +0200 Subject: [PATCH 14/30] improve italics translation --- src/editpage/components/blocks/WpBlock.vue | 4 ++-- src/io/specification.md | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/editpage/components/blocks/WpBlock.vue b/src/editpage/components/blocks/WpBlock.vue index 21657624..3428fdce 100644 --- a/src/editpage/components/blocks/WpBlock.vue +++ b/src/editpage/components/blocks/WpBlock.vue @@ -56,8 +56,8 @@ export default { // Translate bold to md converted = converted.replace(/#<\/?strong>#/g, '**'); // Translate italics to md - converted = converted.replace(/[\s*]_/g, ' *'); - converted = converted.replace(/_[\s*]/g, '* '); + converted = converted.replace(/[\s]_/g, ' *'); + converted = converted.replace(/_[\s.,!?]/g, '* '); return md.render(converted); }, diff --git a/src/io/specification.md b/src/io/specification.md index ddb0536d..32d2b660 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -54,7 +54,7 @@ Convert in rendering (in the `render` function in `WpBlock.vue`) - Header-*'s to #'s - `##` and `##` both to `**` - Consecutive `[` and `]` both to backticks. -- \_arbitrary text\_ to \*arbitrary text\* +- \_arbitrary text\_ to \*arbitrary text\* if \_ preceded by a whitespace or followed by a whitespace or punctuation. - If markdown lists with '*' don't work: Coqdoc lists (with '-') to markdown lists (with '*') --- From faebaf05513f29ee7ae7343ae62f27418bb9eeda Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 10:57:41 +0200 Subject: [PATCH 15/30] translate code --- src/editpage/components/blocks/WpBlock.vue | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/editpage/components/blocks/WpBlock.vue b/src/editpage/components/blocks/WpBlock.vue index 3428fdce..89e77327 100644 --- a/src/editpage/components/blocks/WpBlock.vue +++ b/src/editpage/components/blocks/WpBlock.vue @@ -53,6 +53,9 @@ export default { // Remove coq-comment start & end converted = converted.replace(/\(\*/g, '(💧'); converted = converted.replace(/\*\)/g, '💧)'); + // Translate code + converted = converted.replace(/\[/g, '`'); + converted = converted.replace(/\]/g, '`'); // Translate bold to md converted = converted.replace(/#<\/?strong>#/g, '**'); // Translate italics to md From 7bee2e9a48cb4683fc89edaf80bbc55844f04579 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 11:04:04 +0200 Subject: [PATCH 16/30] Translate single backticks to [ and ] --- wrapper/assistance/Tutorial.wpe | 58 ++++++++++++++++----------------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/wrapper/assistance/Tutorial.wpe b/wrapper/assistance/Tutorial.wpe index 44061d63..54b5eaaf 100644 --- a/wrapper/assistance/Tutorial.wpe +++ b/wrapper/assistance/Tutorial.wpe @@ -11,7 +11,7 @@ }, { "type": "text", - "text": "The code consists of several _sentences_. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." + "text": "The code consists of several _sentences_ . Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." }, { "type": "text", @@ -27,7 +27,7 @@ }, { "type": "text", - "text": "\nWe will now prove the lemma. We start the proof by writing the sentence `\"Proof.\"` in a code cell." + "text": "\nWe will now prove the lemma. We start the proof by writing the sentence [\"Proof.\"] in a code cell." }, { "type": "code", @@ -35,11 +35,11 @@ }, { "type": "text", - "text": "\nExecute the code sentence after sentence (press ##Alt + ↓## or ##Option + ↓##), until a blue checkmark appears in place of the period after `Proof.`. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under ##Proof progress## (either on the right of the screen, or down below) appeared what we need to show, namely `(0=0)`. We will often refer to this as the current ##goal##." + "text": "\nExecute the code sentence after sentence (press ##Alt + ↓## or ##Option + ↓##), until a blue checkmark appears in place of the period after [Proof.]. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under ##Proof progress## (either on the right of the screen, or down below) appeared what we need to show, namely [(0=0)]. We will often refer to this as the current ##goal##." }, { "type": "text", - "text": "\nNext, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence `\"We conclude that (0=0).\"` and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as ##applying a tactic.##" + "text": "\nNext, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence [\"We conclude that (0=0).\"] and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as ##applying a tactic.##" }, { "type": "code", @@ -47,7 +47,7 @@ }, { "type": "text", - "text": "\nExecute the above sentence, with ##Alt + ↓##, until the checkmark appears after the sentence. Note how under proof progress it says `Done.`. The lemma is proved! We close the proof by writing `Qed.`." + "text": "\nExecute the above sentence, with ##Alt + ↓##, until the checkmark appears after the sentence. Note how under proof progress it says [Done.]. The lemma is proved! We close the proof by writing [Qed.]." }, { "type": "code", @@ -55,7 +55,7 @@ }, { "type": "text", - "text": "\n##HINT:## When writing `We conclude that (...)`, it is important that at the place of the dots you write the current goal (which you can see under ##Proof progress##), and not another statement.\n\n##HINT:## If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in." + "text": "\n##HINT:## When writing [We conclude that (...)], it is important that at the place of the dots you write the current goal (which you can see under ##Proof progress##), and not another statement.\n\n##HINT:## If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in." }, { "type": "text", @@ -67,7 +67,7 @@ }, { "type": "text", - "text": "The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing ##Alt + c## (On MacOS: ##Ctrl + c##), and add a text cell by pressing ##Alt + t## (On MacOS: ##Ctrl + t##).\n\nYou can also change the text that is already there between the blue brackets by clicking on it.\n\nBelow we already added one code cell, which says `Admitted.`. Executing that code cell (##Alt + ↓##), will also make the proof progress turn to `Done.` ##However,## in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise.\n\nAfter you have found a proof, replace the `Admitted.` by `Qed.` (click on the code cell and change the sentence)." + "text": "The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing ##Alt + c## (On MacOS: ##Ctrl + c##), and add a text cell by pressing ##Alt + t## (On MacOS: ##Ctrl + t##).\n\nYou can also change the text that is already there between the blue brackets by clicking on it.\n\nBelow we already added one code cell, which says [Admitted.]. Executing that code cell (##Alt + ↓##), will also make the proof progress turn to [Done.] ##However,## in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise.\n\nAfter you have found a proof, replace the [Admitted.] by [Qed.] (click on the code cell and change the sentence)." }, { "type": "input", @@ -76,7 +76,7 @@ }, { "type": "text", - "text": "Write your solution here, then change the `Admitted.` below to `Qed.`." + "text": "Write your solution here, then change the [Admitted.] below to [Qed.]." }, { "type": "code", @@ -129,7 +129,7 @@ }, { "type": "text", - "text": "\n##HINT:## If you would like to get a hint on what you need to do, you can write and execute the sentence `Help.`" + "text": "\n##HINT:## If you would like to get a hint on what you need to do, you can write and execute the sentence [Help.]" }, { "type": "code", @@ -146,7 +146,7 @@ }, { "type": "text", - "text": "Write your solution here. After you have found a proof, remember to change the `Admitted.` below to `Qed.`." + "text": "Write your solution here. After you have found a proof, remember to change the [Admitted.] below to [Qed.]." }, { "type": "code", @@ -171,7 +171,7 @@ }, { "type": "text", - "text": "\nWe first choose $y:=2$ by using the tactic `Choose y := ((* value *)).`." + "text": "\nWe first choose $y:=2$ by using the tactic [Choose y := ((* value *)).]." }, { "type": "code", @@ -179,7 +179,7 @@ }, { "type": "text", - "text": "\n(In this particular case we could also have written `Choose y := 2`, but in general the brackets are important.)\n\nWe now need to show that (y<3) (see ##Proof progress## after executing the previous sentence). We can record this for our own convenience." + "text": "\n(In this particular case we could also have written [Choose y := 2], but in general the brackets are important.)\n\nWe now need to show that (y<3) (see ##Proof progress## after executing the previous sentence). We can record this for our own convenience." }, { "type": "code", @@ -187,7 +187,7 @@ }, { "type": "text", - "text": "\nIn other words, we need to show that ($2 < 3$). We can also use the `We need to show that ` tactic to slightly reformulate the goal." + "text": "\nIn other words, we need to show that ($2 < 3$). We can also use the [We need to show that] tactic to slightly reformulate the goal." }, { "type": "code", @@ -319,7 +319,7 @@ }, { "type": "text", - "text": "\nIf you now execute the code up to previous sentence, you can see in the ##Proof progress## that we need to show `a < 0 ⇒ -a > 0.` Remembering the rules for brackets, this means:" + "text": "\nIf you now execute the code up to previous sentence, you can see in the ##Proof progress## that we need to show [a < 0 ⇒ -a > 0.] Remembering the rules for brackets, this means:" }, { "type": "code", @@ -369,7 +369,7 @@ }, { "type": "text", - "text": "* 6. Chains of (in)equalities\n\nAs a last step of a proof in Analysis, we often have a chain of (in)equalities. Consider for instance a case in which we would like to show that for all $ε : \\mathbb{R}$, if $ε > 0$ then $\\min(\\epsilon, 1) ≤ 2$. \n\nHere are the statement and a possible proof in Waterproof. Note that we need to write `Rmin x y` for the minimum of two real numbers $x$ and $y$." + "text": "* 6. Chains of (in)equalities\n\nAs a last step of a proof in Analysis, we often have a chain of (in)equalities. Consider for instance a case in which we would like to show that for all $ε : \\mathbb{R}$, if $ε > 0$ then $\\min(\\epsilon, 1) ≤ 2$. \n\nHere are the statement and a possible proof in Waterproof. Note that we need to write [Rmin x y] for the minimum of two real numbers $x$ and $y$." }, { "type": "code", @@ -381,7 +381,7 @@ }, { "type": "text", - "text": "\nNote how we used special notation for the chain of inequalities\n\n``\n(& Rmin ε 1 &≤ 1\n &< 2).\n``\n\nWe think of this statement that ##and## `Rmin ε 1 ≤ 1` ##and## `1 < 2`. \n\n\n##IMPORTANT##: Here are a few issues to pay attention to:\n- After opening the first parenthesis, you need to write a '&' sign.\n- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign.\n- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported." + "text": "\nNote how we used special notation for the chain of inequalities\n\n``\n(& Rmin ε 1 &≤ 1\n &< 2).\n``\n\nWe think of this statement that ##and## [Rmin ε 1 ≤ 1] ##and## [1 < 2]. \n\n\n##IMPORTANT##: Here are a few issues to pay attention to:\n- After opening the first parenthesis, you need to write a '&' sign.\n- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign.\n- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported." }, { "type": "text", @@ -469,7 +469,7 @@ }, { "type": "text", - "text": "* 8. Forward reasoning in smaller steps\n\nSometimes, the step to what you need to show is too big for Waterproof to find a proof. In that case, the tactic `We conclude that (...).` will not find a proof. Then it often helps to make smaller steps.\n\nHere is an example." + "text": "* 8. Forward reasoning in smaller steps\n\nSometimes, the step to what you need to show is too big for Waterproof to find a proof. In that case, the tactic [We conclude that (...).] will not find a proof. Then it often helps to make smaller steps.\n\nHere is an example." }, { "type": "code", @@ -481,7 +481,7 @@ }, { "type": "text", - "text": "\nWe now make an intermediate step. We let Waterproof automatically show that `(Rmax ε 1 ≥ 1)`, and we call that statement `Rmax_gt_1`." + "text": "\nWe now make an intermediate step. We let Waterproof automatically show that [(Rmax ε 1 ≥ 1)], and we call that statement [Rmax_gt_1]." }, { "type": "code", @@ -497,7 +497,7 @@ }, { "type": "text", - "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called `Rmax_r`.\n\n```\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n```\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n```\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n ( _proof of claim_ )\n}\n```" + "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r].\n\n```\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n```\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n```\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n ( _proof of claim_ )\n}\n```" }, { "type": "text", @@ -539,7 +539,7 @@ }, { "type": "text", - "text": "We can now ##use## the statement that we called `del_cond` with $δ = 1/2$. We can do this by substituting $\\delta = 1/2$ as follows." + "text": "We can now ##use## the statement that we called [del_cond] with $δ = 1/2$. We can do this by substituting $\\delta = 1/2$ as follows." }, { "type": "code", @@ -547,7 +547,7 @@ }, { "type": "text", - "text": "Similarly, we can use the statement that we called `eps_cond`. We can also indicate explicitly that we choose $ε = 1/2$ in the statement by writing `By (eps_cond (1/2)) ...` as in" + "text": "Similarly, we can use the statement that we called [eps_cond]. We can also indicate explicitly that we choose $ε = 1/2$ in the statement by writing [By (eps_cond (1/2)) ...] as in" }, { "type": "code", @@ -667,7 +667,7 @@ }, { "type": "text", - "text": "\nInstead of writing `Contradiction.` you can also write `↯.`. You can get the symbol `↯` with the backslash-command `\\contradiction`." + "text": "\nInstead of writing [Contradiction.] you can also write [↯.]. You can get the symbol [↯] with the backslash-command [\\contradiction]." }, { "type": "text", @@ -729,7 +729,7 @@ }, { "type": "hint", - "text": "Click to open hint.\n\nDistinguish between cases `x < y` and `x ≥ y`." + "text": "Click to open hint.\n\nDistinguish between cases [x < y] and [x ≥ y]." }, { "type": "input", @@ -771,7 +771,7 @@ }, { "type": "text", - "text": "\nNow the proof splits into two parts, one for each statement. We need to indicate these two parts using bullet points. They can be indicated by any of `-`, `+`, `*`, `--` etc.. You can use a bulleted list inside of a bulleted list." + "text": "\nNow the proof splits into two parts, one for each statement. We need to indicate these two parts using bullet points. They can be indicated by any of [-], [+], [*], [--] etc.. You can use a bulleted list inside of a bulleted list." }, { "type": "code", @@ -859,7 +859,7 @@ }, { "type": "text", - "text": "* 15. Proof by induction\n\nThe following example shows how one could use mathematical induction to show a statement of the form\n\n $$∀ k : ℕ, ... $$\n\nNote that Waterproof will usually interpret any statement such as an inequality `n(k +1 ) > n k` as a statement comparing real numbers, while in this exercise we need statements that compare natural numbers. To indicate this, we have to write `(n (k+1) > n k)%nat` instead." + "text": "* 15. Proof by induction\n\nThe following example shows how one could use mathematical induction to show a statement of the form\n\n $$∀ k : ℕ, ... $$\n\nNote that Waterproof will usually interpret any statement such as an inequality [n(k +1 ) > n k] as a statement comparing real numbers, while in this exercise we need statements that compare natural numbers. To indicate this, we have to write [(n (k+1) > n k)%nat] instead." }, { "type": "code", @@ -905,7 +905,7 @@ }, { "type": "text", - "text": "* 16. Expand definitions\n\nIt happens that you need to use a definition of some object in Waterproof, for instance the definition of a function. Here is the definition of a function called `square`." + "text": "* 16. Expand definitions\n\nIt happens that you need to use a definition of some object in Waterproof, for instance the definition of a function. Here is the definition of a function called [square]." }, { "type": "code", @@ -925,7 +925,7 @@ }, { "type": "text", - "text": "At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing `We need to show that (x^2 ≥ 0).`, or we could write \n\n```\nWe conclude that\n (& square x &= x^2\n &≥ 0). \n```\nHowever these options aren't available if you do not know the definition of `square`. In that case you could write" + "text": "At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing [We need to show that (x^2 ≥ 0).], or we could write \n\n```\nWe conclude that\n (& square x &= x^2\n &≥ 0). \n```\nHowever these options aren't available if you do not know the definition of [square]. In that case you could write" }, { "type": "code", @@ -933,7 +933,7 @@ }, { "type": "text", - "text": "\nNow Waterproof has expanded the definition of `square` in the goal. It is always important to keep the proof readable, so that's why Waterproof asks you now to also reformulate the goal." + "text": "\nNow Waterproof has expanded the definition of [square] in the goal. It is always important to keep the proof readable, so that's why Waterproof asks you now to also reformulate the goal." }, { "type": "code", @@ -941,7 +941,7 @@ }, { "type": "text", - "text": "You can also expand the definition in a hypothesis. For instance,\n```\nExpand the definition of square in H.\n```\nwould expand the definition of `square` in the hypothesis with the name `H`." + "text": "You can also expand the definition in a hypothesis. For instance,\n```\nExpand the definition of square in H.\n```\nwould expand the definition of [square] in the hypothesis with the name [H]." }, { "type": "text", From 5bab58cefc4b8053fa5bcab3424e5357a4d49c83 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 11:45:42 +0200 Subject: [PATCH 17/30] preformatted code with [[ and ]] (``` in markdown) --- src/editpage/components/blocks/WpBlock.vue | 5 ++++- src/io/specification.md | 1 + wrapper/assistance/Tutorial.wpe | 8 ++++---- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/editpage/components/blocks/WpBlock.vue b/src/editpage/components/blocks/WpBlock.vue index 89e77327..ae7d6b0d 100644 --- a/src/editpage/components/blocks/WpBlock.vue +++ b/src/editpage/components/blocks/WpBlock.vue @@ -54,6 +54,8 @@ export default { converted = converted.replace(/\(\*/g, '(💧'); converted = converted.replace(/\*\)/g, '💧)'); // Translate code + converted = converted.replace(/\[\[/g, '```'); + converted = converted.replace(/\]\]/g, '```'); converted = converted.replace(/\[/g, '`'); converted = converted.replace(/\]/g, '`'); // Translate bold to md @@ -62,7 +64,8 @@ export default { converted = converted.replace(/[\s]_/g, ' *'); converted = converted.replace(/_[\s.,!?]/g, '* '); - return md.render(converted); + converted = md.render(converted); + return converted; }, renderToSpan: function(text) { let htmlString = this.render(text); diff --git a/src/io/specification.md b/src/io/specification.md index 32d2b660..7eb84a99 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -53,6 +53,7 @@ Convert in rendering (in the `render` function in `WpBlock.vue`) - `(*` to `(💧` and `*)` to `💧)`, where precedence goes from left to right. - Header-*'s to #'s - `##` and `##` both to `**` +- Consecutive `[[` and `]]` both to triple backticks. (TODO figure out how to color this the same) - Consecutive `[` and `]` both to backticks. - \_arbitrary text\_ to \*arbitrary text\* if \_ preceded by a whitespace or followed by a whitespace or punctuation. - If markdown lists with '*' don't work: Coqdoc lists (with '-') to markdown lists (with '*') diff --git a/wrapper/assistance/Tutorial.wpe b/wrapper/assistance/Tutorial.wpe index 54b5eaaf..98fe9edf 100644 --- a/wrapper/assistance/Tutorial.wpe +++ b/wrapper/assistance/Tutorial.wpe @@ -393,7 +393,7 @@ }, { "type": "hint", - "text": "Click to open hint.\n\nAt the end of your proof, use the following chain of inequalities \n\n```\nRmin (ε / 2) 1 ≤ ε / 2 < ε\n```\n\nbut pay attention to the issues mentioned above: in particular use the '&' sign at the appropriate places." + "text": "Click to open hint.\n\nAt the end of your proof, use the following chain of inequalities \n\n[[\nRmin (ε / 2) 1 ≤ ε / 2 < ε\n]]\n\nbut pay attention to the issues mentioned above: in particular use the '&' sign at the appropriate places." }, { "type": "input", @@ -497,7 +497,7 @@ }, { "type": "text", - "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r].\n\n```\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n```\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n```\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n ( _proof of claim_ )\n}\n```" + "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r].\n\n[[\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n]]\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n[[\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n ( _proof of claim_ )\n}\n]]" }, { "type": "text", @@ -925,7 +925,7 @@ }, { "type": "text", - "text": "At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing [We need to show that (x^2 ≥ 0).], or we could write \n\n```\nWe conclude that\n (& square x &= x^2\n &≥ 0). \n```\nHowever these options aren't available if you do not know the definition of [square]. In that case you could write" + "text": "At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing [We need to show that (x^2 ≥ 0).], or we could write \n\n[[\nWe conclude that\n (& square x &= x^2\n &≥ 0). \n]]\nHowever these options aren't available if you do not know the definition of [square]. In that case you could write" }, { "type": "code", @@ -941,7 +941,7 @@ }, { "type": "text", - "text": "You can also expand the definition in a hypothesis. For instance,\n```\nExpand the definition of square in H.\n```\nwould expand the definition of [square] in the hypothesis with the name [H]." + "text": "You can also expand the definition in a hypothesis. For instance,\n[[\nExpand the definition of square in H.\n]]\nwould expand the definition of [square] in the hypothesis with the name [H]." }, { "type": "text", From 16e2533921b172bfedfd1c5484aeee4770076a7e Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 11:52:04 +0200 Subject: [PATCH 18/30] lint --- src/io/notebook.js | 55 ++++++++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 26 deletions(-) diff --git a/src/io/notebook.js b/src/io/notebook.js index a3ebcd75..39545b31 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -1,5 +1,4 @@ -import { Pass } from 'codemirror'; -import { assert, error } from 'console'; +import {assert} from 'console'; const fs = require('fs'); @@ -560,20 +559,22 @@ function coqToWp(coqCode) { } else if (coqdoc === 'INPUT-START') { // FIXME: Open input blocks get closed before a next input // block is opened, additional closures of input blocks are ignored - assert(inInputField === false, - 'INPUT-START encountered, but input section has already started.' + assert( + inInputField === false, + 'INPUT-START encountered, but input section has already started.' ); blocks.push({type: 'input', start: true, id: inputFieldId}); inInputField = true; } else if (coqdoc === 'INPUT-END') { - assert(inInputField === true, - 'INPUT-END encountered, but not in an input section.' + assert( + inInputField === true, + 'INPUT-END encountered, but not in an input section.' ); blocks.push({type: 'input', start: false, id: inputFieldId}); inInputField = false; inputFieldId++; } else if (coqdoc.indexOf('') !== -1) { - blocks.push({type: 'hint', text: coqdoc, }) + blocks.push({type: 'hint', text: coqdoc}); } else { blocks.push({type: 'text', text: coqdoc}); } @@ -590,6 +591,7 @@ function coqToWp(coqCode) { } i = next; } + return blocks; } /** @@ -606,38 +608,39 @@ function wpToCoq(blocks) { blockStrings.push('(***)'); } blockStrings.push(block.text); - } - else if (block.type === 'text') { - blockStrings.push('(** ' + convert_to_valid(block.text) + ' *)'); - } - else if (block.type === 'hint') { - const hint = block.text.split(''); - if (hint.length == 2) { + } else if (block.type === 'text') { + blockStrings.push('(** ' + convertToValid(block.text) + ' *)'); + } else if (block.type === 'hint') { + const hint = block.text.split(''); + if (hint.length == 2) { blockStrings.push( - '(** ' + convert_to_valid(hint[0].trim()) + '\n\n' - + convert_to_valid(hint[1].trim()) + ' *)' + '(** ' + convertToValid(hint[0].trim()) + '\n\n' + + convertToValid(hint[1].trim()) + ' *)' ); - } else { - throw Error('Unexpected hint block: ' + hint.text) - } - } - else if (block.type === 'input') { + } else { + throw Error('Unexpected hint block: ' + hint.text); + } + } else if (block.type === 'input') { if (block.start) { - blockStrings.push('(** INPUT-START *)') + blockStrings.push('(** INPUT-START *)'); } else { - blockStrings.push('(** INPUT-END *)') + blockStrings.push('(** INPUT-END *)'); } } - + prevBlockType = block.type; } return blockStrings.join('\n'); } -function convert_to_valid(text) { +/** + * Convert a block's text to something that is valid. + * @param {string} text + */ +function convertToValid(text) { // Close string literal let converted = text; - + // Close all open comments // Open comments at the beginning const opens = (converted.match(/\(\*/g) || []).length; From 126482f1448be5147e0e3b621b811d00c92e9e07 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 12:05:25 +0200 Subject: [PATCH 19/30] Improved italics translation further --- src/editpage/components/blocks/WpBlock.vue | 4 ++-- src/io/notebook.js | 5 +++++ src/io/specification.md | 2 +- wrapper/assistance/Tutorial.wpe | 4 ++-- 4 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/editpage/components/blocks/WpBlock.vue b/src/editpage/components/blocks/WpBlock.vue index ae7d6b0d..14e8093f 100644 --- a/src/editpage/components/blocks/WpBlock.vue +++ b/src/editpage/components/blocks/WpBlock.vue @@ -61,8 +61,8 @@ export default { // Translate bold to md converted = converted.replace(/#<\/?strong>#/g, '**'); // Translate italics to md - converted = converted.replace(/[\s]_/g, ' *'); - converted = converted.replace(/_[\s.,!?]/g, '* '); + converted = converted.replace(/\W_/g, ' *'); + converted = converted.replace(/_\W/g, '* '); converted = md.render(converted); return converted; diff --git a/src/io/notebook.js b/src/io/notebook.js index 39545b31..7eb09f00 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -626,6 +626,8 @@ function wpToCoq(blocks) { } else { blockStrings.push('(** INPUT-END *)'); } + } else { + throw Error('Can not interpret block type ' + block.type); } prevBlockType = block.type; @@ -636,6 +638,7 @@ function wpToCoq(blocks) { /** * Convert a block's text to something that is valid. * @param {string} text + * @return {string} converted text */ function convertToValid(text) { // Close string literal @@ -651,6 +654,8 @@ function convertToValid(text) { converted = (closes - opens) * '(* ' + converted; } // Seperate setting for doubling $, %, # + + return converted; } export {coqToWp, wpToCoq}; diff --git a/src/io/specification.md b/src/io/specification.md index 7eb84a99..469fde32 100644 --- a/src/io/specification.md +++ b/src/io/specification.md @@ -55,7 +55,7 @@ Convert in rendering (in the `render` function in `WpBlock.vue`) - `##` and `##` both to `**` - Consecutive `[[` and `]]` both to triple backticks. (TODO figure out how to color this the same) - Consecutive `[` and `]` both to backticks. -- \_arbitrary text\_ to \*arbitrary text\* if \_ preceded by a whitespace or followed by a whitespace or punctuation. +- \_arbitrary text\_ to \*arbitrary text\* if \_ preceded or followed by an alphanumeric or underscore. - If markdown lists with '*' don't work: Coqdoc lists (with '-') to markdown lists (with '*') --- diff --git a/wrapper/assistance/Tutorial.wpe b/wrapper/assistance/Tutorial.wpe index 98fe9edf..62769ffc 100644 --- a/wrapper/assistance/Tutorial.wpe +++ b/wrapper/assistance/Tutorial.wpe @@ -11,7 +11,7 @@ }, { "type": "text", - "text": "The code consists of several _sentences_ . Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." + "text": "The code consists of several _sentences_. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." }, { "type": "text", @@ -497,7 +497,7 @@ }, { "type": "text", - "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r].\n\n[[\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n]]\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n[[\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n ( _proof of claim_ )\n}\n]]" + "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r].\n\n[[\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n]]\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n[[\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n (* proof of claim *)\n}\n]]" }, { "type": "text", From cd6f81858a467fe16e866b40b06d22d9eb3f814f Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 12:44:02 +0200 Subject: [PATCH 20/30] default block state added to blocks --- src/io/notebook.js | 67 ++++++++++++++++++++++++++++------------------ 1 file changed, 41 insertions(+), 26 deletions(-) diff --git a/src/io/notebook.js b/src/io/notebook.js index 7eb09f00..b5a724aa 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -550,33 +550,46 @@ function coqToWp(coqCode) { if (next === -1) { next = coqCode.length; } - const block = coqCode.substring(i, next).trim(); - const finalCommentCloseIndex = block.lastIndexOf('*)'); + const blockContent = coqCode.substring(i, next).trim(); + const finalCommentCloseIndex = blockContent.lastIndexOf('*)'); if (finalCommentCloseIndex !== -1) { - const coqdoc = block.substring(3, finalCommentCloseIndex).trim(); + const coqdoc = blockContent.substring(3, finalCommentCloseIndex).trim(); if (coqdoc === '') { - // The block could have been (***) or an empty text block - } else if (coqdoc === 'INPUT-START') { - // FIXME: Open input blocks get closed before a next input - // block is opened, additional closures of input blocks are ignored - assert( - inInputField === false, - 'INPUT-START encountered, but input section has already started.' - ); - blocks.push({type: 'input', start: true, id: inputFieldId}); - inInputField = true; - } else if (coqdoc === 'INPUT-END') { - assert( - inInputField === true, - 'INPUT-END encountered, but not in an input section.' - ); - blocks.push({type: 'input', start: false, id: inputFieldId}); - inInputField = false; - inputFieldId++; - } else if (coqdoc.indexOf('') !== -1) { - blocks.push({type: 'hint', text: coqdoc}); + // The block could have been (***) or an empty text block. We don't add + // a block in that case. } else { - blocks.push({type: 'text', text: coqdoc}); + const block = {}; + if (coqdoc === 'INPUT-START') { + // FIXME: Open input blocks get closed before a next input + // block is opened, additional closures of input blocks are ignored + assert( + inInputField === false, + 'INPUT-START encountered, but input section has already started.' + ); + block.type = 'input'; + block.start = true; + block.id = inputFieldId; + inInputField = true; + } else if (coqdoc === 'INPUT-END') { + assert( + inInputField === true, + 'INPUT-END encountered, but not in an input section.' + ); + block.type = 'input'; + block.start = false; + block.id = inputFieldId; + inInputField = false; + inputFieldId++; + } else if (coqdoc.indexOf('') !== -1) { + block.type = 'hint'; + block.text = coqdoc; + } else { + block.type = 'text'; + block.text = coqdoc; + } + const withinInputFieldMarkers = inInputField && block.type !== 'input'; + Notebook.setDefaultBlockState(block, withinInputFieldMarkers); + blocks.push(block); } } let startCode; @@ -585,9 +598,11 @@ function coqToWp(coqCode) { } else { startCode = finalCommentCloseIndex + 2; } - const code = block.substring(startCode).trim(); + const code = blockContent.substring(startCode).trim(); if (code !== -1) { - blocks.push({type: 'code', text: code}); + const block = {type: 'code', text: code}; + Notebook.setDefaultBlockState(block, inInputField); + blocks.push(block); } i = next; } From 067c6a97d0e109874edaf6aed26873870d95ce45 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 18:00:16 +0200 Subject: [PATCH 21/30] Remove invisible empty code block --- wrapper/assistance/Tutorial.wpe | 4 ---- wrapper/wplib/Notebooks/Tutorial.wpn | 4 ---- 2 files changed, 8 deletions(-) diff --git a/wrapper/assistance/Tutorial.wpe b/wrapper/assistance/Tutorial.wpe index 62769ffc..73b84212 100644 --- a/wrapper/assistance/Tutorial.wpe +++ b/wrapper/assistance/Tutorial.wpe @@ -695,10 +695,6 @@ "start": false, "id": "input-9" }, - { - "type": "code", - "text": " " - }, { "type": "text", "text": "* 12. Split into cases.\n\nAt times, you need to make a case distinction in your proof, as in the following example." diff --git a/wrapper/wplib/Notebooks/Tutorial.wpn b/wrapper/wplib/Notebooks/Tutorial.wpn index da3732a1..7f74e42d 100644 --- a/wrapper/wplib/Notebooks/Tutorial.wpn +++ b/wrapper/wplib/Notebooks/Tutorial.wpn @@ -695,10 +695,6 @@ "start": false, "id": "input-9" }, - { - "type": "code", - "text": " " - }, { "type": "text", "text": "* 12. Split into cases.\n\nAt times, you need to make a case distinction in your proof, as in the following example." From 24ccf4e717e7e4b2715b4f5b00ad7d3e289457d6 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 18:11:01 +0200 Subject: [PATCH 22/30] change id of imported blocks --- src/io/notebook.js | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/io/notebook.js b/src/io/notebook.js index b5a724aa..b169e6e1 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -339,6 +339,7 @@ class Notebook { } try { + // TODO move this to seperate function, also for coqToWp? this.clearContent(); const read = JSON.parse(data); @@ -543,7 +544,7 @@ export default Notebook; function coqToWp(coqCode) { const blocks = []; // return array let inInputField = false; - let inputFieldId = 0; + let inputFieldId = 1; let i = 0; while (i < coqCode.length) { let next = coqCode.indexOf('(**', i+3); @@ -568,7 +569,7 @@ function coqToWp(coqCode) { ); block.type = 'input'; block.start = true; - block.id = inputFieldId; + block.id = 'input-' + inputFieldId; inInputField = true; } else if (coqdoc === 'INPUT-END') { assert( @@ -577,7 +578,7 @@ function coqToWp(coqCode) { ); block.type = 'input'; block.start = false; - block.id = inputFieldId; + block.id = 'input-' + inputFieldId; inInputField = false; inputFieldId++; } else if (coqdoc.indexOf('') !== -1) { @@ -599,7 +600,7 @@ function coqToWp(coqCode) { startCode = finalCommentCloseIndex + 2; } const code = blockContent.substring(startCode).trim(); - if (code !== -1) { + if (code !== '') { const block = {type: 'code', text: code}; Notebook.setDefaultBlockState(block, inInputField); blocks.push(block); From 40718329853cd4efc13c74ec5eee20c1be520dbd Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 18:11:18 +0200 Subject: [PATCH 23/30] first unit test for new import/export spec --- tests/unit/io/test-porting.spec.js | 67 ++ tests/unit/io/test-porting/tutorial.v | 649 ++++++++++++++++ tests/unit/io/test-porting/tutorial.wpe | 969 ++++++++++++++++++++++++ 3 files changed, 1685 insertions(+) create mode 100644 tests/unit/io/test-porting.spec.js create mode 100644 tests/unit/io/test-porting/tutorial.v create mode 100644 tests/unit/io/test-porting/tutorial.wpe diff --git a/tests/unit/io/test-porting.spec.js b/tests/unit/io/test-porting.spec.js new file mode 100644 index 00000000..d2e92975 --- /dev/null +++ b/tests/unit/io/test-porting.spec.js @@ -0,0 +1,67 @@ +import Notebook from '../../../src/io/notebook'; +import {coqToWp} from '../../../src/io/notebook'; +/* eslint-disable */ + +const fs = require('fs'); +const chai = require('chai'); +chai.use(require('chai-string')); +const expect = chai.expect; + +const testcasePath = './tests/unit/io/test-porting/'; +const tests = ['tutorial']; + +const notebook = new Notebook; + + +/** + * Loads the specified notebook + * @param {string} file the desired test notebook + * @return {Promise} a promise that resolves when the file is read, + * or rejects when a read or parse error occurs + */ +function loadNotebook(file) { + + notebook.filePath = file; + + return new Promise((resolve, reject) => { + notebook.read( + () => { + resolve(); + }, + (err) => { + reject(err); + } + ); + }); +} + +if (process.env.NODE_ENV !== 'coverage') { + describe('Full standardized test suite', () => { + for (let i = 0; i < tests.length; i++) { + const fname = tests[i]; + it('test ' + fname, (done) => { + const v = fs.readFileSync(testcasePath + fname + '.v', 'utf-8').toString(); + loadNotebook(testcasePath + fname + '.wpe').then(() => { + /** EXPORTING */ + const text = notebook.parseToText(); + expect(text).to.equal(v); + + /** IMPORTING */ + const blocks = coqToWp(v); + expect(blocks.length).to.equal(notebook.blocks.length); + for (let j = 0; j < blocks.length; j++) { + const a = blocks[j]; + const b = notebook.blocks[j]; + expect(a.type).to.equal(b.type); + if (b.text !== undefined) { + expect(a.text).to.equal(b.text.trim()); + } + expect(a.start).to.equal(b.start); + // expect(a.id).to.equal(b.id); + } + done(); + }).catch(done); + }); + } + }); +} diff --git a/tests/unit/io/test-porting/tutorial.v b/tests/unit/io/test-porting/tutorial.v new file mode 100644 index 00000000..cc9cdf9f --- /dev/null +++ b/tests/unit/io/test-porting/tutorial.v @@ -0,0 +1,649 @@ +(** * Tutorial: Getting used to Waterproof + +This tutorial explains how to get started with Waterproof. The aim of Waterproof is to help learning how to prove mathematical statements. + +This tutorial is in the form of an ##exercise sheet## (sometimes we will call it a ##notebook##). It is a mix of explanations and exercises in which you can try proving mathematical statements yourself. + +The exercise sheet contains ##text cells## (white background) and ##code cells## (gray background). So far, we have been writing text, in text cells. But now we will introduce the first code cell. + *) +Require Import Rbase. +Require Import Rfunctions. + +Require Import Waterproof.AllTactics. +Require Import Waterproof.notations.notations. +Require Import Waterproof.load_database.RealsAndIntegers. + +Open Scope R_scope. + +Set Default Goal Selector "!". +Set Default Timeout 5. +(** The code consists of several _sentences_. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work. *) +(** +We recommend that while you read this notebook, you execute the code sentence-by-sentence by pressing ##Alt + ↓## (on MacOS: ##Option + ↓## or ##⌥ + ↓##). (Alternatively, you can use the buttons on the left, but it is typically much faster to work with keyboard shortcuts.) *) +(** * 1. Prove a lemma + +In the following code cell, we introduce a ##lemma##. We called the lemma ##example_reflexivity##. *) +Lemma example_reflexivity : + 0 = 0. +(** +We will now prove the lemma. We start the proof by writing the sentence ["Proof."] in a code cell. *) + +Proof. +(** +Execute the code sentence after sentence (press ##Alt + ↓## or ##Option + ↓##), until a blue checkmark appears in place of the period after [Proof.]. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under ##Proof progress## (either on the right of the screen, or down below) appeared what we need to show, namely [(0=0)]. We will often refer to this as the current ##goal##. *) +(** +Next, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence ["We conclude that (0=0)."] and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as ##applying a tactic.## *) + +We conclude that (0 = 0). +(** +Execute the above sentence, with ##Alt + ↓##, until the checkmark appears after the sentence. Note how under proof progress it says [Done.]. The lemma is proved! We close the proof by writing [Qed.]. *) + +Qed. +(** +##HINT:## When writing [We conclude that (...)], it is important that at the place of the dots you write the current goal (which you can see under ##Proof progress##), and not another statement. + +##HINT:## If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in. *) +(** ** Try it yourself: prove a lemma + +You can now try this for yourself. We prepared a lemma below, that we named ##exercise_reflexivity##. *) +Lemma exercise_reflexivity : + 3 = 3. +Proof. +(** The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing ##Alt + c## (On MacOS: ##Ctrl + c##), and add a text cell by pressing ##Alt + t## (On MacOS: ##Ctrl + t##). + +You can also change the text that is already there between the blue brackets by clicking on it. + +Below we already added one code cell, which says [Admitted.]. Executing that code cell (##Alt + ↓##), will also make the proof progress turn to [Done.] ##However,## in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise. + +After you have found a proof, replace the [Admitted.] by [Qed.] (click on the code cell and change the sentence). *) +(** INPUT-START *) +(** Write your solution here, then change the [Admitted.] below to [Qed.]. *) + +Admitted. +(** INPUT-END *) +(** * 2. Show *for-all* statements: take arbitrary values + +Let us consider the following lemma. *) +Lemma every_x_equal_to_itself : + for all x : ℝ, + x = x. +(** > ##NOTE:## the notation $x : ℝ$ means $x$ is in $\mathbb{R}$ (or more accurately, $x$ is of type $\mathbb{R}$) may be unfamiliar to you, and you may be more familiar with the notation $x ∈ \reals$. This difference is due to the fact that Waterproof is built on ##type theory## and not on set theory. + +##HINT:## You can insert characters such as ℝ either from the symbol menu that opens when clicking on 'Σ' in the top right corner, or you can write '\reals' until a menu pops up and press enter. Make sure that the code reads 'ℝ' and not '\reals' itself. For many other unicode characters you can use a backslash command as well. *) + +Proof. +(** +To show a statement like "for all $x : \mathbb{R}$, ...", you first need to take an arbitrary $x : \mathbb{R}$, and then continue showing ... . We do this by writing and executing the following sentence, i.e. by applying the following ##tactic##. *) + +Take x : ℝ. +(** +When showing $∀ x : ℝ, ...$, after taking $x : \mathbb{R}$ we need to continue showing whatever statement is at the place of the dots $...$. In our case, we need to show that $x = x$. So we are back in a situation we are by now familiar with. We finish the proof as before. *) + +We conclude that (x = x). +Qed. +(** ** Try it yourself: show *for-all* statements + +Try to complete the proof of the following lemma. *) +Lemma exercise : + for all x : ℝ, + x + 3 = 3 + x. +Proof. +(** +##HINT:## If you would like to get a hint on what you need to do, you can write and execute the sentence [Help.] *) + +Help. +(** + +##HINT:## We recommend that always after you write down a sentence, you immediately execute it (##Alt + ↓##). *) +(** INPUT-START *) +(** Write your solution here. After you have found a proof, remember to change the [Admitted.] below to [Qed.]. *) + +Admitted. +(** INPUT-END *) +(** * 3. Show *there-exists* statements: choose values + +If you want to show that *there exists* $y : \mathbb{R}$ such that $(\dots)$, you need to ##choose## a candidate for $y$, and continue showing $(\dots)$ with your choice. *) +Lemma example_choosing : + there exists y : ℝ, + y < 3. +(***) + +Proof. +(** +We first choose $y:=2$ by using the tactic [Choose y := ((* value *)).]. *) + +Choose y := (2). +(** +(In this particular case we could also have written [Choose y := 2], but in general the brackets are important.) + +We now need to show that (y<3) (see ##Proof progress## after executing the previous sentence). We can record this for our own convenience. *) + +We need to show that (y < 3). +(** +In other words, we need to show that ($2 < 3$). We can also use the [We need to show that] tactic to slightly reformulate the goal. *) + +We need to show that (2 < 3). +(***) + +We conclude that (2 < 3). +Qed. +(** *** Try it yourself: show *there-exists* statements *) +Lemma exercise_choosing : + there exists z : ℝ, + 10 < z. +Proof. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 4. Combine *for-all* and *there-exists* statements + +Often the statement you need to prove consists of many quantifiers. To deal with such a statement, it is useful to deal with this one quantifier at a time, using the techniques that you have just learnt. Here is an example. *) +Lemma example_combine_quantifiers : + ∀ a : ℝ, + ∀ b : ℝ, + ∃ c : ℝ, + c > b - a. +(***) + +Proof. +(** We first deal with (∀ a : ℝ, ... ) by taking an arbitrary $a$ in $ℝ$. *) + +Take a : ℝ. +(** +Next, we need to deal with the quantified statement (∀ b : ℝ, ...). We take an arbitrary $b$ in $ℝ$. *) + +Take b : ℝ. +(** +Now we need to deal with (∃ c : ℝ, ...). We need to make a choice for $c$. *) + +Choose c := (b - a + 1). +(** +Now we can finish the proof. *) + +We need to show that (c > b - a). +We need to show that (b - a + 1 > b - a). +We conclude that (b - a + 1 > b - a). +Qed. +(** ** Try it yourself: combine *for-all* and *there-exists* statements. + +Can you prove the following lemma by dealing with one quantifier at a time? *) +Lemma exercise_combine_quantifiers : + ∀ x : ℝ, + ∀ y : ℝ, + ∃ z : ℝ, + x < z - y. + +Proof. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 5. Make an assumption + +The following lemma expresses that for all $a : \mathbb{R}$, if $a < 0$ then ($-a > 0$). *) + +Lemma example_assumptions : + ∀ a : ℝ, a < 0 ⇒ - a > 0. +(** Corresponding to what we explained above, if we want to show this statement, we first need to take an arbitrary $a : ℝ$. Afterwards, we need to show that $(a < 0) ⇒ (- a > 0)$. + +To show such an implication, we should first assume whatever is on the left hand side of the implication arrow, and then continue showing the right-hand side. In Waterproof, this works as follows. *) + +Proof. +(** +Because we need to show a for-all statement, we know how to start the proof. *) + +Take a : ℝ. +(** +If you now execute the code up to previous sentence, you can see in the ##Proof progress## that we need to show [a < 0 ⇒ -a > 0.] Remembering the rules for brackets, this means: *) +We need to show that + ((a < 0) ⇒ (-a > 0)). +(** +In words, if $a < 0$ then ($- a > 0$). To show this we need to assume that $a < 0$, and then continue proving that $(-a > 0)$. We can make such an assumption with the following sentence. *) + +Assume a_lt_0 : (a < 0). +(** +The ##name## of this assumption is in this case ##a_lt_0##. What you are actually assuming is written after the colon, namely ##a < 0##. Note how after executing the sentence, the assumption $a < 0$ is added under ##Proof progress## with the name ##a_lt_0##. + +We finish the proof. *) +We need to show that (-a > 0). +We conclude that (-a > 0). +Qed. +(** ** Try it yourself: make an assumption + +You can practice making assumptions by proving the lemma below. We have added brackets in the statement to help in reading it, but we didn't have to: the lemma would have exactly the same meaning if we would have left out the brackets. *) +Lemma exercise_assumptions : + ∀ a : ℝ, (∀ b : ℝ, ( a > 0 ⇒ (b > 0 ⇒ a + b > -1))). + +Proof. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 6. Chains of (in)equalities + +As a last step of a proof in Analysis, we often have a chain of (in)equalities. Consider for instance a case in which we would like to show that for all $ε : \mathbb{R}$, if $ε > 0$ then $\min(\epsilon, 1) ≤ 2$. + +Here are the statement and a possible proof in Waterproof. Note that we need to write [Rmin x y] for the minimum of two real numbers $x$ and $y$. *) + +Lemma example_inequalities : + ∀ ε : ℝ, ε > 0 ⇒ Rmin ε 1 < 2. +(***) +Proof. +Take ε : ℝ. +Assume ε_gt_0 : (ε > 0). +We conclude that + (& Rmin ε 1 &≤ 1 + &< 2). +Qed. +(** +Note how we used special notation for the chain of inequalities + +`` +(& Rmin ε 1 &≤ 1 + &< 2). +`` + +We think of this statement that ##and## [Rmin ε 1 ≤ 1] ##and## [1 < 2]. + + +##IMPORTANT##: Here are a few issues to pay attention to: +- After opening the first parenthesis, you need to write a '&' sign. +- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign. +- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported. *) +(** ** Try it yourself: chains of (in)equalities *) +Lemma exercise_inequalities : + ∀ ε : ℝ, ε > 0 ⇒ Rmin (ε / 2) 1 < ε. + +Proof. +(** Click to open hint. + +At the end of your proof, use the following chain of inequalities + +[[ +Rmin (ε / 2) 1 ≤ ε / 2 < ε +]] + +but pay attention to the issues mentioned above: in particular use the '&' sign at the appropriate places. *) +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 7. Backward reasoning in smaller steps + +Sometimes, what you need to show can be derived from another statement. In that case, you can tell Waterproof that it suffices to show the second statement. It will then try to verify that indeed the first statement can be derived from the second, and all that's left to do for you is show the second statement. Here is an example. *) +Lemma example_backwards : + ∀ ε : ℝ, + ε > 0 ⇒ + 3 + Rmax ε 2 ≥ 3. +(***) +Proof. +Take ε : ℝ. +Assume ε_gt_0 : (ε > 0). +(** +We now tell Waterproof that it suffices to show that ($\max( ε, 2)≥ 0$). It will automatically try to verify that this is indeed enough. *) + +It suffices to show that (Rmax ε 2 ≥ 0). +(** +We can finish the proof. *) + +Rewrite inequality (Rmax ε 2) "≥" (2) "≥" 0. +Qed. +(** ** Try it yourself: backward reasoning in smaller steps + + *) +Lemma exercise_backwards : + ∀ ε : ℝ, ε > 0 ⇒ 5 - Rmax ε 3 ≤ 5. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 8. Forward reasoning in smaller steps + +Sometimes, the step to what you need to show is too big for Waterproof to find a proof. In that case, the tactic [We conclude that (...).] will not find a proof. Then it often helps to make smaller steps. + +Here is an example. *) +Lemma example_smaller_steps : + ∀ ε : ℝ, ε > 0 ⇒ + 4 - Rmax ε 1 ≤ 3. +(***) +Proof. +Take ε : ℝ. +Assume ε_gt_0 : (ε > 0). + +(** +We now make an intermediate step. We let Waterproof automatically show that [(Rmax ε 1 ≥ 1)], and we call that statement [Rmax_gt_1]. *) + +It holds that Rmax_gt_1 : (Rmax ε 1 ≥ 1). +(** +Now Waterproof can finish the proof. *) + +We conclude that (4 - Rmax ε 1 ≤ 3). +Qed. +(** +Sometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r]. + +[[ +By Rmax_r it holds that + Rmax_gt_1 : (Rmax ε 1 ≥ 1). +]] + +For very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim. + +[[ +We claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1). +{ + (* proof of claim *) +} +]] *) +(** ** Try it yourself: forward reasoning in smaller steps *) + +Lemma exercise_smallers_steps : + ∀ ε : ℝ, ε > 0 ⇒ + 3 + Rmax 2 ε ≥ 5. + +Proof. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 9. Use a _for-all_ statement + +A special case of the above is when you would like to _use_ a for-all statement, as in the example below. *) +Lemma example_use_for_all : + ∀ x : ℝ, ∀ y : ℝ, + (∀ δ : ℝ, δ > 0 ⇒ x < δ) ⇒ + (∀ ε : ℝ, ε > 0 ⇒ y < ε) ⇒ + x + y < 1. +(***) +Proof. +Take x : ℝ. Take y : ℝ. +Assume del_cond : (∀ δ : ℝ, δ > 0 ⇒ x < δ). +Assume eps_cond : (∀ ε : ℝ, ε > 0 ⇒ y < ε). + +(** We can now ##use## the statement that we called [del_cond] with $δ = 1/2$. We can do this by substituting $\delta = 1/2$ as follows. *) + +By del_cond it holds that x_lt_half : (x < 1/2). +(** Similarly, we can use the statement that we called [eps_cond]. We can also indicate explicitly that we choose $ε = 1/2$ in the statement by writing [By (eps_cond (1/2)) ...] as in *) + +By (eps_cond (1/2)) it holds that y_lt_half : (y < 1/2). + +We conclude that (x + y < 1). +Qed. +(** ** Try it yourself: Use a for-all statement *) +Lemma exercise_use_for_all: + ∀ x : ℝ, + (∀ ε : ℝ, ε > 0 ⇒ x < ε) ⇒ + 10 * x < 1. + +Proof. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 10. Use a _there-exists_ statement + +In this example we show how to ##use## a there-exists statement (when you know it holds). *) + +Lemma example_use_there_exists : + ∀ x : ℝ, + (∃ y : ℝ, 10 < y ∧ y < x) ⇒ + 10 < x. +(***) +Proof. +Take x : ℝ. +Assume exists_y_with_prop : (∃ y : ℝ, 10 < y ∧ y < x). + +(** We now would like to use that there exists a $y$ in $\mathbb{R}$ such that $y>10$ and $x > y$. In other words, we would like to obtain such a $y$. We do this as follows. *) + +Choose y such that + y_gt_10_and_x_gt_y according to exists_y_with_prop. + +(***) +We conclude that + (& 10 &< y + &< x). +Qed. +(** ** Try it yourself: use a _there-exists_ statement *) +Lemma exercise_use_there_exists : + ∀ z : ℝ, + (∃ x : ℝ, (x < -5) ∧ (z > x^2)) ⇒ + 25 < z. + +Proof. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 11. Argue by contradiction + +Sometimes a direct proof is not easy to find, or maybe even impossible, and you need to use a contradiction argument. The following example illustrates how you can do this in Waterproof. *) +Lemma example_contradiction : + ∀ x : ℝ, + (∀ ε : ℝ, ε > 0 ⇒ x < ε) ⇒ + x ≤ 0. +(***) +Proof. +Take x : ℝ. +Assume eps_cond : (∀ ε : ℝ, ε > 0 ⇒ x < ε). +We need to show that (x ≤ 0). +(** We will now argue by contradiction. *) + +We argue by contradiction. +(** +Note how we need to show that $¬ (¬ (x ≤ 0))$. To do so, we first need to assume that $¬ (x ≤ 0)$ and try to arrive at a contradiction. *) + +Assume not_x_le_0 : (¬ (x ≤ 0)). +It holds that x_gt_0 : (x > 0). +By eps_cond it holds that x_lt_x_div_2 : (x < x/2). +It holds that x_le_0 : (x ≤ 0). +(** Now we have derived that both $(x ≤ 0)$ and $¬ (x ≤ 0)$. In general, in a contradiction proof in Waterproof you need to make sure that you get a statement $P$ and the statement $¬ P$ in your list of hypotheses. Then you can finish the proof as follows. *) + +Contradiction. +Qed. +(** +Instead of writing [Contradiction.] you can also write [↯.]. You can get the symbol [↯] with the backslash-command [\contradiction]. *) +(** ** Try it yourself: argue by contradiction *) +Lemma exercise_contradiction : + ∀ x : ℝ, + (∀ ε : ℝ, ε > 0 ⇒ x > 1 - ε) ⇒ + x ≥ 1. + +Proof. +(** INPUT-START *) +(** +Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 12. Split into cases. + +At times, you need to make a case distinction in your proof, as in the following example. *) +Lemma example_cases : + ∀ x : ℝ, ∀ y : ℝ, + Rmax x y = x ∨ Rmax x y = y. +(***) +Proof. +Take x : ℝ. Take y : ℝ. +(** We now make a case distinction. *) + +Either (x < y) or (x ≥ y). +- Case (x < y). + It suffices to show that (Rmax x y = y). + By Rmax_right we conclude that (Rmax x y = y). +- Case (x ≥ y). + It suffices to show that (Rmax x y = x). + By Rmax_left we conclude that (Rmax x y = x). +Qed. +(** ** Try it yourself: split into cases + +See if you can find a proof of the following exercise using a case distinction. *) +Lemma exercises_cases : + ∀ x : ℝ, ∀ y : ℝ, + Rmin x y = x ∨ Rmin x y = y. + +Proof. +(** Click to open hint. + +Distinguish between cases [x < y] and [x ≥ y]. *) +(** INPUT-START *) +(** +Write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 13. Prove two statements: A ∧ B + +The next example shows how you could prove a statement of the form $A ∧ B$. *) +Lemma example_both_statements: + ∀ x : ℝ, x^2 ≥ 0 ∧ | x | ≥ 0. +(***) +Proof. +Take x : ℝ. +(** We now need to show $(x^2 ≥ 0) ∧ (|x| ≥ 0)$. *) + +We show both statements. +(** +Now the proof splits into two parts, one for each statement. We need to indicate these two parts using bullet points. They can be indicated by any of [-], [+], [*], [--] etc.. You can use a bulleted list inside of a bulleted list. *) + +- We need to show that (x^2 ≥ 0). + We conclude that (x^2 ≥ 0). +- We need to show that (| x | ≥ 0). + We conclude that (| x | ≥ 0). +Qed. +(** ** Try it yourself: show both statements + +The following exercise gives some practice in showing two statements. *) +Lemma exercise_both_statements: + ∀ x : ℝ, 0 * x = 0 ∧ x + 1 > x. + +Proof. +(** INPUT-START *) +(** Write your solution here... Don't forget to use bullet points... *) + +Admitted. +(** INPUT-END *) +(** ** 14. Show both directions + +If you need to show a statement of the form $A ⇔ B$, then you need to show both directions separately, namely $A ⇒ B$ and $B ⇒ A$. Here is an example. *) +Lemma example_both_directions: + ∀ x : ℝ, ∀ y : ℝ, + x < y ⇔ y > x. +(***) +Proof. +Take x : ℝ. Take y : ℝ. + +(** We need to indicate that we show both directions. *) + +We show both directions. +(** +Again we need to make use of bullet points to indicate the two directions. *) + +- We need to show that (x < y ⇒ y > x ). + Assume x_lt_y : (x < y). + We conclude that (y > x). +- We need to show that (y > x ⇒ x < y ). + Assume y_gt_x : (y > x). + We need to show that (x < y). + We conclude that (x < y). +Qed. +(** ** Try it yourself: show both directions + +See if you can prove both directions in the following statement. *) +Lemma exercise_both_directions: + ∀ x : ℝ, x > 1 ⇔ x - 1 > 0. + +Proof. +(** INPUT-START *) +(** Write your solution here... Don't forget to use bullet points... *) + +Admitted. +(** INPUT-END *) +(** * 15. Proof by induction + +The following example shows how one could use mathematical induction to show a statement of the form + + $$∀ k : ℕ, ... $$ + +Note that Waterproof will usually interpret any statement such as an inequality [n(k +1 ) > n k] as a statement comparing real numbers, while in this exercise we need statements that compare natural numbers. To indicate this, we have to write [(n (k+1) > n k)%nat] instead. *) +Lemma example_induction : + ∀ n : ℕ → ℕ, (∀ k : ℕ, (n k < n (k + 1))%nat) ⇒ + ∀ k : ℕ, (k ≤ n k)%nat. +(***) +Proof. +Take n : (ℕ → ℕ). +Assume n_increasing : (∀ k : ℕ, (n k < n (k + 1))%nat). +(** We can now perform the induction argument. *) + +We use induction on k. +- We first show the base case, namely ( (0 ≤ n 0)%nat ). + We conclude that (0 ≤ n 0)%nat. +- We now show the induction step. + Assume IH : (k ≤ n k)%nat. + It holds that n_k_lt_n_k_plus_1 : (n k < n (k + 1))%nat. + We conclude that (k + 1 ≤ n (k + 1))%nat. +Qed. +(** ** Try it yourself: a proof by induction + +Can you prove the following statement using mathematical induction? *) +Lemma exercise_induction : + ∀ f : ℕ → ℕ, (∀ k : ℕ, (f (k + 1) = f k)%nat) ⇒ + ∀ k : ℕ, (f k = f 0)%nat. + +Proof. +(** INPUT-START *) +(** write your solution here... *) + +Admitted. +(** INPUT-END *) +(** * 16. Expand definitions + +It happens that you need to use a definition of some object in Waterproof, for instance the definition of a function. Here is the definition of a function called [square]. *) + +Definition square (x : ℝ) := x^2. +(** +We now aim to prove the following lemma. *) +Lemma example_expand : + ∀ x : ℝ, square x ≥ 0. +(***) +Proof. +Take x : ℝ. +(** At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing [We need to show that (x^2 ≥ 0).], or we could write + +[[ +We conclude that + (& square x &= x^2 + &≥ 0). +]] +However these options aren't available if you do not know the definition of [square]. In that case you could write *) + +Expand the definition of square. +(** +Now Waterproof has expanded the definition of [square] in the goal. It is always important to keep the proof readable, so that's why Waterproof asks you now to also reformulate the goal. *) + +That is, write the goal as (x^2 ≥ 0). +We conclude that (x^2 ≥ 0). +Qed. +(** You can also expand the definition in a hypothesis. For instance, +[[ +Expand the definition of square in H. +]] +would expand the definition of [square] in the hypothesis with the name [H]. *) +(** ** Try it yourself: expand a definition *) +Lemma exercise_expand : + ∀ x : ℝ, - (square x) ≤ 0. + +Proof. +(** INPUT-START *) +(** Write your solution here... *) + +Admitted. +(** INPUT-END *) \ No newline at end of file diff --git a/tests/unit/io/test-porting/tutorial.wpe b/tests/unit/io/test-porting/tutorial.wpe new file mode 100644 index 00000000..73b84212 --- /dev/null +++ b/tests/unit/io/test-porting/tutorial.wpe @@ -0,0 +1,969 @@ +{ + "exerciseSheet": true, + "blocks": [ + { + "type": "text", + "text": "* Tutorial: Getting used to Waterproof\n\nThis tutorial explains how to get started with Waterproof. The aim of Waterproof is to help learning how to prove mathematical statements.\n\nThis tutorial is in the form of an ##exercise sheet## (sometimes we will call it a ##notebook##). It is a mix of explanations and exercises in which you can try proving mathematical statements yourself. \n\nThe exercise sheet contains ##text cells## (white background) and ##code cells## (gray background). So far, we have been writing text, in text cells. But now we will introduce the first code cell.\n" + }, + { + "type": "code", + "text": "Require Import Rbase.\nRequire Import Rfunctions.\n\nRequire Import Waterproof.AllTactics.\nRequire Import Waterproof.notations.notations.\nRequire Import Waterproof.load_database.RealsAndIntegers.\n\nOpen Scope R_scope.\n\nSet Default Goal Selector \"!\".\nSet Default Timeout 5." + }, + { + "type": "text", + "text": "The code consists of several _sentences_. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." + }, + { + "type": "text", + "text": "\nWe recommend that while you read this notebook, you execute the code sentence-by-sentence by pressing ##Alt + ↓## (on MacOS: ##Option + ↓## or ##⌥ + ↓##). (Alternatively, you can use the buttons on the left, but it is typically much faster to work with keyboard shortcuts.)" + }, + { + "type": "text", + "text": "* 1. Prove a lemma\n\nIn the following code cell, we introduce a ##lemma##. We called the lemma ##example_reflexivity##." + }, + { + "type": "code", + "text": "Lemma example_reflexivity :\n 0 = 0." + }, + { + "type": "text", + "text": "\nWe will now prove the lemma. We start the proof by writing the sentence [\"Proof.\"] in a code cell." + }, + { + "type": "code", + "text": "\nProof." + }, + { + "type": "text", + "text": "\nExecute the code sentence after sentence (press ##Alt + ↓## or ##Option + ↓##), until a blue checkmark appears in place of the period after [Proof.]. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under ##Proof progress## (either on the right of the screen, or down below) appeared what we need to show, namely [(0=0)]. We will often refer to this as the current ##goal##." + }, + { + "type": "text", + "text": "\nNext, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence [\"We conclude that (0=0).\"] and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as ##applying a tactic.##" + }, + { + "type": "code", + "text": "\nWe conclude that (0 = 0)." + }, + { + "type": "text", + "text": "\nExecute the above sentence, with ##Alt + ↓##, until the checkmark appears after the sentence. Note how under proof progress it says [Done.]. The lemma is proved! We close the proof by writing [Qed.]." + }, + { + "type": "code", + "text": "\nQed." + }, + { + "type": "text", + "text": "\n##HINT:## When writing [We conclude that (...)], it is important that at the place of the dots you write the current goal (which you can see under ##Proof progress##), and not another statement.\n\n##HINT:## If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in." + }, + { + "type": "text", + "text": "** Try it yourself: prove a lemma\n\nYou can now try this for yourself. We prepared a lemma below, that we named ##exercise_reflexivity##." + }, + { + "type": "code", + "text": "Lemma exercise_reflexivity :\n 3 = 3.\nProof." + }, + { + "type": "text", + "text": "The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing ##Alt + c## (On MacOS: ##Ctrl + c##), and add a text cell by pressing ##Alt + t## (On MacOS: ##Ctrl + t##).\n\nYou can also change the text that is already there between the blue brackets by clicking on it.\n\nBelow we already added one code cell, which says [Admitted.]. Executing that code cell (##Alt + ↓##), will also make the proof progress turn to [Done.] ##However,## in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise.\n\nAfter you have found a proof, replace the [Admitted.] by [Qed.] (click on the code cell and change the sentence)." + }, + { + "type": "input", + "start": true, + "id": "input-1" + }, + { + "type": "text", + "text": "Write your solution here, then change the [Admitted.] below to [Qed.]." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-1" + }, + { + "type": "text", + "text": "* 2. Show *for-all* statements: take arbitrary values\n\nLet us consider the following lemma." + }, + { + "type": "code", + "text": "Lemma every_x_equal_to_itself :\n for all x : ℝ,\n x = x." + }, + { + "type": "text", + "text": "> ##NOTE:## the notation $x : ℝ$ means $x$ is in $\\mathbb{R}$ (or more accurately, $x$ is of type $\\mathbb{R}$) may be unfamiliar to you, and you may be more familiar with the notation $x ∈ \\reals$. This difference is due to the fact that Waterproof is built on ##type theory## and not on set theory. \n\n##HINT:## You can insert characters such as ℝ either from the symbol menu that opens when clicking on 'Σ' in the top right corner, or you can write '\\reals' until a menu pops up and press enter. Make sure that the code reads 'ℝ' and not '\\reals' itself. For many other unicode characters you can use a backslash command as well." + }, + { + "type": "code", + "text": "\nProof." + }, + { + "type": "text", + "text": "\nTo show a statement like \"for all $x : \\mathbb{R}$, ...\", you first need to take an arbitrary $x : \\mathbb{R}$, and then continue showing ... . We do this by writing and executing the following sentence, i.e. by applying the following ##tactic##." + }, + { + "type": "code", + "text": "\nTake x : ℝ." + }, + { + "type": "text", + "text": "\nWhen showing $∀ x : ℝ, ...$, after taking $x : \\mathbb{R}$ we need to continue showing whatever statement is at the place of the dots $...$. In our case, we need to show that $x = x$. So we are back in a situation we are by now familiar with. We finish the proof as before." + }, + { + "type": "code", + "text": "\nWe conclude that (x = x).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: show *for-all* statements\n\nTry to complete the proof of the following lemma." + }, + { + "type": "code", + "text": "Lemma exercise :\n for all x : ℝ,\n x + 3 = 3 + x.\nProof." + }, + { + "type": "text", + "text": "\n##HINT:## If you would like to get a hint on what you need to do, you can write and execute the sentence [Help.]" + }, + { + "type": "code", + "text": "\nHelp." + }, + { + "type": "text", + "text": "\n\n##HINT:## We recommend that always after you write down a sentence, you immediately execute it (##Alt + ↓##)." + }, + { + "type": "input", + "start": true, + "id": "input-2" + }, + { + "type": "text", + "text": "Write your solution here. After you have found a proof, remember to change the [Admitted.] below to [Qed.]." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-2" + }, + { + "type": "text", + "text": "* 3. Show *there-exists* statements: choose values\n\nIf you want to show that *there exists* $y : \\mathbb{R}$ such that $(\\dots)$, you need to ##choose## a candidate for $y$, and continue showing $(\\dots)$ with your choice." + }, + { + "type": "code", + "text": "Lemma example_choosing : \n there exists y : ℝ,\n y < 3." + }, + { + "type": "code", + "text": "\nProof." + }, + { + "type": "text", + "text": "\nWe first choose $y:=2$ by using the tactic [Choose y := ((* value *)).]." + }, + { + "type": "code", + "text": "\nChoose y := (2)." + }, + { + "type": "text", + "text": "\n(In this particular case we could also have written [Choose y := 2], but in general the brackets are important.)\n\nWe now need to show that (y<3) (see ##Proof progress## after executing the previous sentence). We can record this for our own convenience." + }, + { + "type": "code", + "text": "\nWe need to show that (y < 3)." + }, + { + "type": "text", + "text": "\nIn other words, we need to show that ($2 < 3$). We can also use the [We need to show that] tactic to slightly reformulate the goal." + }, + { + "type": "code", + "text": "\nWe need to show that (2 < 3)." + }, + { + "type": "code", + "text": "\nWe conclude that (2 < 3).\nQed." + }, + { + "type": "text", + "text": "*** Try it yourself: show *there-exists* statements" + }, + { + "type": "code", + "text": "Lemma exercise_choosing :\n there exists z : ℝ,\n 10 < z.\nProof." + }, + { + "type": "input", + "start": true, + "id": "input-3" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-3" + }, + { + "type": "text", + "text": "* 4. Combine *for-all* and *there-exists* statements\n\nOften the statement you need to prove consists of many quantifiers. To deal with such a statement, it is useful to deal with this one quantifier at a time, using the techniques that you have just learnt. Here is an example." + }, + { + "type": "code", + "text": "Lemma example_combine_quantifiers :\n ∀ a : ℝ,\n ∀ b : ℝ,\n ∃ c : ℝ,\n c > b - a." + }, + { + "type": "code", + "text": "\nProof." + }, + { + "type": "text", + "text": "We first deal with (∀ a : ℝ, ... ) by taking an arbitrary $a$ in $ℝ$." + }, + { + "type": "code", + "text": "\nTake a : ℝ." + }, + { + "type": "text", + "text": "\nNext, we need to deal with the quantified statement (∀ b : ℝ, ...). We take an arbitrary $b$ in $ℝ$." + }, + { + "type": "code", + "text": "\nTake b : ℝ." + }, + { + "type": "text", + "text": "\nNow we need to deal with (∃ c : ℝ, ...). We need to make a choice for $c$." + }, + { + "type": "code", + "text": "\nChoose c := (b - a + 1)." + }, + { + "type": "text", + "text": "\nNow we can finish the proof." + }, + { + "type": "code", + "text": "\nWe need to show that (c > b - a).\nWe need to show that (b - a + 1 > b - a).\nWe conclude that (b - a + 1 > b - a).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: combine *for-all* and *there-exists* statements.\n\nCan you prove the following lemma by dealing with one quantifier at a time?" + }, + { + "type": "code", + "text": "Lemma exercise_combine_quantifiers :\n ∀ x : ℝ,\n ∀ y : ℝ,\n ∃ z : ℝ,\n x < z - y.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-16" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-16" + }, + { + "type": "text", + "text": "* 5. Make an assumption\n\nThe following lemma expresses that for all $a : \\mathbb{R}$, if $a < 0$ then ($-a > 0$)." + }, + { + "type": "code", + "text": "\nLemma example_assumptions :\n ∀ a : ℝ, a < 0 ⇒ - a > 0." + }, + { + "type": "text", + "text": "Corresponding to what we explained above, if we want to show this statement, we first need to take an arbitrary $a : ℝ$. Afterwards, we need to show that $(a < 0) ⇒ (- a > 0)$. \n\nTo show such an implication, we should first assume whatever is on the left hand side of the implication arrow, and then continue showing the right-hand side. In Waterproof, this works as follows." + }, + { + "type": "code", + "text": "\nProof." + }, + { + "type": "text", + "text": "\nBecause we need to show a for-all statement, we know how to start the proof." + }, + { + "type": "code", + "text": "\nTake a : ℝ." + }, + { + "type": "text", + "text": "\nIf you now execute the code up to previous sentence, you can see in the ##Proof progress## that we need to show [a < 0 ⇒ -a > 0.] Remembering the rules for brackets, this means:" + }, + { + "type": "code", + "text": "We need to show that \n ((a < 0) ⇒ (-a > 0))." + }, + { + "type": "text", + "text": "\nIn words, if $a < 0$ then ($- a > 0$). To show this we need to assume that $a < 0$, and then continue proving that $(-a > 0)$. We can make such an assumption with the following sentence." + }, + { + "type": "code", + "text": "\nAssume a_lt_0 : (a < 0)." + }, + { + "type": "text", + "text": "\nThe ##name## of this assumption is in this case ##a_lt_0##. What you are actually assuming is written after the colon, namely ##a < 0##. Note how after executing the sentence, the assumption $a < 0$ is added under ##Proof progress## with the name ##a_lt_0##.\n\nWe finish the proof." + }, + { + "type": "code", + "text": "We need to show that (-a > 0).\nWe conclude that (-a > 0).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: make an assumption\n\nYou can practice making assumptions by proving the lemma below. We have added brackets in the statement to help in reading it, but we didn't have to: the lemma would have exactly the same meaning if we would have left out the brackets." + }, + { + "type": "code", + "text": "Lemma exercise_assumptions :\n ∀ a : ℝ, (∀ b : ℝ, ( a > 0 ⇒ (b > 0 ⇒ a + b > -1))).\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-6" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-6" + }, + { + "type": "text", + "text": "* 6. Chains of (in)equalities\n\nAs a last step of a proof in Analysis, we often have a chain of (in)equalities. Consider for instance a case in which we would like to show that for all $ε : \\mathbb{R}$, if $ε > 0$ then $\\min(\\epsilon, 1) ≤ 2$. \n\nHere are the statement and a possible proof in Waterproof. Note that we need to write [Rmin x y] for the minimum of two real numbers $x$ and $y$." + }, + { + "type": "code", + "text": "\nLemma example_inequalities :\n ∀ ε : ℝ, ε > 0 ⇒ Rmin ε 1 < 2." + }, + { + "type": "code", + "text": "Proof.\nTake ε : ℝ.\nAssume ε_gt_0 : (ε > 0).\nWe conclude that\n (& Rmin ε 1 &≤ 1\n &< 2).\nQed." + }, + { + "type": "text", + "text": "\nNote how we used special notation for the chain of inequalities\n\n``\n(& Rmin ε 1 &≤ 1\n &< 2).\n``\n\nWe think of this statement that ##and## [Rmin ε 1 ≤ 1] ##and## [1 < 2]. \n\n\n##IMPORTANT##: Here are a few issues to pay attention to:\n- After opening the first parenthesis, you need to write a '&' sign.\n- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign.\n- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported." + }, + { + "type": "text", + "text": "** Try it yourself: chains of (in)equalities" + }, + { + "type": "code", + "text": "Lemma exercise_inequalities :\n ∀ ε : ℝ, ε > 0 ⇒ Rmin (ε / 2) 1 < ε.\n \nProof." + }, + { + "type": "hint", + "text": "Click to open hint.\n\nAt the end of your proof, use the following chain of inequalities \n\n[[\nRmin (ε / 2) 1 ≤ ε / 2 < ε\n]]\n\nbut pay attention to the issues mentioned above: in particular use the '&' sign at the appropriate places." + }, + { + "type": "input", + "start": true, + "id": "input-4" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-4" + }, + { + "type": "text", + "text": "* 7. Backward reasoning in smaller steps\n\nSometimes, what you need to show can be derived from another statement. In that case, you can tell Waterproof that it suffices to show the second statement. It will then try to verify that indeed the first statement can be derived from the second, and all that's left to do for you is show the second statement. Here is an example." + }, + { + "type": "code", + "text": "Lemma example_backwards :\n ∀ ε : ℝ,\n ε > 0 ⇒\n 3 + Rmax ε 2 ≥ 3." + }, + { + "type": "code", + "text": "Proof.\nTake ε : ℝ.\nAssume ε_gt_0 : (ε > 0)." + }, + { + "type": "text", + "text": "\nWe now tell Waterproof that it suffices to show that ($\\max( ε, 2)≥ 0$). It will automatically try to verify that this is indeed enough." + }, + { + "type": "code", + "text": "\nIt suffices to show that (Rmax ε 2 ≥ 0)." + }, + { + "type": "text", + "text": "\nWe can finish the proof." + }, + { + "type": "code", + "text": "\nRewrite inequality (Rmax ε 2) \"≥\" (2) \"≥\" 0.\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: backward reasoning in smaller steps\n\n" + }, + { + "type": "code", + "text": "Lemma exercise_backwards :\n ∀ ε : ℝ, ε > 0 ⇒ 5 - Rmax ε 3 ≤ 5." + }, + { + "type": "input", + "start": true, + "id": "input-8" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-8" + }, + { + "type": "text", + "text": "* 8. Forward reasoning in smaller steps\n\nSometimes, the step to what you need to show is too big for Waterproof to find a proof. In that case, the tactic [We conclude that (...).] will not find a proof. Then it often helps to make smaller steps.\n\nHere is an example." + }, + { + "type": "code", + "text": "Lemma example_smaller_steps :\n ∀ ε : ℝ, ε > 0 ⇒\n 4 - Rmax ε 1 ≤ 3." + }, + { + "type": "code", + "text": "Proof.\nTake ε : ℝ.\nAssume ε_gt_0 : (ε > 0).\n" + }, + { + "type": "text", + "text": "\nWe now make an intermediate step. We let Waterproof automatically show that [(Rmax ε 1 ≥ 1)], and we call that statement [Rmax_gt_1]." + }, + { + "type": "code", + "text": "\nIt holds that Rmax_gt_1 : (Rmax ε 1 ≥ 1)." + }, + { + "type": "text", + "text": "\nNow Waterproof can finish the proof." + }, + { + "type": "code", + "text": "\nWe conclude that (4 - Rmax ε 1 ≤ 3).\nQed." + }, + { + "type": "text", + "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r].\n\n[[\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n]]\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n[[\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n (* proof of claim *)\n}\n]]" + }, + { + "type": "text", + "text": "** Try it yourself: forward reasoning in smaller steps" + }, + { + "type": "code", + "text": "\nLemma exercise_smallers_steps :\n ∀ ε : ℝ, ε > 0 ⇒\n 3 + Rmax 2 ε ≥ 5. \n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-5" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-5" + }, + { + "type": "text", + "text": "* 9. Use a _for-all_ statement\n\nA special case of the above is when you would like to _use_ a for-all statement, as in the example below." + }, + { + "type": "code", + "text": "Lemma example_use_for_all :\n ∀ x : ℝ, ∀ y : ℝ,\n (∀ δ : ℝ, δ > 0 ⇒ x < δ) ⇒\n (∀ ε : ℝ, ε > 0 ⇒ y < ε) ⇒\n x + y < 1." + }, + { + "type": "code", + "text": "Proof.\nTake x : ℝ. Take y : ℝ.\nAssume del_cond : (∀ δ : ℝ, δ > 0 ⇒ x < δ).\nAssume eps_cond : (∀ ε : ℝ, ε > 0 ⇒ y < ε).\n" + }, + { + "type": "text", + "text": "We can now ##use## the statement that we called [del_cond] with $δ = 1/2$. We can do this by substituting $\\delta = 1/2$ as follows." + }, + { + "type": "code", + "text": "\nBy del_cond it holds that x_lt_half : (x < 1/2)." + }, + { + "type": "text", + "text": "Similarly, we can use the statement that we called [eps_cond]. We can also indicate explicitly that we choose $ε = 1/2$ in the statement by writing [By (eps_cond (1/2)) ...] as in" + }, + { + "type": "code", + "text": "\nBy (eps_cond (1/2)) it holds that y_lt_half : (y < 1/2).\n\nWe conclude that (x + y < 1).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: Use a for-all statement" + }, + { + "type": "code", + "text": "Lemma exercise_use_for_all:\n ∀ x : ℝ,\n (∀ ε : ℝ, ε > 0 ⇒ x < ε) ⇒\n 10 * x < 1.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-15" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-15" + }, + { + "type": "text", + "text": "* 10. Use a _there-exists_ statement\n\nIn this example we show how to ##use## a there-exists statement (when you know it holds)." + }, + { + "type": "code", + "text": "\nLemma example_use_there_exists :\n ∀ x : ℝ,\n (∃ y : ℝ, 10 < y ∧ y < x) ⇒\n 10 < x." + }, + { + "type": "code", + "text": "Proof.\nTake x : ℝ.\nAssume exists_y_with_prop : (∃ y : ℝ, 10 < y ∧ y < x).\n" + }, + { + "type": "text", + "text": "We now would like to use that there exists a $y$ in $\\mathbb{R}$ such that $y>10$ and $x > y$. In other words, we would like to obtain such a $y$. We do this as follows." + }, + { + "type": "code", + "text": "\nChoose y such that \n y_gt_10_and_x_gt_y according to exists_y_with_prop.\n" + }, + { + "type": "code", + "text": "We conclude that\n (& 10 &< y\n &< x).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: use a _there-exists_ statement" + }, + { + "type": "code", + "text": "Lemma exercise_use_there_exists :\n ∀ z : ℝ,\n (∃ x : ℝ, (x < -5) ∧ (z > x^2)) ⇒\n 25 < z.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-7" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-7" + }, + { + "type": "text", + "text": "* 11. Argue by contradiction\n\nSometimes a direct proof is not easy to find, or maybe even impossible, and you need to use a contradiction argument. The following example illustrates how you can do this in Waterproof." + }, + { + "type": "code", + "text": "Lemma example_contradiction :\n ∀ x : ℝ,\n (∀ ε : ℝ, ε > 0 ⇒ x < ε) ⇒\n x ≤ 0." + }, + { + "type": "code", + "text": "Proof. \nTake x : ℝ.\nAssume eps_cond : (∀ ε : ℝ, ε > 0 ⇒ x < ε).\nWe need to show that (x ≤ 0)." + }, + { + "type": "text", + "text": "We will now argue by contradiction." + }, + { + "type": "code", + "text": "\nWe argue by contradiction." + }, + { + "type": "text", + "text": "\nNote how we need to show that $¬ (¬ (x ≤ 0))$. To do so, we first need to assume that $¬ (x ≤ 0)$ and try to arrive at a contradiction." + }, + { + "type": "code", + "text": "\nAssume not_x_le_0 : (¬ (x ≤ 0)).\nIt holds that x_gt_0 : (x > 0).\nBy eps_cond it holds that x_lt_x_div_2 : (x < x/2).\nIt holds that x_le_0 : (x ≤ 0)." + }, + { + "type": "text", + "text": "Now we have derived that both $(x ≤ 0)$ and $¬ (x ≤ 0)$. In general, in a contradiction proof in Waterproof you need to make sure that you get a statement $P$ and the statement $¬ P$ in your list of hypotheses. Then you can finish the proof as follows." + }, + { + "type": "code", + "text": "\nContradiction.\nQed." + }, + { + "type": "text", + "text": "\nInstead of writing [Contradiction.] you can also write [↯.]. You can get the symbol [↯] with the backslash-command [\\contradiction]." + }, + { + "type": "text", + "text": "** Try it yourself: argue by contradiction" + }, + { + "type": "code", + "text": "Lemma exercise_contradiction :\n ∀ x : ℝ,\n (∀ ε : ℝ, ε > 0 ⇒ x > 1 - ε) ⇒\n x ≥ 1.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-9" + }, + { + "type": "text", + "text": "\nWrite your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-9" + }, + { + "type": "text", + "text": "* 12. Split into cases.\n\nAt times, you need to make a case distinction in your proof, as in the following example." + }, + { + "type": "code", + "text": "Lemma example_cases : \n ∀ x : ℝ, ∀ y : ℝ,\n Rmax x y = x ∨ Rmax x y = y." + }, + { + "type": "code", + "text": "Proof. \nTake x : ℝ. Take y : ℝ." + }, + { + "type": "text", + "text": "We now make a case distinction." + }, + { + "type": "code", + "text": "\nEither (x < y) or (x ≥ y).\n- Case (x < y).\n It suffices to show that (Rmax x y = y).\n By Rmax_right we conclude that (Rmax x y = y).\n- Case (x ≥ y).\n It suffices to show that (Rmax x y = x).\n By Rmax_left we conclude that (Rmax x y = x).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: split into cases\n\nSee if you can find a proof of the following exercise using a case distinction." + }, + { + "type": "code", + "text": "Lemma exercises_cases :\n ∀ x : ℝ, ∀ y : ℝ,\n Rmin x y = x ∨ Rmin x y = y.\n \nProof." + }, + { + "type": "hint", + "text": "Click to open hint.\n\nDistinguish between cases [x < y] and [x ≥ y]." + }, + { + "type": "input", + "start": true, + "id": "input-10" + }, + { + "type": "text", + "text": "\nWrite your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-10" + }, + { + "type": "text", + "text": "* 13. Prove two statements: A ∧ B\n\nThe next example shows how you could prove a statement of the form $A ∧ B$." + }, + { + "type": "code", + "text": "Lemma example_both_statements:\n ∀ x : ℝ, x^2 ≥ 0 ∧ | x | ≥ 0." + }, + { + "type": "code", + "text": "Proof.\nTake x : ℝ." + }, + { + "type": "text", + "text": "We now need to show $(x^2 ≥ 0) ∧ (|x| ≥ 0)$." + }, + { + "type": "code", + "text": "\nWe show both statements." + }, + { + "type": "text", + "text": "\nNow the proof splits into two parts, one for each statement. We need to indicate these two parts using bullet points. They can be indicated by any of [-], [+], [*], [--] etc.. You can use a bulleted list inside of a bulleted list." + }, + { + "type": "code", + "text": "\n- We need to show that (x^2 ≥ 0).\n We conclude that (x^2 ≥ 0).\n- We need to show that (| x | ≥ 0).\n We conclude that (| x | ≥ 0).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: show both statements\n\nThe following exercise gives some practice in showing two statements." + }, + { + "type": "code", + "text": "Lemma exercise_both_statements:\n ∀ x : ℝ, 0 * x = 0 ∧ x + 1 > x.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-11" + }, + { + "type": "text", + "text": "Write your solution here... Don't forget to use bullet points..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-11" + }, + { + "type": "text", + "text": "** 14. Show both directions\n\nIf you need to show a statement of the form $A ⇔ B$, then you need to show both directions separately, namely $A ⇒ B$ and $B ⇒ A$. Here is an example." + }, + { + "type": "code", + "text": "Lemma example_both_directions:\n ∀ x : ℝ, ∀ y : ℝ,\n x < y ⇔ y > x." + }, + { + "type": "code", + "text": "Proof.\nTake x : ℝ. Take y : ℝ.\n" + }, + { + "type": "text", + "text": "We need to indicate that we show both directions." + }, + { + "type": "code", + "text": "\nWe show both directions." + }, + { + "type": "text", + "text": "\nAgain we need to make use of bullet points to indicate the two directions." + }, + { + "type": "code", + "text": "\n- We need to show that (x < y ⇒ y > x ).\n Assume x_lt_y : (x < y).\n We conclude that (y > x).\n- We need to show that (y > x ⇒ x < y ).\n Assume y_gt_x : (y > x).\n We need to show that (x < y).\n We conclude that (x < y).\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: show both directions\n\nSee if you can prove both directions in the following statement." + }, + { + "type": "code", + "text": "Lemma exercise_both_directions:\n ∀ x : ℝ, x > 1 ⇔ x - 1 > 0.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-12" + }, + { + "type": "text", + "text": "Write your solution here... Don't forget to use bullet points..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-12" + }, + { + "type": "text", + "text": "* 15. Proof by induction\n\nThe following example shows how one could use mathematical induction to show a statement of the form\n\n $$∀ k : ℕ, ... $$\n\nNote that Waterproof will usually interpret any statement such as an inequality [n(k +1 ) > n k] as a statement comparing real numbers, while in this exercise we need statements that compare natural numbers. To indicate this, we have to write [(n (k+1) > n k)%nat] instead." + }, + { + "type": "code", + "text": "Lemma example_induction :\n ∀ n : ℕ → ℕ, (∀ k : ℕ, (n k < n (k + 1))%nat) ⇒\n ∀ k : ℕ, (k ≤ n k)%nat." + }, + { + "type": "code", + "text": "Proof.\nTake n : (ℕ → ℕ).\nAssume n_increasing : (∀ k : ℕ, (n k < n (k + 1))%nat)." + }, + { + "type": "text", + "text": "We can now perform the induction argument." + }, + { + "type": "code", + "text": "\nWe use induction on k.\n- We first show the base case, namely ( (0 ≤ n 0)%nat ).\n We conclude that (0 ≤ n 0)%nat.\n- We now show the induction step.\n Assume IH : (k ≤ n k)%nat.\n It holds that n_k_lt_n_k_plus_1 : (n k < n (k + 1))%nat.\n We conclude that (k + 1 ≤ n (k + 1))%nat.\nQed." + }, + { + "type": "text", + "text": "** Try it yourself: a proof by induction\n\nCan you prove the following statement using mathematical induction?" + }, + { + "type": "code", + "text": "Lemma exercise_induction :\n ∀ f : ℕ → ℕ, (∀ k : ℕ, (f (k + 1) = f k)%nat) ⇒\n ∀ k : ℕ, (f k = f 0)%nat.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-13" + }, + { + "type": "text", + "text": "write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-13" + }, + { + "type": "text", + "text": "* 16. Expand definitions\n\nIt happens that you need to use a definition of some object in Waterproof, for instance the definition of a function. Here is the definition of a function called [square]." + }, + { + "type": "code", + "text": "\nDefinition square (x : ℝ) := x^2." + }, + { + "type": "text", + "text": "\nWe now aim to prove the following lemma." + }, + { + "type": "code", + "text": "Lemma example_expand :\n ∀ x : ℝ, square x ≥ 0." + }, + { + "type": "code", + "text": "Proof.\nTake x : ℝ." + }, + { + "type": "text", + "text": "At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing [We need to show that (x^2 ≥ 0).], or we could write \n\n[[\nWe conclude that\n (& square x &= x^2\n &≥ 0). \n]]\nHowever these options aren't available if you do not know the definition of [square]. In that case you could write" + }, + { + "type": "code", + "text": "\nExpand the definition of square." + }, + { + "type": "text", + "text": "\nNow Waterproof has expanded the definition of [square] in the goal. It is always important to keep the proof readable, so that's why Waterproof asks you now to also reformulate the goal." + }, + { + "type": "code", + "text": "\nThat is, write the goal as (x^2 ≥ 0).\nWe conclude that (x^2 ≥ 0).\nQed." + }, + { + "type": "text", + "text": "You can also expand the definition in a hypothesis. For instance,\n[[\nExpand the definition of square in H.\n]]\nwould expand the definition of [square] in the hypothesis with the name [H]." + }, + { + "type": "text", + "text": "** Try it yourself: expand a definition" + }, + { + "type": "code", + "text": "Lemma exercise_expand :\n ∀ x : ℝ, - (square x) ≤ 0.\n \nProof." + }, + { + "type": "input", + "start": true, + "id": "input-14" + }, + { + "type": "text", + "text": "Write your solution here..." + }, + { + "type": "code", + "text": "\nAdmitted." + }, + { + "type": "input", + "start": false, + "id": "input-14" + } + ] +} \ No newline at end of file From efb052e4b1346d214cb63f059875110c62a36661 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 18:13:10 +0200 Subject: [PATCH 24/30] linting --- tests/unit/io/test-porting.spec.js | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/tests/unit/io/test-porting.spec.js b/tests/unit/io/test-porting.spec.js index d2e92975..9454bd71 100644 --- a/tests/unit/io/test-porting.spec.js +++ b/tests/unit/io/test-porting.spec.js @@ -1,6 +1,5 @@ import Notebook from '../../../src/io/notebook'; import {coqToWp} from '../../../src/io/notebook'; -/* eslint-disable */ const fs = require('fs'); const chai = require('chai'); @@ -50,14 +49,14 @@ if (process.env.NODE_ENV !== 'coverage') { const blocks = coqToWp(v); expect(blocks.length).to.equal(notebook.blocks.length); for (let j = 0; j < blocks.length; j++) { - const a = blocks[j]; - const b = notebook.blocks[j]; - expect(a.type).to.equal(b.type); - if (b.text !== undefined) { - expect(a.text).to.equal(b.text.trim()); - } - expect(a.start).to.equal(b.start); - // expect(a.id).to.equal(b.id); + const a = blocks[j]; + const b = notebook.blocks[j]; + expect(a.type).to.equal(b.type); + if (b.text !== undefined) { + expect(a.text).to.equal(b.text.trim()); + } + expect(a.start).to.equal(b.start); + // expect(a.id).to.equal(b.id); } done(); }).catch(done); From ddc71bb8fb25271b5a8356dd16f503e4539437eb Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 18:15:31 +0200 Subject: [PATCH 25/30] lint --- tests/unit/io/test-porting.spec.js | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/unit/io/test-porting.spec.js b/tests/unit/io/test-porting.spec.js index 9454bd71..cb00f51a 100644 --- a/tests/unit/io/test-porting.spec.js +++ b/tests/unit/io/test-porting.spec.js @@ -39,7 +39,9 @@ if (process.env.NODE_ENV !== 'coverage') { for (let i = 0; i < tests.length; i++) { const fname = tests[i]; it('test ' + fname, (done) => { - const v = fs.readFileSync(testcasePath + fname + '.v', 'utf-8').toString(); + const v = fs.readFileSync( + testcasePath + fname + '.v', 'utf-8' + ).toString(); loadNotebook(testcasePath + fname + '.wpe').then(() => { /** EXPORTING */ const text = notebook.parseToText(); From efb4dafacba1e1ceca4e15da0b658339c11ac61d Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 18:51:28 +0200 Subject: [PATCH 26/30] Fix test cases surrounding import/exporting --- .../io/blocks/notebook-parse-to-text.spec.js | 10 +- tests/unit/io/coqImport.spec.js | 116 ++++-------------- tests/unit/io/export-to-coq.spec.js | 13 +- .../unit/io/export-to-exercise-sheet.spec.js | 2 +- tests/unit/io/load-notebook.spec.js | 2 +- tests/unit/io/test-notebooks/hint-block.wpn | 2 +- tests/unit/io/test-porting.spec.js | 16 ++- 7 files changed, 44 insertions(+), 117 deletions(-) diff --git a/tests/unit/io/blocks/notebook-parse-to-text.spec.js b/tests/unit/io/blocks/notebook-parse-to-text.spec.js index 571b3a5e..23ffcc2b 100644 --- a/tests/unit/io/blocks/notebook-parse-to-text.spec.js +++ b/tests/unit/io/blocks/notebook-parse-to-text.spec.js @@ -1,5 +1,4 @@ import Notebook from '../../../../src/io/notebook'; -import {COQ_SPECIAL_COMMENT_START} from '../../../../src/io/notebook'; const chai = require('chai'); const expect = chai.expect; @@ -34,7 +33,7 @@ describe('Notebook parse to text ', () => { notebook.blocks.push( notebook.createTextBlock(code, false)); const output = notebook.parseToText(); - expect(output.trim()).to.equal(COQ_SPECIAL_COMMENT_START + code + '*)'); + expect(output.trim()).to.equal('(** ' + code + ' *)'); done(); }); @@ -44,7 +43,6 @@ describe('Notebook parse to text ', () => { notebook.blocks.push(notebook.createHintBlock(code)); const output = notebook.parseToText(); expect(output).includes(code); - expect(output).to.endsWith('\n'); done(); }); @@ -52,10 +50,8 @@ describe('Notebook parse to text ', () => { it('should parse input blocks to comments with text', (done) => { notebook.blocks = notebook.blocks.concat(notebook.createInputArea('1')); const output = notebook.parseToText(); - expect(output.trim()).startsWith('(*'); - expect(output.trim()).endsWith('*)'); - expect(output).includes('(* Start of input area *)'); - expect(output).includes('(* End of input area *)'); + expect(output).includes('(** INPUT-START *)'); + expect(output).includes('(** INPUT-END *)'); done(); }); diff --git a/tests/unit/io/coqImport.spec.js b/tests/unit/io/coqImport.spec.js index b643111a..acf2a6ab 100644 --- a/tests/unit/io/coqImport.spec.js +++ b/tests/unit/io/coqImport.spec.js @@ -1,5 +1,5 @@ import Notebook from '../../../src/io/notebook'; -import {COQ_SPECIAL_COMMENT_START} from '../../../src/io/notebook'; +import {coqToWp} from '../../../src/io/notebook'; const chai = require('chai'); const expect = chai.expect; @@ -42,7 +42,7 @@ describe('Parse coq to code and text', () => { (done) => { const input = 'Notation "cv_to" := Un_cv.'; - const blocks = notebook.coqToCodeAndText(input); + const blocks = coqToWp(input); expect(blocks).to.be.an('array').that.has.lengthOf(1); expect(blocks[0]).to.have.property('type', 'code'); @@ -50,7 +50,7 @@ describe('Parse coq to code and text', () => { done(); }); - it('should split to different code cells before keywords', + it('should split to different code cells before (***)', (done) => { const lemmaStatement = 'Lemma trans (A B C :Prop): ' + '(A -> B) -> (B->C) -> A -> C.\n'; @@ -62,9 +62,9 @@ describe('Parse coq to code and text', () => { 'specialize (G H).\n' + 'apply G.\n' + 'Qed.'; - const input = lemmaStatement + lemmaProof; + const input = lemmaStatement + '(***)\n' + lemmaProof; - const blocks = notebook.coqToCodeAndText(input); + const blocks = coqToWp(input); expect(blocks).to.be.an('array').that.has.lengthOf(2); expect(blocks[0]).to.have.property('type', 'code'); @@ -76,9 +76,9 @@ describe('Parse coq to code and text', () => { it('should give just one text block if there are only comments', (done) => { - const input = COQ_SPECIAL_COMMENT_START + ' Just a comment *)'; + const input = '(**Just a comment*)'; - const blocks = notebook.coqToCodeAndText(input); + const blocks = coqToWp(input); expect(blocks).to.be.an('array').that.has.lengthOf(1); expect(blocks[0]).to.have.property('type', 'text'); @@ -88,11 +88,11 @@ describe('Parse coq to code and text', () => { it('should give one text and one code block with code first', (done) => { const code = 'Lemma trans (A B C :Prop): (A -> B) -> (B->C) -> A -> C.'; - const comment = ' Just a comment '; + const comment = 'Just a comment'; - const input = code + COQ_SPECIAL_COMMENT_START + comment + '*)'; + const input = code + '(**' + comment + '*)'; - const blocks = notebook.coqToCodeAndText(input); + const blocks = coqToWp(input); expect(blocks).to.be.an('array').that.has.lengthOf(2); expect(blocks[0]).to.have.property('type', 'code'); @@ -104,11 +104,11 @@ describe('Parse coq to code and text', () => { it('should give one text and one code block with text first', (done) => { const code = 'Lemma trans (A B C :Prop): (A -> B) -> (B->C) -> A -> C.'; - const comment = ' Just a comment '; + const comment = 'Just a comment'; - const input = COQ_SPECIAL_COMMENT_START + comment + '*)' + code; + const input = '(**' + comment + '*)' + code; - const blocks = notebook.coqToCodeAndText(input); + const blocks = coqToWp(input); expect(blocks).to.be.an('array').that.has.lengthOf(2); expect(blocks[0]).to.have.property('type', 'text'); @@ -120,11 +120,11 @@ describe('Parse coq to code and text', () => { it('should give one text and two code blocks with text in the middle', (done) => { const code = 'Lemma trans (A B C :Prop): (A -> B) -> (B->C) -> A -> C.'; - const comment = ' Just a comment '; + const comment = 'Just a comment'; - const input = code + COQ_SPECIAL_COMMENT_START + comment + '*)' + code; + const input = code + '(**' + comment + '*)' + code; - const blocks = notebook.coqToCodeAndText(input); + const blocks = coqToWp(input); expect(blocks).to.be.an('array').that.has.lengthOf(3); expect(blocks[0]).to.have.property('type', 'code'); @@ -136,25 +136,11 @@ describe('Parse coq to code and text', () => { it('should give one text block with nested comments', (done) => { - const comment = '(* Just a comment *)'; - - const input = COQ_SPECIAL_COMMENT_START + comment + '*)'; - - const blocks = notebook.coqToCodeAndText(input); - - expect(blocks).to.be.an('array').that.has.lengthOf(1); - expect(blocks[0]).to.have.property('type', 'text'); - expect(blocks[0]).to.have.property('text', comment); - done(); - }); - - it('should give one text block for non closed comment', - (done) => { - const comment = ' Just a comment '; + const comment = '(*Just a comment*)'; - const input = COQ_SPECIAL_COMMENT_START + comment; + const input = '(**' + comment + '*)'; - const blocks = notebook.coqToCodeAndText(input); + const blocks = coqToWp(input); expect(blocks).to.be.an('array').that.has.lengthOf(1); expect(blocks[0]).to.have.property('type', 'text'); @@ -162,62 +148,14 @@ describe('Parse coq to code and text', () => { done(); }); - it('should give one text block after a code block for non closed comment', - (done) => { - const code = 'Lemma trans (A B C :Prop): (A -> B) -> (B->C) -> A -> C.'; - const comment = ' Just a comment '; - - const input = code + COQ_SPECIAL_COMMENT_START + comment; - - const blocks = notebook.coqToCodeAndText(input); - - expect(blocks).to.be.an('array').that.has.lengthOf(2); - expect(blocks[0]).to.have.property('type', 'code'); - expect(blocks[1]).to.have.property('type', 'text'); - expect(blocks[1]).to.have.property('text', comment); - done(); - }); + // it('should remove all hard returns', (done) => { + // const input = + // 'Lemma zero_eq_zero : 0 = 0.\r\nProof.\n\rreflexivity.\n\rQed.'; - it('should give one text block non closed comment with nesting', - (done) => { - const code = 'Lemma trans (A B C :Prop): (A -> B) -> (B->C) -> A -> C.'; - const comment = ' Just a comment (* Nested comment *)'; + // const blocks = coqToWp(input); - const input = code + COQ_SPECIAL_COMMENT_START + comment; - - const blocks = notebook.coqToCodeAndText(input); - - expect(blocks).to.be.an('array').that.has.lengthOf(2); - expect(blocks[0]).to.have.property('type', 'code'); - expect(blocks[1]).to.have.property('type', 'text'); - expect(blocks[1]).to.have.property('text', comment); - done(); - }); - - it('should not revert "( *", "* )" in comments', - (done) => { - // export -> import does not need to give the same result - const comment = ' Just a comment ( * Nested comment * )'; - - const input = COQ_SPECIAL_COMMENT_START + comment + '*)'; - - const blocks = notebook.coqToCodeAndText(input); - - expect(blocks).to.be.an('array').that.has.lengthOf(1); - expect(blocks[0]).to.have.property('type', 'text'); - expect(blocks[0]).to.have.property('text', comment); - done(); - }); - - it('should remove all hard returns', (done) => { - const input = - 'Lemma zero_eq_zero : 0 = 0.\r\nProof.\n\rreflexivity.\n\rQed.'; - - const blocks = notebook.coqToCodeAndText(input); - - expect(blocks).to.be.an('array').that.has.lengthOf(2); - expect(blocks[0].text.indexOf('\r')).to.equal(-1); - expect(blocks[1].text.indexOf('\r')).to.equal(-1); - done(); - }); + // expect(blocks).to.be.an('array').that.has.lengthOf(1); + // expect(blocks[0].text.indexOf('\r')).to.equal(-1); + // done(); + // }); }); diff --git a/tests/unit/io/export-to-coq.spec.js b/tests/unit/io/export-to-coq.spec.js index ce894dd3..74222478 100644 --- a/tests/unit/io/export-to-coq.spec.js +++ b/tests/unit/io/export-to-coq.spec.js @@ -1,5 +1,4 @@ import Notebook from '../../../src/io/notebook'; -import {COQ_SPECIAL_COMMENT_START} from '../../../src/io/notebook'; const fs = require('fs'); const chai = require('chai'); @@ -79,8 +78,7 @@ if (process.env.NODE_ENV !== 'coverage') { }).then(() => { const data = fs.readFileSync(writeFile, 'utf-8'); fs.unlinkSync(writeFile); - expect(data).to.include(COQ_SPECIAL_COMMENT_START - + 'This is some sample text.*)'); + expect(data).to.include('(** This is some sample text. *)'); done(); }).catch(done); }); @@ -93,8 +91,7 @@ if (process.env.NODE_ENV !== 'coverage') { }).then(() => { const data = fs.readFileSync(writeFile, 'utf-8'); fs.unlinkSync(writeFile); - expect(data).to.include(COQ_SPECIAL_COMMENT_START - + 'It\'s really not that hard.*)'); + expect(data).to.include(''); done(); }).catch(done); }); @@ -108,10 +105,8 @@ if (process.env.NODE_ENV !== 'coverage') { }).then(() => { const data = fs.readFileSync(writeFile, 'utf-8'); fs.unlinkSync(writeFile); - expect(data).to.include(COQ_SPECIAL_COMMENT_START - + '(* Start of input area *)*)'); - expect(data).to.include(COQ_SPECIAL_COMMENT_START - + '(* End of input area *)*)'); + expect(data).to.include('(** INPUT-START *)'); + expect(data).to.include('(** INPUT-END *)'); done(); }).catch(done); }); diff --git a/tests/unit/io/export-to-exercise-sheet.spec.js b/tests/unit/io/export-to-exercise-sheet.spec.js index dcd5183a..791d6356 100644 --- a/tests/unit/io/export-to-exercise-sheet.spec.js +++ b/tests/unit/io/export-to-exercise-sheet.spec.js @@ -101,7 +101,7 @@ if (process.env.NODE_ENV !== 'coverage') { const writeFile = readFile + '.temp'; const expected = { type: 'hint', - text: 'It\'s really not that hard.', + text: 'Click to open hint or something.\n\nHint itself.', }; loadNotebook(readFile).then(() => { diff --git a/tests/unit/io/load-notebook.spec.js b/tests/unit/io/load-notebook.spec.js index d4be709f..c694e61c 100644 --- a/tests/unit/io/load-notebook.spec.js +++ b/tests/unit/io/load-notebook.spec.js @@ -67,7 +67,7 @@ if (process.env.NODE_ENV !== 'coverage') { const file = notebookPath + 'hint-block.wpn'; const expected = { type: 'hint', - text: 'It\'s really not that hard.', + text: 'Click to open hint or something.\n\nHint itself.', }; loadNotebook(file).then(() => { diff --git a/tests/unit/io/test-notebooks/hint-block.wpn b/tests/unit/io/test-notebooks/hint-block.wpn index 5feb16dd..d5debf07 100644 --- a/tests/unit/io/test-notebooks/hint-block.wpn +++ b/tests/unit/io/test-notebooks/hint-block.wpn @@ -3,7 +3,7 @@ "blocks": [ { "type": "hint", - "text": "It's really not that hard." + "text": "Click to open hint or something.\n\nHint itself." } ] } diff --git a/tests/unit/io/test-porting.spec.js b/tests/unit/io/test-porting.spec.js index cb00f51a..f53210cd 100644 --- a/tests/unit/io/test-porting.spec.js +++ b/tests/unit/io/test-porting.spec.js @@ -19,17 +19,15 @@ const notebook = new Notebook; * or rejects when a read or parse error occurs */ function loadNotebook(file) { - notebook.filePath = file; - return new Promise((resolve, reject) => { notebook.read( - () => { - resolve(); - }, - (err) => { - reject(err); - } + () => { + resolve(); + }, + (err) => { + reject(err); + } ); }); } @@ -40,7 +38,7 @@ if (process.env.NODE_ENV !== 'coverage') { const fname = tests[i]; it('test ' + fname, (done) => { const v = fs.readFileSync( - testcasePath + fname + '.v', 'utf-8' + testcasePath + fname + '.v', 'utf-8' ).toString(); loadNotebook(testcasePath + fname + '.wpe').then(() => { /** EXPORTING */ From 1d1282f77e856d97db38aabc67cd52088ac205e4 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Mon, 25 Apr 2022 18:51:35 +0200 Subject: [PATCH 27/30] bookkeep --- src/io/notebook.js | 1 + 1 file changed, 1 insertion(+) diff --git a/src/io/notebook.js b/src/io/notebook.js index b169e6e1..81ea19e0 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -507,6 +507,7 @@ class Notebook { fs.readFile(filename, callback); } + // TODO: unused function, perhaps in future when WP docs are one big doc. /** * Cuts a string up in an array of strings. The cut points are * exactly at the beginning of the matches of the regular expression keywords From 01ac3f8f09163282fdbdc3ed896a8128d75000cd Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Tue, 26 Apr 2022 14:54:02 +0200 Subject: [PATCH 28/30] Also translate Tutorial.wpn to new syntax --- wrapper/wplib/Notebooks/Tutorial.wpn | 84 ++++++++++++++-------------- 1 file changed, 42 insertions(+), 42 deletions(-) diff --git a/wrapper/wplib/Notebooks/Tutorial.wpn b/wrapper/wplib/Notebooks/Tutorial.wpn index 7f74e42d..e17d728c 100644 --- a/wrapper/wplib/Notebooks/Tutorial.wpn +++ b/wrapper/wplib/Notebooks/Tutorial.wpn @@ -3,7 +3,7 @@ "blocks": [ { "type": "text", - "text": "# Tutorial: Getting used to Waterproof\n\nThis tutorial explains how to get started with Waterproof. The aim of Waterproof is to help learning how to prove mathematical statements.\n\nThis tutorial is in the form of an **exercise sheet** (sometimes we will call it a **notebook**). It is a mix of explanations and exercises in which you can try proving mathematical statements yourself. \n\nThe exercise sheet contains **text cells** (white background) and **code cells** (gray background). So far, we have been writing text, in text cells. But now we will introduce the first code cell.\n" + "text": "* Tutorial: Getting used to Waterproof\n\nThis tutorial explains how to get started with Waterproof. The aim of Waterproof is to help learning how to prove mathematical statements.\n\nThis tutorial is in the form of an ##exercise sheet## (sometimes we will call it a ##notebook##). It is a mix of explanations and exercises in which you can try proving mathematical statements yourself. \n\nThe exercise sheet contains ##text cells## (white background) and ##code cells## (gray background). So far, we have been writing text, in text cells. But now we will introduce the first code cell.\n" }, { "type": "code", @@ -11,15 +11,15 @@ }, { "type": "text", - "text": "The code consists of several *sentences*. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." + "text": "The code consists of several _sentences_. Every sentence finishes with a period. These sentences above are necessary to make the rest of the notebook work." }, { "type": "text", - "text": "\nWe recommend that while you read this notebook, you execute the code sentence-by-sentence by pressing **Alt + ↓** (on MacOS: **Option + ↓** or **⌥ + ↓**). (Alternatively, you can use the buttons on the left, but it is typically much faster to work with keyboard shortcuts.)" + "text": "\nWe recommend that while you read this notebook, you execute the code sentence-by-sentence by pressing ##Alt + ↓## (on MacOS: ##Option + ↓## or ##⌥ + ↓##). (Alternatively, you can use the buttons on the left, but it is typically much faster to work with keyboard shortcuts.)" }, { "type": "text", - "text": "* 1. Prove a lemma\n\nIn the following code cell, we introduce a **lemma**. We called the lemma **example_reflexivity**." + "text": "* 1. Prove a lemma\n\nIn the following code cell, we introduce a ##lemma##. We called the lemma ##example_reflexivity##." }, { "type": "code", @@ -27,7 +27,7 @@ }, { "type": "text", - "text": "\nWe will now prove the lemma. We start the proof by writing the sentence `\"Proof.\"` in a code cell." + "text": "\nWe will now prove the lemma. We start the proof by writing the sentence [\"Proof.\"] in a code cell." }, { "type": "code", @@ -35,11 +35,11 @@ }, { "type": "text", - "text": "\nExecute the code sentence after sentence (press **Alt + ↓** or **Option + ↓**), until a blue checkmark appears in place of the period after `Proof.`. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under **Proof progress** (either on the right of the screen, or down below) appeared what we need to show, namely `(0=0)`. We will often refer to this as the current **goal**." + "text": "\nExecute the code sentence after sentence (press ##Alt + ↓## or ##Option + ↓##), until a blue checkmark appears in place of the period after [Proof.]. The checkmark means that Waterproof has checked every sentence before the checkmark. Note how in the part of the screen under ##Proof progress## (either on the right of the screen, or down below) appeared what we need to show, namely [(0=0)]. We will often refer to this as the current ##goal##." }, { "type": "text", - "text": "\nNext, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence `\"We conclude that (0=0).\"` and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as **applying a tactic.**" + "text": "\nNext, we tell Waterproof what to do to prove the lemma. For such a simple statement, we can just write and execute the sentence [\"We conclude that (0=0).\"] and Waterproof will check automatically that this holds. We will often refer to executing such a sentence as ##applying a tactic.##" }, { "type": "code", @@ -47,7 +47,7 @@ }, { "type": "text", - "text": "\nExecute the above sentence, with **Alt + ↓**, until the checkmark appears after the sentence. Note how under proof progress it says `Done.`. The lemma is proved! We close the proof by writing `Qed.`." + "text": "\nExecute the above sentence, with ##Alt + ↓##, until the checkmark appears after the sentence. Note how under proof progress it says [Done.]. The lemma is proved! We close the proof by writing [Qed.]." }, { "type": "code", @@ -55,11 +55,11 @@ }, { "type": "text", - "text": "\n**HINT:** When writing `We conclude that (...)`, it is important that at the place of the dots you write the current goal (which you can see under **Proof progress**), and not another statement.\n\n**HINT:** If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in." + "text": "\n##HINT:## When writing [We conclude that (...)], it is important that at the place of the dots you write the current goal (which you can see under ##Proof progress##), and not another statement.\n\n##HINT:## If you click on the hammer symbol on the top right, a list of tactics will open. You can click on one of the icons next to the tactics, and the tactic will be either be copied to the clipboard or inserted in the text at the place of the cursor, usually with some placeholders that you need to fill in." }, { "type": "text", - "text": "** Try it yourself: prove a lemma\n\nYou can now try this for yourself. We prepared a lemma below, that we named **exercise_reflexivity**." + "text": "** Try it yourself: prove a lemma\n\nYou can now try this for yourself. We prepared a lemma below, that we named ##exercise_reflexivity##." }, { "type": "code", @@ -67,7 +67,7 @@ }, { "type": "text", - "text": "The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing **Alt + c** (On MacOS: **Ctrl + c**), and add a text cell by pressing **Alt + t** (On MacOS: **Ctrl + t**).\n\nYou can also change the text that is already there between the blue brackets by clicking on it.\n\nBelow we already added one code cell, which says `Admitted.`. Executing that code cell (**Alt + ↓**), will also make the proof progress turn to `Done.` **However,** in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise.\n\nAfter you have found a proof, replace the `Admitted.` by `Qed.` (click on the code cell and change the sentence)." + "text": "The blue brackets below delineate an input area. You can freely work there. Move the mouse just below the first blue bracket until a blue, horizontal line appears and click on it. Then, you can add a code cell by pressing ##Alt + c## (On MacOS: ##Ctrl + c##), and add a text cell by pressing ##Alt + t## (On MacOS: ##Ctrl + t##).\n\nYou can also change the text that is already there between the blue brackets by clicking on it.\n\nBelow we already added one code cell, which says [Admitted.]. Executing that code cell (##Alt + ↓##), will also make the proof progress turn to [Done.] ##However,## in that case it is not proven but assumed as an axiom. We do this so you can continue executing the notebook even if you cannot solve the exercise.\n\nAfter you have found a proof, replace the [Admitted.] by [Qed.] (click on the code cell and change the sentence)." }, { "type": "input", @@ -76,7 +76,7 @@ }, { "type": "text", - "text": "Write your solution here, then change the `Admitted.` below to `Qed.`." + "text": "Write your solution here, then change the [Admitted.] below to [Qed.]." }, { "type": "code", @@ -97,7 +97,7 @@ }, { "type": "text", - "text": "> **NOTE:** the notation $x : ℝ$ means $x$ is in $\\mathbb{R}$ (or more accurately, $x$ is of type $\\mathbb{R}$) may be unfamiliar to you, and you may be more familiar with the notation $x ∈ \\reals$. This difference is due to the fact that Waterproof is built on **type theory** and not on set theory. \n\n**HINT:** You can insert characters such as ℝ either from the symbol menu that opens when clicking on 'Σ' in the top right corner, or you can write '\\reals' until a menu pops up and press enter. Make sure that the code reads 'ℝ' and not '\\reals' itself. For many other unicode characters you can use a backslash command as well." + "text": "> ##NOTE:## the notation $x : ℝ$ means $x$ is in $\\mathbb{R}$ (or more accurately, $x$ is of type $\\mathbb{R}$) may be unfamiliar to you, and you may be more familiar with the notation $x ∈ \\reals$. This difference is due to the fact that Waterproof is built on ##type theory## and not on set theory. \n\n##HINT:## You can insert characters such as ℝ either from the symbol menu that opens when clicking on 'Σ' in the top right corner, or you can write '\\reals' until a menu pops up and press enter. Make sure that the code reads 'ℝ' and not '\\reals' itself. For many other unicode characters you can use a backslash command as well." }, { "type": "code", @@ -105,7 +105,7 @@ }, { "type": "text", - "text": "\nTo show a statement like \"for all $x : \\mathbb{R}$, ...\", you first need to take an arbitrary $x : \\mathbb{R}$, and then continue showing ... . We do this by writing and executing the following sentence, i.e. by applying the following **tactic**." + "text": "\nTo show a statement like \"for all $x : \\mathbb{R}$, ...\", you first need to take an arbitrary $x : \\mathbb{R}$, and then continue showing ... . We do this by writing and executing the following sentence, i.e. by applying the following ##tactic##." }, { "type": "code", @@ -129,7 +129,7 @@ }, { "type": "text", - "text": "\n**HINT:** If you would like to get a hint on what you need to do, you can write and execute the sentence `Help.`" + "text": "\n##HINT:## If you would like to get a hint on what you need to do, you can write and execute the sentence [Help.]" }, { "type": "code", @@ -137,7 +137,7 @@ }, { "type": "text", - "text": "\n\n**HINT:** We recommend that always after you write down a sentence, you immediately execute it (**Alt + ↓**)." + "text": "\n\n##HINT:## We recommend that always after you write down a sentence, you immediately execute it (##Alt + ↓##)." }, { "type": "input", @@ -146,7 +146,7 @@ }, { "type": "text", - "text": "Write your solution here. After you have found a proof, remember to change the `Admitted.` below to `Qed.`." + "text": "Write your solution here. After you have found a proof, remember to change the [Admitted.] below to [Qed.]." }, { "type": "code", @@ -159,7 +159,7 @@ }, { "type": "text", - "text": "* 3. Show *there-exists* statements: choose values\n\nIf you want to show that *there exists* $y : \\mathbb{R}$ such that $(\\dots)$, you need to **choose** a candidate for $y$, and continue showing $(\\dots)$ with your choice." + "text": "* 3. Show *there-exists* statements: choose values\n\nIf you want to show that *there exists* $y : \\mathbb{R}$ such that $(\\dots)$, you need to ##choose## a candidate for $y$, and continue showing $(\\dots)$ with your choice." }, { "type": "code", @@ -171,7 +171,7 @@ }, { "type": "text", - "text": "\nWe first choose $y:=2$ by using the tactic `Choose y := ((* value *)).`." + "text": "\nWe first choose $y:=2$ by using the tactic [Choose y := ((* value *)).]." }, { "type": "code", @@ -179,7 +179,7 @@ }, { "type": "text", - "text": "\n(In this particular case we could also have written `Choose y := 2`, but in general the brackets are important.)\n\nWe now need to show that (y<3) (see **Proof progress** after executing the previous sentence). We can record this for our own convenience." + "text": "\n(In this particular case we could also have written [Choose y := 2], but in general the brackets are important.)\n\nWe now need to show that (y<3) (see ##Proof progress## after executing the previous sentence). We can record this for our own convenience." }, { "type": "code", @@ -187,7 +187,7 @@ }, { "type": "text", - "text": "\nIn other words, we need to show that ($2 < 3$). We can also use the `We need to show that ` tactic to slightly reformulate the goal." + "text": "\nIn other words, we need to show that ($2 < 3$). We can also use the [We need to show that] tactic to slightly reformulate the goal." }, { "type": "code", @@ -319,7 +319,7 @@ }, { "type": "text", - "text": "\nIf you now execute the code up to previous sentence, you can see in the **Proof progress** that we need to show `a < 0 ⇒ -a > 0.` Remembering the rules for brackets, this means:" + "text": "\nIf you now execute the code up to previous sentence, you can see in the ##Proof progress## that we need to show [a < 0 ⇒ -a > 0.] Remembering the rules for brackets, this means:" }, { "type": "code", @@ -335,7 +335,7 @@ }, { "type": "text", - "text": "\nThe **name** of this assumption is in this case **a_lt_0**. What you are actually assuming is written after the colon, namely **a < 0**. Note how after executing the sentence, the assumption $a < 0$ is added under **Proof progress** with the name **a_lt_0**.\n\nWe finish the proof." + "text": "\nThe ##name## of this assumption is in this case ##a_lt_0##. What you are actually assuming is written after the colon, namely ##a < 0##. Note how after executing the sentence, the assumption $a < 0$ is added under ##Proof progress## with the name ##a_lt_0##.\n\nWe finish the proof." }, { "type": "code", @@ -369,7 +369,7 @@ }, { "type": "text", - "text": "* 6. Chains of (in)equalities\n\nAs a last step of a proof in Analysis, we often have a chain of (in)equalities. Consider for instance a case in which we would like to show that for all $ε : \\mathbb{R}$, if $ε > 0$ then $\\min(\\epsilon, 1) ≤ 2$. \n\nHere are the statement and a possible proof in Waterproof. Note that we need to write `Rmin x y` for the minimum of two real numbers $x$ and $y$." + "text": "* 6. Chains of (in)equalities\n\nAs a last step of a proof in Analysis, we often have a chain of (in)equalities. Consider for instance a case in which we would like to show that for all $ε : \\mathbb{R}$, if $ε > 0$ then $\\min(\\epsilon, 1) ≤ 2$. \n\nHere are the statement and a possible proof in Waterproof. Note that we need to write [Rmin x y] for the minimum of two real numbers $x$ and $y$." }, { "type": "code", @@ -381,7 +381,7 @@ }, { "type": "text", - "text": "\nNote how we used special notation for the chain of inequalities\n\n``\n(& Rmin ε 1 &≤ 1\n &< 2).\n``\n\nWe think of this statement that **and** `Rmin ε 1 ≤ 1` **and** `1 < 2`. \n\n\n**IMPORTANT**: Here are a few issues to pay attention to:\n- After opening the first parenthesis, you need to write a '&' sign.\n- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign.\n- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported." + "text": "\nNote how we used special notation for the chain of inequalities\n\n``\n(& Rmin ε 1 &≤ 1\n &< 2).\n``\n\nWe think of this statement that ##and## [Rmin ε 1 ≤ 1] ##and## [1 < 2]. \n\n\n##IMPORTANT##: Here are a few issues to pay attention to:\n- After opening the first parenthesis, you need to write a '&' sign.\n- Directly in front of every comparison operator (such as '≤'), you also need to put the '&' sign.\n- Chains of inequalities go from smaller to larger. So only $=$, $≤$ and $<$ are supported." }, { "type": "text", @@ -393,7 +393,7 @@ }, { "type": "hint", - "text": "Click to open hint.\n\nAt the end of your proof, use the following chain of inequalities \n\n```\nRmin (ε / 2) 1 ≤ ε / 2 < ε\n```\n\nbut pay attention to the issues mentioned above: in particular use the '&' sign at the appropriate places." + "text": "Click to open hint.\n\nAt the end of your proof, use the following chain of inequalities \n\n[[\nRmin (ε / 2) 1 ≤ ε / 2 < ε\n]]\n\nbut pay attention to the issues mentioned above: in particular use the '&' sign at the appropriate places." }, { "type": "input", @@ -469,7 +469,7 @@ }, { "type": "text", - "text": "* 8. Forward reasoning in smaller steps\n\nSometimes, the step to what you need to show is too big for Waterproof to find a proof. In that case, the tactic `We conclude that (...).` will not find a proof. Then it often helps to make smaller steps.\n\nHere is an example." + "text": "* 8. Forward reasoning in smaller steps\n\nSometimes, the step to what you need to show is too big for Waterproof to find a proof. In that case, the tactic [We conclude that (...).] will not find a proof. Then it often helps to make smaller steps.\n\nHere is an example." }, { "type": "code", @@ -481,7 +481,7 @@ }, { "type": "text", - "text": "\nWe now make an intermediate step. We let Waterproof automatically show that `(Rmax ε 1 ≥ 1)`, and we call that statement `Rmax_gt_1`." + "text": "\nWe now make an intermediate step. We let Waterproof automatically show that [(Rmax ε 1 ≥ 1)], and we call that statement [Rmax_gt_1]." }, { "type": "code", @@ -497,7 +497,7 @@ }, { "type": "text", - "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called `Rmax_r`.\n\n```\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n```\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n```\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n (* proof of claim *)\n}\n```" + "text": "\nSometimes, you also need to tell Waterproof what lemma to use in proving the intermediate step. The following line would tell Waterproof to use the lemma called [Rmax_r].\n\n[[\nBy Rmax_r it holds that\n Rmax_gt_1 : (Rmax ε 1 ≥ 1). \n]]\n\nFor very difficult statements, it may happen that Waterproof cannot find a proof even when providing the name of a lemma. In that case you can first make an intermediate claim.\n\n[[\nWe claim that Rmax_gt_1 : (Rmax ε 1 ≥ 1).\n{\n (* proof of claim *)\n}\n]]" }, { "type": "text", @@ -527,7 +527,7 @@ }, { "type": "text", - "text": "* 9. Use a *for-all* statement\n\nA special case of the above is when you would like to *use* a for-all statement, as in the example below." + "text": "* 9. Use a _for-all_ statement\n\nA special case of the above is when you would like to _use_ a for-all statement, as in the example below." }, { "type": "code", @@ -539,7 +539,7 @@ }, { "type": "text", - "text": "We can now **use** the statement that we called `del_cond` with $δ = 1/2$. We can do this by substituting $\\delta = 1/2$ as follows." + "text": "We can now ##use## the statement that we called [del_cond] with $δ = 1/2$. We can do this by substituting $\\delta = 1/2$ as follows." }, { "type": "code", @@ -547,7 +547,7 @@ }, { "type": "text", - "text": "Similarly, we can use the statement that we called `eps_cond`. We can also indicate explicitly that we choose $ε = 1/2$ in the statement by writing `By (eps_cond (1/2)) ...` as in" + "text": "Similarly, we can use the statement that we called [eps_cond]. We can also indicate explicitly that we choose $ε = 1/2$ in the statement by writing [By (eps_cond (1/2)) ...] as in" }, { "type": "code", @@ -581,7 +581,7 @@ }, { "type": "text", - "text": "* 10. Use a *there-exists* statement\n\nIn this example we show how to **use** a there-exists statement (when you know it holds)." + "text": "* 10. Use a _there-exists_ statement\n\nIn this example we show how to ##use## a there-exists statement (when you know it holds)." }, { "type": "code", @@ -605,7 +605,7 @@ }, { "type": "text", - "text": "** Try it yourself: use a *there-exists* statement" + "text": "** Try it yourself: use a _there-exists_ statement" }, { "type": "code", @@ -667,7 +667,7 @@ }, { "type": "text", - "text": "\nInstead of writing `Contradiction.` you can also write `↯.`. You can get the symbol `↯` with the backslash-command `\\contradiction`." + "text": "\nInstead of writing [Contradiction.] you can also write [↯.]. You can get the symbol [↯] with the backslash-command [\\contradiction]." }, { "type": "text", @@ -725,7 +725,7 @@ }, { "type": "hint", - "text": "Click to open hint.\n\nDistinguish between cases `x < y` and `x ≥ y`." + "text": "Click to open hint.\n\nDistinguish between cases [x < y] and [x ≥ y]." }, { "type": "input", @@ -767,7 +767,7 @@ }, { "type": "text", - "text": "\nNow the proof splits into two parts, one for each statement. We need to indicate these two parts using bullet points. They can be indicated by any of `-`, `+`, `*`, `--` etc.. You can use a bulleted list inside of a bulleted list." + "text": "\nNow the proof splits into two parts, one for each statement. We need to indicate these two parts using bullet points. They can be indicated by any of [-], [+], [*], [--] etc.. You can use a bulleted list inside of a bulleted list." }, { "type": "code", @@ -855,7 +855,7 @@ }, { "type": "text", - "text": "* 15. Proof by induction\n\nThe following example shows how one could use mathematical induction to show a statement of the form\n\n $$∀ k : ℕ, ... $$\n\nNote that Waterproof will usually interpret any statement such as an inequality `n(k +1 ) > n k` as a statement comparing real numbers, while in this exercise we need statements that compare natural numbers. To indicate this, we have to write `(n (k+1) > n k)%nat` instead." + "text": "* 15. Proof by induction\n\nThe following example shows how one could use mathematical induction to show a statement of the form\n\n $$∀ k : ℕ, ... $$\n\nNote that Waterproof will usually interpret any statement such as an inequality [n(k +1 ) > n k] as a statement comparing real numbers, while in this exercise we need statements that compare natural numbers. To indicate this, we have to write [(n (k+1) > n k)%nat] instead." }, { "type": "code", @@ -901,7 +901,7 @@ }, { "type": "text", - "text": "* 16. Expand definitions\n\nIt happens that you need to use a definition of some object in Waterproof, for instance the definition of a function. Here is the definition of a function called `square`." + "text": "* 16. Expand definitions\n\nIt happens that you need to use a definition of some object in Waterproof, for instance the definition of a function. Here is the definition of a function called [square]." }, { "type": "code", @@ -921,7 +921,7 @@ }, { "type": "text", - "text": "At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing `We need to show that (x^2 ≥ 0).`, or we could write \n\n```\nWe conclude that\n (& square x &= x^2\n &≥ 0). \n```\nHowever these options aren't available if you do not know the definition of `square`. In that case you could write" + "text": "At this stage, Waterproof does not know how to continue. We could immediately reformulate the goal by writing [We need to show that (x^2 ≥ 0).], or we could write \n\n[[\nWe conclude that\n (& square x &= x^2\n &≥ 0). \n]]\nHowever these options aren't available if you do not know the definition of [square]. In that case you could write" }, { "type": "code", @@ -929,7 +929,7 @@ }, { "type": "text", - "text": "\nNow Waterproof has expanded the definition of `square` in the goal. It is always important to keep the proof readable, so that's why Waterproof asks you now to also reformulate the goal." + "text": "\nNow Waterproof has expanded the definition of [square] in the goal. It is always important to keep the proof readable, so that's why Waterproof asks you now to also reformulate the goal." }, { "type": "code", @@ -937,7 +937,7 @@ }, { "type": "text", - "text": "You can also expand the definition in a hypothesis. For instance,\n```\nExpand the definition of square in H.\n```\nwould expand the definition of `square` in the hypothesis with the name `H`." + "text": "You can also expand the definition in a hypothesis. For instance,\n[[\nExpand the definition of square in H.\n]]\nwould expand the definition of [square] in the hypothesis with the name [H]." }, { "type": "text", From f82405dd8a5422ec630ae267f10892aadc613f49 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Thu, 2 Jun 2022 10:57:17 +0200 Subject: [PATCH 29/30] Fix problems with line endings in test case --- tests/unit/io/test-porting.spec.js | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/tests/unit/io/test-porting.spec.js b/tests/unit/io/test-porting.spec.js index f53210cd..938903df 100644 --- a/tests/unit/io/test-porting.spec.js +++ b/tests/unit/io/test-porting.spec.js @@ -7,7 +7,7 @@ chai.use(require('chai-string')); const expect = chai.expect; const testcasePath = './tests/unit/io/test-porting/'; -const tests = ['tutorial']; +const tests = ['tutorial', 'block_structure']; const notebook = new Notebook; @@ -32,6 +32,10 @@ function loadNotebook(file) { }); } +function normalizeLineEndings(s) { + return s.replace(/\r/g, '').replace(/\n/g, ''); +} + if (process.env.NODE_ENV !== 'coverage') { describe('Full standardized test suite', () => { for (let i = 0; i < tests.length; i++) { @@ -43,7 +47,9 @@ if (process.env.NODE_ENV !== 'coverage') { loadNotebook(testcasePath + fname + '.wpe').then(() => { /** EXPORTING */ const text = notebook.parseToText(); - expect(text).to.equal(v); + expect(normalizeLineEndings(text)).to.equal( + normalizeLineEndings(v) + ); /** IMPORTING */ const blocks = coqToWp(v); @@ -53,7 +59,9 @@ if (process.env.NODE_ENV !== 'coverage') { const b = notebook.blocks[j]; expect(a.type).to.equal(b.type); if (b.text !== undefined) { - expect(a.text).to.equal(b.text.trim()); + expect(normalizeLineEndings(a.text)).to.equal( + normalizeLineEndings(b.text.trim()) + ); } expect(a.start).to.equal(b.start); // expect(a.id).to.equal(b.id); From fda095b55925878630c511bb6437055ac4572194 Mon Sep 17 00:00:00 2001 From: SeanMcCarren Date: Thu, 2 Jun 2022 10:57:31 +0200 Subject: [PATCH 30/30] block structure test case --- tests/unit/io/test-porting/block_structure.v | 7 +++++ .../unit/io/test-porting/block_structure.wpe | 27 +++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 tests/unit/io/test-porting/block_structure.v create mode 100644 tests/unit/io/test-porting/block_structure.wpe diff --git a/tests/unit/io/test-porting/block_structure.v b/tests/unit/io/test-porting/block_structure.v new file mode 100644 index 00000000..ec2f8bb7 --- /dev/null +++ b/tests/unit/io/test-porting/block_structure.v @@ -0,0 +1,7 @@ +(** text block *) +code +(** before + +after *) +(** INPUT-START *) +(** INPUT-END *) \ No newline at end of file diff --git a/tests/unit/io/test-porting/block_structure.wpe b/tests/unit/io/test-porting/block_structure.wpe new file mode 100644 index 00000000..dea61924 --- /dev/null +++ b/tests/unit/io/test-porting/block_structure.wpe @@ -0,0 +1,27 @@ +{ + "exerciseSheet": true, + "blocks": [ + { + "type": "text", + "text": "text block" + }, + { + "type": "code", + "text": "code" + }, + { + "type": "hint", + "text": "before\n\nafter" + }, + { + "type": "input", + "start": true, + "id": "input-1" + }, + { + "type": "input", + "start": false, + "id": "input-1" + } + ] +} \ No newline at end of file