From c30b10b2c4e166c439d2639e2c5300c46f872ebf Mon Sep 17 00:00:00 2001 From: Ben de Vries Date: Sat, 17 Sep 2022 17:54:59 +0200 Subject: [PATCH 1/2] Adding new constraint --- src/js/controller/LogIndController.js | 10 ++++++++++ src/lang/en.json | 2 ++ src/lang/nl.json | 2 ++ 3 files changed, 14 insertions(+) diff --git a/src/js/controller/LogIndController.js b/src/js/controller/LogIndController.js index b77bdc1..c1c1df6 100644 --- a/src/js/controller/LogIndController.js +++ b/src/js/controller/LogIndController.js @@ -602,6 +602,16 @@ export class LogIndController extends ExerciseController { this.updateAlert('logind.error.caseNotRecognized', null, 'error') break } + if (term.includes('not basestep (not recognized)')) { + this.setErrorLocation(['formula-bottom', 'formula-top']) + this.updateAlert('logind.error.baseStepNotRecognized', null, 'error') + break + } + if (term.includes('not ihstep (not recognized)')) { + this.setErrorLocation(['formula-bottom', 'formula-top']) + this.updateAlert('logind.error.IHNotRecognized', null, 'error') + break + } if (term.includes('not an instantiation')) { this.setErrorLocation(['formula-bottom', 'formula-top']) this.updateAlert('logind.error.notInstantiation', null, 'error') diff --git a/src/lang/en.json b/src/lang/en.json index c83f8c3..e859da0 100644 --- a/src/lang/en.json +++ b/src/lang/en.json @@ -439,6 +439,7 @@ }, "completed": "The exercise is finished.", "error": { + "baseStepNotRecognized": "This is not a correct instantiation of a base case", "butBasestep": "This is not [[case]] but a base case for {{identifier}}", "butIhstep": "This is not [[case]] but an induction hypothesis for $${{identifier}}$$", "butInductivestep": "This is not [[case]] but an inductive case for $${{identifier}}$$", @@ -448,6 +449,7 @@ "differentMetaVarsWith": "Use the same metavariable in the first and second expression of the induction hypothesis, so $${{metaVar}}$$ in the second expression.", "doubleCase": "There is already a case $${{case}}$$, you need to prove exactly one case for each connective in the language.", "doubleIH": "You already formulated an induction hypothesis for $${{case}}$$.", + "ihNotRecognized": "This is not a correct induction hypothesis", "incorrect": "The proof contains an error.", "incorrectApplicationIh": "The application of the induction hypothesis is not correct.", "invalidAtomsInInductiveCase": "Do not formulate inductive cases for compositions of atomic formulae, use the variables from the induction hypothesis.", diff --git a/src/lang/nl.json b/src/lang/nl.json index 8842f4a..e735104 100644 --- a/src/lang/nl.json +++ b/src/lang/nl.json @@ -439,6 +439,7 @@ }, "completed": "De uitwerking is compleet", "error": { + "baseStepNotRecognized": "Dit is geen correcte instantiatie van een basisstap", "butBasestep": "Dit is geen [[case]] maar een basis geval voor {{identifier}}", "butIhstep": "Dit is geen [[case]] maar een inductiehypothese voor $${{identifier}}$$", "butInductivestep": "Dit is geen [[case]] maar een inductief geval $${{identifier}}$$", @@ -448,6 +449,7 @@ "differentMetaVarsWith": "Gebruik dezelfde metavariabele in de eerste en tweede expressie van de inductiehypothese, dus een $${{metaVar}}$$ in de tweede expressie", "doubleCase": "Je hebt al een geval $${{case}}$$, voor elk connectief in de taal moet je precies 1 geval bewijzen.", "doubleIH": " je hebt al een inductiehypothese geformuleerd voor $${{case}}$$.", + "ihNotRecognized": "Dit is geen correcte inductiehypothese", "incorrect": "Er is een fout in het bewijs.", "incorrectApplicationIh": "De toepassing van de inductiehypothese is niet correct", "invalidAtomsInInductiveCase": "Formuleer de inductieve gevallen niet voor samenstellingen van atomaire formules, gebruik de variabelen uit de inductiehypothese", From 5717520025e081f783d54699279ba8998bf1205c Mon Sep 17 00:00:00 2001 From: Ben de Vries Date: Mon, 26 Sep 2022 19:34:40 +0200 Subject: [PATCH 2/2] Add constraint for inductive step --- src/js/controller/LogIndController.js | 7 ++++++- src/lang/en.json | 1 + src/lang/nl.json | 1 + 3 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/js/controller/LogIndController.js b/src/js/controller/LogIndController.js index c1c1df6..f98c0d0 100644 --- a/src/js/controller/LogIndController.js +++ b/src/js/controller/LogIndController.js @@ -609,7 +609,12 @@ export class LogIndController extends ExerciseController { } if (term.includes('not ihstep (not recognized)')) { this.setErrorLocation(['formula-bottom', 'formula-top']) - this.updateAlert('logind.error.IHNotRecognized', null, 'error') + this.updateAlert('logind.error.ihNotRecognized', null, 'error') + break + } + if (term.includes('not inductivestep (not recognized)')) { + this.setErrorLocation(['formula-bottom', 'formula-top']) + this.updateAlert('logind.error.inductiveStepNotRecognized', null, 'error') break } if (term.includes('not an instantiation')) { diff --git a/src/lang/en.json b/src/lang/en.json index e859da0..6070b6e 100644 --- a/src/lang/en.json +++ b/src/lang/en.json @@ -452,6 +452,7 @@ "ihNotRecognized": "This is not a correct induction hypothesis", "incorrect": "The proof contains an error.", "incorrectApplicationIh": "The application of the induction hypothesis is not correct.", + "inductiveStepNotRecognized": "This is not a correct instantiation of an inductive step", "invalidAtomsInInductiveCase": "Do not formulate inductive cases for compositions of atomic formulae, use the variables from the induction hypothesis.", "invalidBottomExpr": "The last expression of the subproof is not a correct instantiation of the right hand side of the theorem.", "invalidComposedBaseCase": "Only atomic cases belong to the base cases, composed formulae belong to the inductive cases.", diff --git a/src/lang/nl.json b/src/lang/nl.json index e735104..e44cf32 100644 --- a/src/lang/nl.json +++ b/src/lang/nl.json @@ -452,6 +452,7 @@ "ihNotRecognized": "Dit is geen correcte inductiehypothese", "incorrect": "Er is een fout in het bewijs.", "incorrectApplicationIh": "De toepassing van de inductiehypothese is niet correct", + "inductiveStepNotRecognized": "Dit is geen correcte instantiatie van een inductiestap", "invalidAtomsInInductiveCase": "Formuleer de inductieve gevallen niet voor samenstellingen van atomaire formules, gebruik de variabelen uit de inductiehypothese", "invalidBottomExpr": "De laatste expressie van het deelbewijs is geen correcte instantie van de rechterkant van de stelling", "invalidComposedBaseCase": "Alleen atomaire gevallen horen tot de basisgevallen, samengestelde formules komen in de inductiestap aan bod",