Move proofsamples, and significant updates to proof docs.

doc/en/Authoring/index.md

@@ -49,7 +49,7 @@ The authoring documentation also covers topics on:
 
 #### [Mathematics topics](../Topics/index.md)
 
-* [Proof](../Topics/Proof.md)
+* [Proof](../Proof/index.md)
 * [Curve sketching](../Topics/Curve_sketching.md).
 
 #### Other

doc/en/Developer/Development_history.md

@@ -218,7 +218,7 @@ New features in v4.3:
 * Add in input option 'nounits'.
 * Add in input option 'compact' to input "Show the validation" parameter.
 * Add in a [basic question use report](../Authoring/Reporting.md) page, linked from the question testing page.
-* Add in house styles to help typeset [proof](../Topics/Proof.md).
+* Add in house styles to help typeset [proof](../Proof/Proof_styles.md).
 * Add cache to help reduce parsing overhead.
 
 

doc/en/Proof/Proof_CAS_library.md

@@ -0,0 +1,79 @@
+# CAS libraries for representing text-based proofs
+
+STACK provides libraries to represent and manage lines of a text-based proof in a tree structure.  This page is reference documentation for these CAS libraries.  For examples of how to use these see the topics page on using [Parson's problems](../Topics/Parsons.md).
+
+## Proof construction functions, and their manipulation
+
+Proofs are represented as "proof construction functions" with arguments.  For example, an if and only if proof would be represented as `proof_iff(A,B)`, where both `A` and `B` are sub-proofs. Proof construction functions don't typically modify their arguments, but some proof construction functions have simplification properties.  For example `proof_iff(A,B)` is normally equivalent to `proof_iff(B,A)`.
+
+STACK supports the following types of proof construction functions.  The following are general proofs
+
+* `proof()`: general, unspecified proof.
+* `proof_c()`: general proof, with commutative arguments.  Typically each argument will be another proof block type.
+
+The following represent particular types of proof.
+
+* `proof_iff()`.  This proof must have two arguments.  These arguments are assumed to commute.
+* `proof_cases()`. In proof by exhaustive cases, the first element is fixed, and it typically used to describe/justify the cases.  E.g. "\(n\) is either odd or even".  The remaining cases commute, and typically each argument will be another proof block type.
+* `proof_ind()`.  A proof by induction must have four arguments.  The 1st and 4th are fixed position (defining the statement and conclusion), whereas the 2nd and 3rd commute (for the base case, and induction step).
+
+It is relatively easy to add in new functions to represent a particular type of proof.
+
+The variable `proof_types` is a list holding the names of all proof construction functions.   E.g. this list is used by the predicate `proofp` to decide if the operator represents a proof.
+
+`proof_validatep` is a validation function: the argument must be a tree built from proof construction functions as operators (with the right number of arguments in some cases) or atoms which are integer or strings.
+
+`proof_flatten` turns a proof-tree into a list of steps.  E.g. `proof_flatten(proof_iff(A,B))` is just `[A.B]`.  This function is useful when the teacher creates a structured tree, but a student's proof is a flat list.
+
+`proof_normal` returns a normalised proof-tree, e.g. sorting arguments of commutative proof construction functions.  Note, this function does not change keys, so will not match proofs using integer keys with a proof using string keys.
+
+`proof_alternatives` returns a list of all proof trees which are alternatives to its argument.  E.g. `proof_iff(A,B))` has two alternatives:  `[proof_iff(A,B),proof_iff(B,A)]`.  This function recurses over all sub-proofs to generate any tree which might be equivalent.  Note, if a student is correct then using `proof_normal` will match their answer with the teacher's.  However, when trying to identify possible mistakes we need to find the tree which is _closest_ to one of the acceptable proof trees.  Use this function sparingly, as it is computationally expensive on deeply nested trees with many commutative elements.
+
+## Using a `proof_steps` list
+
+The design relies on a list of `proof_steps`.   Consider this example:"\(n\) is odd if and only if \(n^2\) is odd.";
+
+````
+proof_steps: [
+    ["assodd",     "Assume that \\(n\\) is odd."],
+    ["defn_odd",   "Then there exists an \\(m\\in\\mathbb{Z}\\) such that \\(n=2m+1\\)."],
+    ["alg_odd",    "\\[ n^2 = (2m+1)^2 = 2(2m^2+2m)+1.\\]"],
+    ["def_M_odd",  "Define \\(M=2m^2+2m\\in\\mathbb{Z}\\) then \\(n^2=2M+1\\)."],
+    ["conc_odd",   "Hence \\(n^2\\) is odd."],
+
+    ["contrapos",  "We reformulate \"\\(n^2\\) is odd \\(\\Rightarrow \\) \\(n\\) is odd \" as the contrapositive."],
+    ["assnotodd",  "Assume that \\(n\\) is not odd."],
+    ["even",       "Then \\(n\\) is even, and so there exists an \\(m\\in\\mathbb{Z}\\) such that \\(n=2m\\)."],
+    ["alg_even",   "\\[ n^2 = (2m)^2 = 2(2m^2).\\]"],
+    ["def_M_even", "Define \\(M=2m^2\\in\\mathbb{Z}\\) then \\(n^2=2M\\)."],
+    ["conc_even",  "Hence \\(n^2\\) is even."]
+];
+
+P1:proof_iff(proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd"),proof("contrapos","assnotodd","even","alg_even","def_M_even","conc_even"));
+````
+
+Note that the variable `proof_steps` is a _list_ of lists:  `[ ["key", "step", ("comment")], ...`
+
+1. The first element is a `key`. This is a string, or integer, which is used to refer to the `step`.
+2. The `key` can be an integer position in the proof_steps, a string `key`, or a string.
+  * Using integers: `proof_iff(proof(1,2,3,4,5),proof(6,7,8,9,10,11))`;
+  * Using keys: `proof_iff(proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd"),proof("contrapos","assnotodd","even","alg_even","def_M_even","conc_even"))`
+3. The `proof_steps` list can contain an optional string argument `"comment"`.  This string can be used to store justification, explaination and narative.  Only some display functions use this argument, when it exists.
+4. Note that the backslash must be protected when defining these strings.
+
+`proof_steps_sub(ex, proof_steps)` takes a proof built from numbered indexes, and translate this into string keys.  In the above example, it might be easier to author a proof as `proof(1,2,3,4,5)` rather than type in `proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd")`. The whole design could be built on numbered keys (and these are valid), but string keys are easier to remember and easier to interpret when looking at students' attempts.  Also, string keys can be inserted later without the need to re-number existing numerical keys.
+
+`proof_getstep(key, proof_steps)` looks for the key `key` in the `proof_steps` list.  They key can be either a numerical, or string key.  If found then the function returns the full string, otherwise the key is returned without an error.  One advantage of this approach is that the teacher can define abreviated, alternative proofs using some of the strings in `proof_steps`, e.g. using the above example the following omits all the detail in the sub-proofs, focusing on the structure and hypothesis/conclusion of each block.
+
+````
+P2:proof_iff(proof("assodd","\\(\\cdots\\)","conc_odd"), proof("contrapos","assnotodd","\\(\\cdots\\)","conc_even"));
+````
+
+When displayed, the keys `"\\(\\cdots\\)"` do not occur in `proof_steps`, so are returned unchanged.  (Alteratively a teacher could add keys to `proof_steps` for such situations.)
+
+## Displaying whole proof and proof-step pairs
+
+To display a whole proof whole proof usinf proof-step lists use `proof_display(P1, proof_steps)`.  E.g. add `{@proof_display(P1, proof_steps)@}` to the appropriate castext.  This will (1) replace all keys in the proof `P1` with the corrsponding strings in `proof_steps` (if they exist) and (2) display the structure using the nested `<div class="proof-block">` from the [CSS Styles for displaying proof](Proof_styles.md).
+
+`proof_display_para(P1, proof_steps)` displays a complete proof, but using HTML paragraphs to split blocks.  This is a more traditioanl presentation of proof.
+

doc/en/Topics/Proof.md → doc/en/Proof/Proof_styles.md

@@ -1,29 +1,9 @@
-# Assessment of proof
-
-In STACK the basic assumption is that a student's answer will be a mathematical expression, e.g. a polynomial or an equation.  The facilities for assessing a student's free-form proof is limited.
-
-A discussion of [_Practical Online Assessment of Mathematical Proof_](https://www.tandfonline.com/doi/abs/10.1080/0020739X.2021.1896813) was given by Sangwin, C.J. and Bickerton, R. (2023), International Journal of Mathematical Education in Science and Technology}, 53(10) doi:10.1080/0020739X.2021.1896813.   This included more structured questions making use of
-
-* faded worked examples and,
-* reading comprehension questions.
-
-Colleagues assessing proof might also consider [semi-automatic marking](../Moodle/Semi-automatic_Marking.md) and using [Parson's problems](Parsons.md).
-
-## Representation of text-based proof
-
-STACK provides libraries to represent and manage lines of a text-based proof.  The goals are
-
-* to manage strings forming part of a traditional written proof;
-* to represent the macro structure of a proof, arranged into nested blocks;
-* to separate the text of the proof from choices of how to display a proof;
-* to provide teachers with tools to assess students' attempts at [Parson's problems](Parsons.md).
-
-The goals do not include automatic proof checking.
-
-## Styles
+# CSS Styles for displaying proof
 
 We support the following CSS styles to enable consistent display of mathematical proof, and arguments in general.  General style was also introduced with the [HELM](../Reference/HELM.md) materials.
 
+Note, the precise style will also depend on the styles in your learning environment.  The `class="proof"` styles focus on block structure and layout, e.g. indenting blocks and column layout.  Colour and typeface are generally not specified in the proof styles (although a white background is defined).  Styles are defined in `styles.css` of the top-level of the STACK plugin.
+
 ### `<div class="proof">`
 
 This class is a general high level container.

doc/en/Proof/index.md

@@ -0,0 +1,109 @@
+# Support for proof and recepies in STACK
+
+In STACK the basic assumption is that a student's answer will be a mathematical expression, e.g. a polynomial or an equation.  While the facilities for assessing a student's free-form proof is limited (in any online assessment system), teachers can create materials for assessing students' understanding of proof in general, and of particular mathematical proofs.
+
+This page contains a general discussion of the nature of mathematical writing, especially proof.  For further information see:
+
+1. The topics page on [using Parson's problems](../Topics/Parsons.md) to assess proof.
+2. Reference documentation on the [Parson's problems block](../Authoring/Parsons.md).
+3. Reference documentation on [CAS libraries for representing text-based proofs](Proof_CAS_library.md).
+4. Reference documentation on [CSS Styles for displaying proof](Proof_styles.md).
+5. Example proofs are distributed with the STACK source code within [`stack/maxima/contrib`](https://https://github.com/maths/moodle-qtype_stack/master/stack/maxima/contrib/).
+6. Note also the functions for displaying [trees](../Authoring/Trees.md) which may be useful in some situations.
+
+A discussion of [_Practical Online Assessment of Mathematical Proof_](https://www.tandfonline.com/doi/abs/10.1080/0020739X.2021.1896813) was given by Sangwin, C.J. and Bickerton, R. (2023), International Journal of Mathematical Education in Science and Technology}, 53(10) doi:10.1080/0020739X.2021.1896813.  This included more structured questions making use of
+
+* faded worked examples and,
+* reading comprehension questions.
+
+Colleagues assessing proof might also consider [semi-automatic marking](../Moodle/Semi-automatic_Marking.md) and using [Parson's problems](../Topics/Parsons.md) for drag and drop proof construction tasks.
+
+## The nature of mathematical proof
+
+Mathematical writing, especially for students, commonly takes two forms.
+
+1. A mathematical proof, which is a deductive justification of a claim.  A proof is a "checkable record of reasoning".
+2. A mathematical recepie, which is a set of instructions for carrying out a procedure.
+
+## Presentation of proof
+
+STACK supports representation and display of mathematical proof as trees, with string nodes for the individual sentences/clauses in the proof.  The goals of representing proofs as trees of text-based strings are as follows.
+
+1. Manage strings forming part of a traditional written proof;
+2. Separate the macro tree-structure of the proof from the details of each step.
+3. Separate the content from presentation (following well-established principles in both LaTeX and HTML).
+4. Separate the content from justification, explanation and narrative.
+5. Help teachers present proof in a consistent way within their course.
+6. Make it simpler for teachers to write correct proofs.
+7. Provide mechanisms for dynamically altering the level of detail, e.g. hiding or revealing steps and narrative.
+8. Provide mechanisms for assessing solutions to [Parson's problems](../Topics/Parsons.md) and provide feedback to students.
+
+The goals do not include automatic proof checking.
+
+By separating out these issues we provide more control, and wider opportunities for choice in when and how to generate the right level of cognitive load for students. Traditional presentation of proofs often confound all these issues, confusing students.
+
+# Case study: proof by induction
+
+Consider the following theorem:  \(\sum_{k=1}^n (2k-1) = 1+3+5+\cdots + (2n-1) = n^2\).
+A traditional proof is shown below. This proof was published by DeMorgan in 1838.  According to Cajori (1918) this is the first use of the name "mathematical induction", although DeMorgan calls it "successive induction".
+
+![DeMorgan's induction](../../content/DeMorgan1836-induction.jpeg)
+
+This proof is dense, difficult to read and lacks structure.  Since DeMorgan's day, proof by induction is a slightly more formal method of proof consisting of four parts, (i) a statement to be proved, (ii) a base case, (iii) the induction step, and (iv) the conclusion.  Here is a modern version.
+
+<hr/>
+
+Let \(P(n)\) be the statement "\(\sum_{k=1}^n (2k-1) = n^2\)".
+
+Since \(\sum_{k=1}^1 (2k-1) = 1 = 1^2\) we see \(P(1)\) is true.
+
+Assume \(P(n)\) is true. Then
+\[ \sum_{k=1}^{n+1} (2k-1) = \sum_{k=1}^n (2k-1) + (2(n+1)-1) = n^2 + 2n +1 = (n+1)^2.\]
+Hence \(P(n+1)\) is true.
+
+Since \(P(1)\) is true and \(P(n+1)\) follows from \(P(n)\) we conclude that \(P(n)\) is true for all \(n\) by the principle of mathematical induction.
+
+<hr/>
+
+The above proof contains all the detail, and an expert might choose to omit some of the formality and abbreviate the proof.  This is an example of the expert-reversal affect.  However, it is still written in paragraph mode, we could do a lot more to highlight the structure using styles, e.g.
+
+<div style="color: #2f6473; background-color: #def2f8; border-color: #d1edf6;">
+<div class="proof">
+<p>Let P(n) be the statement [...] </p>
+<p>Consider the base case [...]</p>
+<p>Assume P(n) is true [...] hence P(n+1) is true.</p>
+<p>It follows that P(n) is true for all n by the principle of mathematical induction.</p>
+</div>
+</div>
+
+To represent this proof in STACK we define the following
+
+````
+proof_steps: [
+    ["defn_p",     "Let \\(P(n)\\) be the statement \"\\(\\sum_{k=1}^n (2k-1) = n^2\\)\"."],
+
+    ["base_hyp",   "Note that \\(\\sum_{k=1}^1 (2k-1) = 1 = 1^2\\)"],
+    ["base_conc",  "Hence \\(P(1)\\) is true."],
+
+    ["ind_hyp",    "Assume \\(P(n)\\) is true."],
+    ["ind_1",      "Then \\(\\sum_{k=1}^{n+1} (2k-1)\\)"],
+    ["ind_2",      "\\( = \\sum_{k=1}^n (2k-1) + (2(n+1)-1)\\)"],
+    ["ind_3",      "\\( = n^2 + 2n +1 = (n+1)^2.\\)"],
+    ["ind_conc",   "Hence \\(P(n+1)\\) is true."],
+
+    ["concp",      "Since \\(P(1)\\) is true and \\(P(n+1)\\) follows from \\(P(n)\\) we conclude that \\(P(n)\\) is true for all \\(n\\) by the principle of mathematical induction."]
+];
+
+/****************************************************************/
+P0:proof_ind(1,proof(2,3),proof(5,6,7,8),9);
+P1:proof_ind("defn_p",proof("base_hyp","base_conc"),proof("ind_1","ind_2","ind_3","ind_conc"),"concp");
+````
+
+Note that the variable `proof_steps` is a _list_ of lists:  `[ ["key", "step"], ...`
+
+1. The first element is a `key`. This is a string, or integer, which is used to refer to the `step`.
+2. The `key` can be an integer position in the proof_steps, a string `key`, or a string.
+3. The variables `P0` and `P1` represent the proof structure. `proof_ind` represents a proof by induction.  Notice the base case and induction steps are themselves `proof` representations, giving identity to these blocks.
+
+See the reference documentation on [CAS libraries for representing text-based proofs](Proof_CAS_library.md) for more types of proofs and functions for dealing with them.
+

doc/en/Topics/Parsons.md

@@ -21,8 +21,11 @@ We might expect/require two conscious and separate blocks
 1.  Assume \(A\), \(\cdots\), hence \(B\).
 2.  Assume \(B\), \(\cdots\), hence \(A\).
 
-The order in which these two sub-proofs are presented is (normally) irrelevant.  That is the _if and only if_ proof construct allows its two sub-proofs to commute.  This is precisely the same sense in which \(A=B\) and \(B=A\) are equivalent. There are _blocks_ within the proof which can change order. Furthermore, since proofs are often nested blocks these sub-proofs may themselves have acceptable options for correctness. If the student has an opportunity to indicate more structure, then the assessment logic becomes considerably simpler, more reliable and transparent. Actually, we think there is significant educational merit in making this structure explicit and consciously separating proof-structure from the finer grained details.
-It is true that professional mathematicians often omit indicating explicit structure, they abbreviate and omit whole blocks ("the other cases are similar") but these are all further examples of expert reversal.
+The order in which these two sub-proofs are presented is (normally) irrelevant.  That is the _if and only if_ proof construct allows its two sub-proofs to commute.  This is precisely the same sense in which \(A=B\) and \(B=A\) are equivalent. There are _blocks_ within the proof which can change order. Furthermore, since proofs are often nested blocks these sub-proofs may themselves have acceptable options for correctness.
+
+Proofs often contain local variables.  Use of explicit block-structres clarify the local scope of variables, and the local scope of assumptions.
+
+If the student has an opportunity to indicate more structure, then the assessment logic becomes considerably simpler, more reliable and transparent. Actually, we think there is significant educational merit in making this structure explicit and consciously separating proof-structure from the finer grained details. It is true that professional mathematicians often omit indicating explicit structure, they abbreviate and omit whole blocks ("the other cases are similar") but these are all further examples of expert reversal.
 
 Notes
 
@@ -155,7 +158,6 @@ FOR NOW
 <p>[[input:ans1]] [[validation:ans1]]</p>
 ````
 
-
 Notice the function `stackjson_stringify` turns the variable `proof_steps` into a JSON object.
 
 Notice in this example the teacher's proof is nested.  This can be seen if we use numerical keys, not string keys and define 

doc/en/Topics/index.md

@@ -10,7 +10,7 @@ Current topics include:
 * [Discrete mathematics](Discrete_mathematics.md)
 * String similarity via the [Levenshtein distance](Levenshtein_distance.md)
 * [Linear algebra](Linear_algebra.md)
-* [Mathematical Proof](Proof.md)
+* [Mathematical Proof](../Proof/index.md)
 * [Propositional Logic](Propositional_Logic.md)
 * [Scientific Units](Units.md)
 * [Vector Calculus](Vector_Calculus.md)