diff --git a/src/editpage/components/blocks/WpBlock.vue b/src/editpage/components/blocks/WpBlock.vue index 51cae78b..14e8093f 100644 --- a/src/editpage/components/blocks/WpBlock.vue +++ b/src/editpage/components/blocks/WpBlock.vue @@ -50,7 +50,22 @@ export default { }); // Replace coqdoc-style lists (-) with markdown lists (*) converted = converted.replace(/^([ ]*)- /gm, '$1* '); - return md.render(converted); + // Remove coq-comment start & end + 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 + converted = converted.replace(/#<\/?strong>#/g, '**'); + // Translate italics to md + converted = converted.replace(/\W_/g, ' *'); + converted = converted.replace(/_\W/g, '* '); + + converted = md.render(converted); + return converted; }, renderToSpan: function(text) { let htmlString = this.render(text); 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..81ea19e0 100644 --- a/src/io/notebook.js +++ b/src/io/notebook.js @@ -1,10 +1,6 @@ -const fs = require('fs'); +import {assert} from 'console'; -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 fs = require('fs'); const DEFAULT_BLACKLIST = [ // commands that allow introducing theorems without proof @@ -275,7 +271,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); } /** @@ -343,6 +339,7 @@ class Notebook { } try { + // TODO move this to seperate function, also for coqToWp? this.clearContent(); const read = JSON.parse(data); @@ -503,13 +500,14 @@ class Notebook { this.createCodeBlock(coqText), ]; } else { - this.blocks = this.coqToCodeAndText(coqText); + this.blocks = coqToWp(coqText); } }; 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 @@ -535,88 +533,146 @@ 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; - } - } - - contentLeft = contentLeft.substring(nextComment) - .replace(COQ_SPECIAL_COMMENT_START, ''); - - let startPos = 0; - let endPos = 0; - nextComment = contentLeft.indexOf(COQ_COMMENT_START, startPos); - let commentEnd = contentLeft.indexOf(COQ_COMMENT_END, endPos); - - 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); - } +export default Notebook; - if (commentEnd < 0) { - blocks.push(this.createTextBlock(contentLeft)); - break; +/** + * Importing from .v file according to specification.md + * @param {String} coqCode the input code + * @return {Array} the blocks from the code + */ +function coqToWp(coqCode) { + const blocks = []; // return array + let inInputField = false; + let inputFieldId = 1; + let i = 0; + while (i < coqCode.length) { + let next = coqCode.indexOf('(**', i+3); + if (next === -1) { + next = coqCode.length; + } + const blockContent = coqCode.substring(i, next).trim(); + const finalCommentCloseIndex = blockContent.lastIndexOf('*)'); + if (finalCommentCloseIndex !== -1) { + const coqdoc = blockContent.substring(3, finalCommentCloseIndex).trim(); + if (coqdoc === '') { + // The block could have been (***) or an empty text block. We don't add + // a block in that case. + } else { + 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 = 'input-' + 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 = 'input-' + 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); } - - blocks.push(this.createTextBlock(contentLeft.substring(0, commentEnd))); - contentLeft = contentLeft.substring(commentEnd) - .replace(COQ_COMMENT_END, ''); } - - return blocks; + let startCode; + if (finalCommentCloseIndex === -1) { + startCode = 0; + } else { + startCode = finalCommentCloseIndex + 2; + } + const code = blockContent.substring(startCode).trim(); + if (code !== '') { + const block = {type: 'code', text: code}; + Notebook.setDefaultBlockState(block, inInputField); + blocks.push(block); + } + i = next; } + return blocks; } -export default Notebook; - /** - * Convert blocks into a coq parsable text + * Exporting to .v file according to 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 = []; + let prevBlockType = null; for (const block of blocks) { if (block.type === 'code') { - coqContent += block.text; + if (prevBlockType === 'code') { + blockStrings.push('(***)'); + } + blockStrings.push(block.text); + } 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( + '(** ' + convertToValid(hint[0].trim()) + '\n\n' + + convertToValid(hint[1].trim()) + ' *)' + ); + } else { + throw Error('Unexpected hint block: ' + hint.text); + } } else if (block.type === 'input') { if (block.start) { - coqContent += COQ_SPECIAL_COMMENT_START + COQ_INPUT_START - + COQ_COMMENT_END; + blockStrings.push('(** INPUT-START *)'); } else { - coqContent += COQ_SPECIAL_COMMENT_START + COQ_INPUT_END - + COQ_COMMENT_END; + blockStrings.push('(** INPUT-END *)'); } } else { - coqContent += COQ_SPECIAL_COMMENT_START + block.text + COQ_COMMENT_END; + throw Error('Can not interpret block type ' + block.type); } - coqContent += '\n'; + + prevBlockType = block.type; } - return coqContent; + return blockStrings.join('\n'); +} + +/** + * Convert a block's text to something that is valid. + * @param {string} text + * @return {string} converted 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; + 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 $, %, # + + return converted; } -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..469fde32 --- /dev/null +++ b/src/io/specification.md @@ -0,0 +1,98 @@ +# 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 + +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: + +- 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). + +## 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 triple backticks. (TODO figure out how to color this the same) +- Consecutive `[` and `]` both to backticks. +- \_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 '*') + +--- + +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: + +> (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`. + +TODO: maybe need to start enforcing matching of comments in Waterproof + +### 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 the open comment in `text` if it contains an odd number of quotes. + +### 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 +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.** +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? + +Always import as notebook. So previously exported exercise sheet can become notebook. + +***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*** 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 new file mode 100644 index 00000000..938903df --- /dev/null +++ b/tests/unit/io/test-porting.spec.js @@ -0,0 +1,74 @@ +import Notebook from '../../../src/io/notebook'; +import {coqToWp} from '../../../src/io/notebook'; + +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', 'block_structure']; + +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); + } + ); + }); +} + +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++) { + 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(normalizeLineEndings(text)).to.equal( + normalizeLineEndings(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(normalizeLineEndings(a.text)).to.equal( + normalizeLineEndings(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/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 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 diff --git a/wrapper/assistance/Tutorial.wpe b/wrapper/assistance/Tutorial.wpe index 59b5531e..73b84212 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", @@ -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", @@ -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." @@ -729,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", @@ -771,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", @@ -859,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", @@ -905,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", @@ -925,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", @@ -933,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", @@ -941,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", diff --git a/wrapper/wplib/Notebooks/Tutorial.wpn b/wrapper/wplib/Notebooks/Tutorial.wpn index da3732a1..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", @@ -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." @@ -729,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", @@ -771,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", @@ -859,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", @@ -905,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", @@ -925,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", @@ -933,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", @@ -941,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",