add stackmaxima 2025012100

README.md

@@ -71,6 +71,7 @@ What Stackmaxima version do I need?
 | -                   | `4.7.0`              | 2024072400          | 5.44.0                  |
 | -                   | `4.8.0`              | 2024111500          | 5.44.0                  |
 | -                   | `4.8.1`              | 2024111900          | 5.44.0                  |
+| -                   | `4.8.3`              | 2025012100          | 5.44.0                  |
 
 
 Building a Docker Image

docker-compose.yml

 version: "3.3"
 services:
   maxima:
-    image: mathinstitut/goemaxima:${STACKMAXIMA_VERSION:-2024111900}-latest
+    image: mathinstitut/goemaxima:${STACKMAXIMA_VERSION:-2025012100}-latest
     ports:
       - 0.0.0.0:8080:8080
     tmpfs:

src/web/web.go

@@ -620,13 +620,13 @@ func init_metrics() Metrics {
 
 func user_info(user_id uint) (*User, error) {
 	user_name := fmt.Sprintf("maxima-%d", user_id)
+	var uid int
+	var gid int
+	if process_isolation {
 		usr, err := user.Lookup(user_name)
 		if err != nil {
 			log.Fatalf("Fatal: Could not look up user with id %d: %s", user_id, err)
 		}
-	var uid int
-	var gid int
-	if process_isolation {
 		uid, err = strconv.Atoi(usr.Uid)
 		if err != nil {
 			log.Fatalf("Fatal: Cannot parse uid %s as number: %s", usr.Uid, err)

stack/2025012100/maxima/contrib/builder.mac

+/*  Author Neil P Strickland
+    University of Sheffield
+    Copyright (C) 2024 Neil P Strickland
+
+    This program is free software: you can redistribute it or modify
+    it under the terms of the GNU General Public License version two.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+    GNU General Public License for details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program. If not, see <http://www.gnu.org/licenses/>. */
+
+/******************************************************************/
+/* For proof-builder questions, the teacher answer field is a list
+ * of lists of the form [key, phrase, pos] where
+ * phrase and key are strings, and pos is a nonnegative
+ * integer.  
+ *
+ * For the original source see
+ * https://github.com/NeilStrickland/moodle-qtype_stack/blob/sheffield/stack/maxima/builder.mac
+ *
+ */
+/******************************************************************/
+
+builder_add_pos(opts) := block([],
+ makelist(endcons(i,opts[i]),i,1,length(opts))
+)$
+
+builder_correct(opts) := block(
+ [oo,o],
+ oo : sublist(opts,lambda([o],o[3] > 0)),
+ oo : sort(oo,lambda([p,q],ev(p[3] < q[3],pred))),
+ return(map(first,oo))
+)$
+
+builder_sol(opts) := block(
+ [oo,o],
+ oo : sublist(opts,lambda([o],o[3] > 0)),
+ oo : sort(oo,lambda([p,q],ev(p[3] < q[3],pred))),
+ return(simplode(map(second,oo)," "))
+)$
+
+builder_say_includes(phrase) := sconcat(
+ "Your answer includes the following phrase: <br/>",newline,
+ "<blockquote class=\"builder_phrase\">",newline,
+ phrase,newline,
+ "</blockquote>",newline
+);
+
+builder_say_excludes(phrase) := sconcat(
+ "Your answer does not include the following phrase: <br/>",newline,
+ "<blockquote class=\"builder_phrase\">",newline,
+ phrase,newline,
+ "</blockquote>",newline
+);
+
+builder_needs_intro(s) := block(
+ [t],
+ t : sconcat("\\(",s,"\\)"),
+ return(sconcat(
+  "This refers to ",t,", but at the point where this phrase appears, ",
+  "we do not know what this means.  Before using the symbol ",t,", ",
+  "you need to introduce it in some way, with a phrase like ",
+  "'Let ",t," be an integer' or 'Consider an element \\(",s,"\\in X\\)' ",
+  "or 'There exists a permutation ",t," such that...'."
+ ))
+);
+
+builder_get_phrase(skey,opts) := block([o,t],
+ t : "",
+ for o in opts do (
+  if first(o) = skey then (
+    t : second(o),
+    return(t)
+  )
+ ),
+ return(t) 
+);
+
+builder_check_present(ans,skey) := member(skey,ans);
+
+builder_check_precedes(ans,key_a,key_b) := block([k,r],
+ if not(member(key_a,ans)) then return(false),
+ if not(member(key_b,ans)) then return(false),
+ r : false,
+ for k in ans do (
+  if k = key_a then (r : true, return(r)),
+  if k = key_b then (r : false, return(r))
+ ),
+ return(r)
+);
+
+builder_check_needs(ans,dict,needers,needed,fb) := block(
+ [seen,needed_set,needed_seen,ret,k,Z],
+ seen : [],
+ ret : false,
+ if setp(needed) then
+  needed_set : needed
+ elseif listp(needed) then 
+  needed_set : apply(set,needed) 
+ else 
+  needed_set : {needed}, 
+ for k in ans do (
+  if member(k,needers) and length(intersect(needed_set,apply(set,seen))) = 0 then (
+   ffb : sconcat(builder_say_includes(dict[k]),fb),
+   ret : ["needs",k,needed,ffb],
+   return(ret)
+  ),
+  seen : endcons(k,seen)
+ ),
+ return(ret)
+);
+
+builder_check_needs_immediate(ans,dict,needers,needed,fb) := block(
+ [ret,k,i],
+ ret : false,
+ for i from 1 thru length(ans) do (
+  k : ans[i],
+  if member(k,needers) and (i = 1 or not(ans[i-1] = needed)) then (
+   ffb : sconcat(builder_say_includes(dict[k]),fb),
+   ret : ["needs_immediate",k,needed,ffb],
+   return(ret)
+  )
+ ),
+ return(ret)
+);
+
+builder_check_exclude(ans,dict,excluded,fb) := block(
+ [p,ret,ffb],
+ ret : false,
+ for p in excluded do (
+  if member(p,ans) then (
+   ffb : sconcat(builder_say_includes(dict[p]),fb),
+   ret : ["exclude",p,ffb],
+   return(ret)
+  )
+ ),
+ return(ret)
+);
+
+builder_check_require(ans,dict,required,fb) := block(
+ [p,ret,ffb],
+ ret : false,
+ for p in required do (
+  if not(member(p,ans)) then (
+   ffb : sconcat(builder_say_excludes(dict[p]),fb),
+   ret : ["require",p,ffb],
+   return(ret)
+  )
+ ),
+ return(ret)
+);
+
+builder_check_rules(ans,opts,prules) := block(
+ [dict,o,r],
+ for o in opts do dict[first(o)] : second(o),
+ ret : false,
+ for r in prules do (
+  if first(r) = "needs" then (
+   c : builder_check_needs(ans,dict,r[2],r[3],r[4]),
+   if not(c = false) then (
+    sc : 0, 
+    an : sconcat("needs/",c[2],"/",r[3]),
+    fb : c[4],
+    ret : [sc,an,fb],
+    return(ret)
+   )
+  ) elseif first(r) = "needs_immediate" then (
+   c : builder_check_needs_immediate(ans,dict,r[2],r[3],r[4]),
+   if not(c = false) then (
+    sc : 0, 
+    an : sconcat("needs_immediate/",c[2],"/",c[3]),
+    fb : c[4],
+    ret : [sc,an,fb],
+    return(ret)
+   )
+  ) elseif first(r) = "exclude" then (
+   c : builder_check_exclude(ans,dict,r[2],r[3]),
+   if not(c = false) then (
+    sc : 0, 
+    an : sconcat("exclude/",c[2]),
+    fb : c[3],
+    ret : [sc,an,fb],
+    return(ret)
+   )
+  ) elseif first(r) = "require" then (
+   c : builder_check_require(ans,dict,r[2],r[3]),
+   if not(c = false) then (
+    sc : 0, 
+    an : sconcat("require/",c[2]),
+    fb : c[3],
+    ret : [sc,an,fb],
+    return(ret)
+   )
+  )
+ ),
+ if (ret = false) then (
+  return([1,"correct",""])
+ ) else (
+  return(ret)
+ ) 
+);

stack/2025012100/maxima/contrib/matchlib.mac

+/*  Author Salvatore Mercuri
+    University of Edinburgh
+    Copyright (C) 2024 Salvatore Mercuri
+
+    This program is free software: you can redistribute it or modify
+    it under the terms of the GNU General Public License version two.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+    GNU General Public License for details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program. If not, see <http://www.gnu.org/licenses/>. */
+
+/******************************************************************/
+/*  Functions for extracting data from matching problems          */
+/*  in STACK to a format that can be assessed by the author.      */
+/*  Should be used when providing model answers and writing       */
+/*  PRTs for matching problems using the `parsons` block.         */
+/*                                                                */
+/*  Salvatore Mercuri, <smercuri@ed.ac.uk>                        */
+/*  V1.0 May 2024                                                 */
+/*                                                                */
+/******************************************************************/
+
+/* To use these functions load the library via one of the following 
+two commands inside `Question variables`.
+
+stack_include("https://raw.githubusercontent.com/maths/moodle-qtype_stack/proof-builder/stack/maxima/contrib/matchlib.mac");
+stack_include("contribl://matchlib.mac");
+*/
+
+/******************************************************************/
+/*                                                                */
+/*  Assessment helper functions                                   */
+/*                                                                */
+/******************************************************************/
+
+/*
+ * Hashes the first element of each sublist in a two-dimensional steps array using Base64 hashing. 
+ *
+ * It will turn `[["a", "b"], ["c", "d"], ["e", "f"]]` into `[["YQ==", "b"], ["Yg==", "d"], ["ZQ==", "f"]]`.
+ */
+hash_keys_array(steps) := block(
+  return(map(lambda([item], join([base64(first(item))], rest(item, 1))), steps))
+);
+
+/*
+ * Hashes all strings in a two-dimensional steps array using Base64 hashing. 
+ *
+ * It will turn `[["a", "b"], ["c", "d"], ["e", "f"]]` into `[["YQ==", "Yg=="], ["Yg==", "ZA=="], ["ZQ==", "Zg=="]]`.
+ */
+hash_2d_array(arr) := block(
+    return(map(lambda([l], map(base64, l)), arr))
+);
+
+/*
+ * Takes the hashed JSON from STACK Parson's block and return a de-hashed array.
+ */
+match_decode(st, [rows]) := block([js, arr],
+    js: first(first(stackjson_parse(st))),
+    arr: stackmap_get(js, "used"),
+    if rows=[] then arr:map(lambda([keys], map(base64_decode, first(keys))), arr) 
+      else arr:map(lambda([keys], map(lambda([k], if k # [] then base64_decode(first(k)) else []), keys)), arr),
+    return(arr)
+);
+
+/*
+ * Turns a two-dimensional proof steps array into a JSON string with Base64-hashed keys.
+ */
+match_encode(steps) := block(
+  return(stackjson_stringify(hash_keys_array(steps)))
+);
+
+/*
+ * Auxiliary function.
+ *
+ * Takes a list of hashed answer keys and the full 2d steps array and returns the the all used hashed keys and unusued hashed keys.
+ * Needed to create a "teacher's answer" in JSON format, including unused text.
+ */
+match_keys_used_unused_hash(ans, steps) := block([tkeys],
+  tkeys:map(first, hash_keys_array(steps)),
+  skeys:hash_2d_array(ans),
+  return([skeys, listdifference(tkeys, ev(unique(flatten(skeys)), simp))])
+);
+
+/*
+ * Use this to transform the teacher's answer into the shape expected by the Parson's block.
+ * Returns an array of `[answer_keys, unused_keys]`, where `unused_keys` is always a flat
+ * list of keys that are in the question but not inside `ans`.
+ * 
+ * If only `columns` has been specified in the `parsons` block, then use 
+ * this function as `match_reshape_hash(ans1)`. This will return `answer_keys` as an 
+ * array of shape `(columns, 1, ?)` if, where `?` represents variable dimension.
+ * 
+ * If both `rows` and `columns` have been specified in the `parson` block, then 
+ * use this function as `match_reshape_hash(ans1, true)`. This will 
+ * return `answer_keys` as an array of shape `(columns, rows, 1)`.
+ */
+match_reshape_hash(ans, steps, [rows]) := block([tkeys, akeys],
+  tkeys: match_keys_used_unused_hash(ans, steps),
+  if rows=[] then akeys: map(lambda([keys], [keys]), first(tkeys)) 
+    else akeys:map(lambda([keys], map(lambda([k], [k]), keys)), first(tkeys)),
+  return([akeys, second(tkeys)])
+);
+
+/*
+ * Use this to transform the teacher's answer into the JSON format expected by the `Model answer` field.
+ * 
+ * If only `columns` has been specified in the `parsons` block, then use 
+ * this function as `match_answer(ans1)`. 
+ *
+ * If both `rows` and `columns` have been specified in the `parson` block, then 
+ * use this function as `match_answer(ans1, true)`. 
+ */
+match_answer(ans, steps, [rows]) := block([akeys, ukeys],
+  if rows=[] then [akeys, ukeys]: match_reshape_hash(ans, steps)
+    else [akeys, ukeys]: match_reshape_hash(ans, steps, rows),
+  sconcat("[[{\"used\":", stackjson_stringify(akeys), ", \"available\":", stackjson_stringify(ukeys), "}, 0]]")
+);
+
+/*
+ * Alias for for the column-only usage `match_answer(ans_steps)` of `match_answer`.
+ */
+group_answer(ans, steps) := match_answer(ans, steps);
+
+/*
+ * Use this to turn a row-grouped answer into a column-grouped answer and vice-versa.
+ * 
+ * Note that model answers for matching problems in STACK should always be written by grouping 
+ * the columns, that is they should be a two-dimensional array of shape `(columns, rows)`. Authors 
+ * may prefer to use the row-grouped answer in PRTs. This function will move between them.
+ */
+match_transpose(ans) := block(
+    return(args(transpose(apply(matrix, ans))))
+);
+
+/*
+ * Use this on both the model answer and the student input 
+ * when you do not care about the order within a column.
+ * 
+ * It will turn `[[a, b], [c, d], [e, f]]` into `[{a, b}, {c, d}, {e, f}]`.
+ */
+match_column_set(ans) := block(
+    return(map(lambda([col], apply(set, col)), ans))
+);
+
+/*
+ * Use this on both the model answer and the student input 
+ * when you do not care about the order within a row.
+ * 
+ * It will turn `[[a, b], [c, d], [e, f]]` into `[{a, c, e}, {b, d, f}]`.
+ */
+match_row_set(ans) := block(
+    return(match_column_set(match_transpose(ans)))
+);
+
+/*
+ * Use this on both the model answer and the student input 
+ * when you do not care about the order between columns.
+ * 
+ * It will turn `[[a, b], [c, d], [e, f]]` into `{[a, b], [c, d], [e, f]}`.
+ */
+match_set_column(ans) := block(
+    return(apply(set, ans))
+);
+
+/*
+ * Use this on both the model answer and the student input 
+ * when you do not care about the order between rows.
+ * 
+ * It will turn `[[a, b], [c, d], [e, f]]` into `{[a, c, e], [b, d, f]}`.
+ */
+match_set_row(ans) := block(
+    return(match_set_column(match_transpose(ans)))
+);
+
+/******************************************************************/
+/*                                                                */
+/*  Assessment helper functions (legacy)                          */
+/*                                                                */
+/******************************************************************/
+
+/*
+ * Use this to extract an answer from the student's input of desirable format
+ * for assessing.
+ *
+ * Take the JSON from STACK Parson's block when using `columns` and/or 
+ * `rows` header parameter, and returns a two-dimensional array corresponding to 
+ * the answer keys in the JSON. 
+ * 
+ * If only `columns` has been specified in the `parsons` block, then use 
+ * this function as `match_interpret(ans1)`. This will return an 
+ * array of shape `(columns, ?)` if, where `?` represents variable dimension.
+ *
+ * If both `rows` and `columns` have been specified in the `parson` block, then 
+ * use this function as `match_interpret(ans1, true)`. This will 
+ * return an array of shape `(columns, rows)`.
+ */
+match_interpret(st, [rows]) := block([js, arr],
+    js: first(first(stackjson_parse(st))),
+    arr: stackmap_get(js, "used"),
+    if rows=[] then arr:map(lambda([keys], first(keys)), arr) 
+      else arr:map(lambda([keys], map(lambda([k], first(k)), keys)), arr),
+    return(arr)
+);
+
+/*
+ * Auxiliary function.
+ *
+ * Takes a list of matched keys and returns the keys not used.
+ * Needed to create a "teacher's answer" in JSON format, including unused text.
+ */
+match_keys_used_unused(ans, steps) := block([tkeys],
+  tkeys:map(first, steps),
+  return([ans, listdifference(tkeys, ev(unique(flatten(ans)), simp))])
+);
+
+/*
+ * Use this to transform the teacher's answer into the shape expected by the Parson's block.
+ * Returns an array of `[answer_keys, unused_keys]`, where `unused_keys` is always a flat
+ * list of keys that are in the question but not inside `ans`.
+ * 
+ * If only `columns` has been specified in the `parsons` block, then use 
+ * this function as `match_reshape(ans1)`. This will return `answer_keys` as an 
+ * array of shape `(columns, 1, ?)` if, where `?` represents variable dimension.
+ * 
+ * If both `rows` and `columns` have been specified in the `parson` block, then 
+ * use this function as `match_interpret(ans1, true)`. This will 
+ * return `answer_keys` as an array of shape `(columns, rows, 1)`.
+ */
+match_reshape(ans, steps, [rows]) := block([tkeys, akeys],
+  tkeys: match_keys_used_unused(ans, steps),
+  if rows=[] then akeys: map(lambda([keys], [keys]), first(tkeys)) 
+    else akeys:map(lambda([keys], map(lambda([k], [k]), keys)), first(tkeys)),
+  return([akeys, second(tkeys)])
+);
+
+/*
+ * Use this to transform the teacher's answer into the JSON format expected by the `Model answer` field.
+ * 
+ * If only `columns` has been specified in the `parsons` block, then use 
+ * this function as `match_correct(ans1)`. 
+ *
+ * If both `rows` and `columns` have been specified in the `parson` block, then 
+ * use this function as `match_correct(ans1, true)`. 
+ */
+match_correct(ans, steps, [rows]) := block([akeys, ukeys],
+  if rows=[] then [akeys, ukeys]: match_reshape(ans, steps)
+    else [akeys, ukeys]: match_reshape(ans, steps, rows),
+  sconcat("[[{\"used\":", stackjson_stringify(akeys), ", \"available\":", stackjson_stringify(ukeys), "}, 0]]")
+);

stack/2025012100/maxima/contrib/prooflib_test.mac

+/*  Author Chris Sangwin
+    University of Edinburgh
+    Copyright (C) 2023 Chris Sangwin
+
+    This program is free software: you can redistribute it or modify
+    it under the terms of the GNU General Public License version two.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+    GNU General Public License for details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program. If not, see <http://www.gnu.org/licenses/>. */
+
+/******************************************************************/
+/*  Functions for representing, typesetting and assessing proof.  */
+/*  Mostly for use with Parsons problems.                         */
+/*                                                                */
+/*  Test cases.                                                   */
+/*                                                                */
+/*  Chris Sangwin, <C.J.Sangwin@ed.ac.uk>                         */
+/*  V1.0 May 2024                                                 */
+/*                                                                */
+/******************************************************************/
+
+
+s_test_case(proof_alternatives(proof(A,B,C,D)), [proof(A,B,C,D)]);
+s_test_case(proof_alternatives(proof_c(A,B)), [proof_c(A,B),proof_c(B,A)]);
+s_test_case(proof_alternatives(proof_iff(A,B)), [proof_iff(A,B),proof_iff(B,A)]);
+s_test_case(proof_alternatives(proof_ind(A,B,C,D)), [proof_ind(A,B,C,D),proof_ind(A,C,B,D)]);
+s_test_case(proof_alternatives(proof_cases(A,B,C)), [proof_cases(A,B,C),proof_cases(A,C,B)]);
+s_test_case(proof_alternatives(proof_goal(A,B,C)), [proof_goal(A,B,C),proof_goal(B,A,C)]);
+s_test_case(proof_alternatives(proof_iff(proof(proof_opt(A), B),C)), [proof_iff(proof(A,B),C),proof_iff(proof(B),C),proof_iff(C,proof(A,B)),proof_iff(C,proof(B))]);
+
+s_test_case(proof_parsons_interpret("{\"used\":[[[\"MA==\",\"Mw==\",\"NQ==\"]]],\"available\":[\"MQ==\",\"Mg==\",\"NA==\",\"Ng==\",\"Nw==\"]}"), proof("0","3","5"));
+
+s_test_case(proof_inline_maths("\\[ 3 = 2^{\\frac{p}{q}}\\]"), "\\( 3 = 2^{\\frac{p}{q}}\\)");
+
+/******************************************************************/
+
+s_test_case(proof_damerau_levenstein([1,2,3],[1,2,3]), [0,[]]);
+s_test_case(proof_damerau_levenstein([1,2,3],[1,2,3,4]), [1,[dl_ok(1),dl_ok(2),dl_ok(3),dl_add(4)]]);
+s_test_case(proof_damerau_levenstein([1,3,4],[1,2,3,4]), [1,[dl_ok(1),dl_add(2),dl_ok(3),dl_ok(4)]]);
+s_test_case(proof_damerau_levenstein([3,4],[1,2,3,4]), [2,[dl_add(1),dl_add(2),dl_ok(3),dl_ok(4)]]);
+s_test_case(proof_damerau_levenstein([1,3,2,4],[1,2,3,4]), [1,[dl_ok(1),dl_swap(3,2),dl_swap_follow(2),dl_ok(4)]]);
+

stack/2025012100/maxima/contrib/proofsamples/analysis-sequence-sum-diverge.mac

+/****************************************************************/
+thm:"Proposition: If \\((a_n)\\) diverges to infinity and \\((b_n)\\) converges to \\(b\\in\\mathbb{R}\\), then the sequence \\((a_n+b_n)\\) diverges to infinity.";
+
+/****************************************************************/
+proof_steps: [
+    ["ass1",     "Let \\((a_n)\\) be a sequence that diverges to infinity."],
+    ["ass2",     "Let \\((b_n)\\) be a sequence that converges to a limit \\(b\\)."],
+    ["ass3",     "Let \\(M>0\\)."],
+    ["defc1",    "Let \\(N_1\\) be such that if \\(n>N_1\\) then \\(a_n\\geq M-b+1\\), which exists because \\((a_n)\\) diverges to infinity."],
+    ["defc2",    "Let \\(N_2\\) be such that if \\(n>N_2\\), then \\(|b_n-b|<1\\), which exists from the definition of \\((b_n)\\) converges to \\(b\\) with \\(\\epsilon=1\\). "],
+    ["s1",       "Let \\(N\\) be the maximum of \\(N_1\\) and \\(N_2\\). "],
+    ["s2",       "If \\(n>N\\), then \\(a_n+b_n>(M-b+1)+(b-1)\\)."],
+    ["s3",       "If \\(n>N\\), then \\(a_n+b_n>M\\)."],
+    ["conc",     "\\((a_n+b_n)\\) diverges to infinity."]
+];
+
+wrong_steps: [];
+
+proof_steps:append(proof_steps,wrong_steps);
+
+ta:proof(proof_c("ass1","ass2","ass3"),proof_c("defc1","defc2"),"s1","s2","s3","conc");
+ta2:proof(proof_c(proof(proof_c("ass1","ass3"),"defc1"),proof("ass2","defc2")), "s1","s2","s3","conc");
+proof_ans:append(proof_alternatives(ta),proof_alternatives(ta2));

stack/2025012100/maxima/contrib/proofsamples/harmonic-series.mac

+/****************************************************************/
+thm:"The harmonic series diverges.";
+
+
+/****************************************************************/
+proof_steps: [
+    ["defn_pn",    "Define \\(p_n\\) to be the \\(n\\)th prime number."],
+    ["pn_gt_n",    "We know that \\(p_n \\geq n > 0\\) for all natural numbers \\(n\\)."],
+    ["pn_lt_n",    "Hence \\(\\frac{1}{p_n} \\leq \\frac{1}{n}\\) for all natural numbers \\(n\\)."],
+    ["pn_div",     "We know that \\(\\sum_{n=1}^\\infty \\frac{1}{p_n}\\) diverges."],
+    ["comptst",    "Apply the comparison test: if \\(a_n \\leq b_n\\) and \\(\\sum_{n=1}^\\infty a_n\\) diverges then \\(\\sum_{n=1}^\\infty b_n\\) diverges."],
+    ["conc",       "The harmonic series diverges."]
+    ];
+
+/* This is how the teacher defines their answer, as nested proofs. */
+proof_ans:proof("defn_pn","pn_gt_n","pn_lt_n","pn_div","comptst","conc");

stack/2025012100/maxima/contrib/proofsamples/index.md

+# Example mathematical proofs
+
+This directory contains example mathematical proofs and other arguments as samples and test cases for the proof library.
+
+Each file must define three variables:
+
+1. a variable `thm` to hold a statement of the theorem.  This is a string variable.
+2. a variable `proof_steps`, which is a list of `["key", "proof string"]` pairs.
+3. a variable `proof_ans` which represents the proof.
+
+A teacher refers to the individual steps in the proof using 
+
+1. the short `"key"` string.  
+2. the integer position in the proof.
+
+For example, if we have "\(\log_2(3)\) is irrational." then the teacher can define the proof as a list of steps using keys as follows.
+
+    proof_ans:proof("assume","defn_rat","defn_rat2","defn_log","defn_log2","alg","alg_int","contra","conc");
+
+The function `proof` represents a proof.  Rather than using a list, which has no type information, using the function `proof` signals that this represents a proof.  The use of keys, e.g. `"assume"` is more meaningful than numbered steps and it also allows steps to be inserted without re-numbering the steps in a proof.
+
+For example, if we have theorem  "\(n\) is odd if and only if \(n^2\) is odd", then we define its proof as a tree using
+
+    proof_ans:proof_iff(proof(1,2,3,4,5),proof(6,7,8,9,10,11));
+
+Really this means the proof is an if and only if proof (`proof_iff`) with two blocks, themselves proofs.  The sub-proofs are the most basic proof type, which is a list of steps, e.g. `proof(1,2,3,4,5)`.   The steps of a proof are integer indexes to the `proof_steps` list.  We deal with indexes, not strings, to simplify the representation and manipulation of the proof trees.

stack/2025012100/maxima/contrib/proofsamples/inf-primes.mac

+/****************************************************************/
+thm:"There are infinitely many prime numbers.";
+
+
+/****************************************************************/
+proof_steps: [
+    ["assume",    "Assume, for a contradiction, that there are only a finite number of prime numbers."],
+    ["false_hyp", "List all the prime numbers \\( p_1, p_2, \\cdots, p_n\\)."],
+    ["obs1",      "Every natural number is either a member of this list, or is divisible by a number on this list."],
+    ["gadget",    "Consider \\(N=p_1\\times p_2 \\times \\cdots \\times p_n +1.\\)"],
+
+    ["notmem1",   "For all \\(k=1,\\cdots, n\\) the number \\(N > p_k\\)"],
+    ["notmem2",   "Hence \\(N\\neq p_k\\)."],
+    ["notmem3",   "Therefore \\(N\\) is not a member of the list."],
+
+    ["div1",      "For all \\(k=1,\\cdots, n\\) when we divide \\(N\\) by \\(p_k\\) we get remainder \\(1\\)."],
+    ["div2",      "Hence \\(N\\) is not divisible by any \\(p_k\\)."],
+
+    ["contra1",   "\\(N\\) is not a member of the list and is not divisible by a number on this list."],
+    ["contra2",   "This contradicts the fact that every number is either a member of this list, or is divisible by a number on this list."],
+    ["conc",      "Therefore the list of prime numbers is not finite."]
+    ];
+
+/* This is how the teacher defines their answer, as nested proofs. */
+proof_ans:proof(1,2,3,4,proof_c(proof(5,6,7),proof(8,9)),10,11,12);
+proof_ans:proof("assume","false_hyp","obs1","gadget",proof_c(proof("notmem1","notmem2","notmem3"),proof("div1","div2")),"contra1","contra2","conc");
\ No newline at end of file

stack/2025012100/maxima/contrib/proofsamples/irrational-power-irrational.mac

+/****************************************************************/
+thm:"An irrational power of an irrational number can be rational.";
+
+
+/****************************************************************/
+proof_steps: [
+    ["gadget",     "Consider \\(a=\\sqrt{2}^{\\sqrt{2}}\\)."],
+    ["cases",      "Note there are exactly two cases: \\(a\\) is either rational or irrational."],
+    ["rat-hyp",    "Assume \\(a=\\sqrt{2}^{\\sqrt{2}}\\) is rational."],
+    ["conc",       "Then, we have an example where an irrational power of an irrational number can be rational."],
+    ["irrat-hyp",  "Assume \\(a=\\sqrt{2}^{\\sqrt{2}}\\) is irrational."],
+    ["irrat-1",    "Consider \\(\\left(\\sqrt{2}^{\\sqrt{2}}\\right)^{\\sqrt{2}}\\)."],
+    ["irrat-2",    "\\(\\left(\\sqrt{2}^{\\sqrt{2}}\\right)^{\\sqrt{2}}= \\sqrt{2}^{\\sqrt{2}\\times \\sqrt{2}} = \\sqrt{2}^2 = 2\\)."]
+];
+
+/* This is how the teacher defines their answer, as nested proofs. */
+proof_ans:proof_cases(proof("gadget","cases"),proof("rat-hyp","conc"),proof("irrat-hyp","irrat-1","irrat-2","conc"));

stack/2025012100/maxima/contrib/proofsamples/log-two-three-irrational.mac

+/****************************************************************/
+thm:"\\(\\log_2(3)\\) is irrational.";
+
+/****************************************************************/
+proof_steps: [
+    ["assume",    "Assume, for a contradiction, that \\(\\log_2(3)\\) is rational."],
+    ["defn_rat",  "Then \\(\\log_2(3) = \\frac{p}{q}>0\\) where "],
+    ["defn_rat2", "\\(p\\) and \\(q\\neq 0\\) are positive integers.",
+                  "This is the definition of rational number."],
+    ["defn_log",  "Using the definition of logarithm:",
+                  "Recall that \\(\\log_a(b)=x \\Leftrightarrow a^x=b\\)."],
+    ["defn_log2", "\\( 3 = 2^{\\frac{p}{q}}\\)"],
+    ["con",       "if and only if"],
+    ["alg",       "\\( 3^q = 2^p\\)"],
+    ["alg_int",   "The left hand side is always odd and the right hand side is always even."],
+    ["contra",    "This is a contradiction.",
+                  "Notice this is a genuine contradiction, making it difficult to reformulate as a contrapositive."],
+    ["conc",      "Hence \\(\\log_2(3)\\) is irrational."]
+];
+
+/****************************************************************/
+/* It is possible to add in extra, unnecessary.                 */
+/****************************************************************/
+wrong_steps:[
+    ["assume2",   "Assume, for a contradiction, that \\(\\log_2(3)\\) is irrational."],
+    ["defn_log3", "\\( 2 = 3^{\\frac{p}{q}}\\)"],
+    ["alg2",      "\\( 2^q = 3^p\\)"],
+    ["alg_int2",  "The right hand side is always odd and the left hand side is always even."]
+];
+/* Remove this comment to use them!
+proof_steps:append(proof_steps,wrong_steps);
+*/
+
+/****************************************************************/
+proof_ans:proof("assume","defn_rat","defn_rat2","defn_log","defn_log2","con","alg","alg_int","contra","conc");
+

stack/2025012100/maxima/contrib/proofsamples/odd-squaredodd.mac

+/****************************************************************/
+thm:"\\(n\\) is odd if and only if \\(n^2\\) is odd.";
+
+/****************************************************************/
+proof_steps: [
+    ["assodd",     "Assume that \\(n\\) is odd.",
+                   "This is the hypothesis in the first half of an if any only if proof"],
+    ["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\\).",
+                   "Notice we have satisfied the algebraic definition that \\(n^2\\) is an odd number."],
+    ["conc_odd",   "Hence \\(n^2\\) is odd.",
+                   "This is the conclusion in the first half of an if any only if proof"],
+
+    ["contrapos",  "We reformulate \"\\(n^2\\) is odd \\(\\Rightarrow \\) \\(n\\) is odd \" as the contrapositive.",
+                   "This reformulation enables us to start with \\(n\\) and not start with \\(n^2\\) which is simpler."],
+    ["assnotodd",  "Assume that \\(n\\) is not odd.",
+                   "This is the reformulated hypothesis in the second half of an if any only if proof"],
+    ["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.",
+                   "This is the conclusion in the second half of an if any only if proof"
+    ]
+];
+
+/****************************************************************/
+/* This is how the teacher defines their answer, as nested proofs. */
+proof_ans:proof_iff(proof(1,2,3,4,5),proof(6,7,8,9,10,11));
+proof_ans:proof_iff(proof("assodd","defn_odd","alg_odd","def_M_odd","conc_odd"),proof("contrapos","assnotodd","even","alg_even","def_M_even","conc_even"));

stack/2025012100/maxima/contrib/proofsamples/root-two-irrational.mac

+/****************************************************************/
+thm:"\\(\\sqrt{2}\\) is irrational.";
+
+
+/****************************************************************/
+proof_steps: [
+    ["assume",     "Assume, for a contradiction, that \\(\\sqrt{2}\\) is rational."],
+    ["defn_rat",   "Then there exist integers \\(p\\) and \\(q\\neq 0\\) such that"],
+    ["defn_rat2",  "\\( \\sqrt{2} = \\frac{p}{q}.\\)"],
+    ["ass_low",    "We can assume that \\(p\\) and \\(q\\) have no common factor, otherwise we can cancel these out."],
+    ["alg1",       "Squaring both sides"],
+    ["alg2",       "\\( 2 = \\frac{p^2}{q^2}\\)"],
+    ["alg3",       "\\( 2q^2=p^2\\)"],
+    ["p2_even",    "Therefore \\(p^2\\) is even."],
+    ["p_even",     "Hence \\(p\\) is even."],
+    ["def_even",   "Say \\(p=2r\\)."],
+    ["sub1",       "Substituting this gives"],
+    ["sub2",       "\\( 2q^2=(2r)^2\\)"],
+    ["sub3",       "\\( 2q^2=4r^2\\)"],
+    ["sub4",       "\\( q^2=2r^2\\)"],
+    ["q2_even",    "Therefore \\(q^2\\) is even."],
+    ["q_even",     "Hence \\(q\\) is even."],
+    ["both_even",  "We have proved that both \\(p\\) and \\(q\\) are even."],
+    ["com_fac",    "This means they have a common factor of \\(2\\)."],
+    ["cont",       "This contradicts the assumption that \\(p\\) and \\(q\\) have no common factor."]
+];
+
+/* This is how the teacher defines their answer, as nested proofs. */
+proof_ans:proof(1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19);
+proof_ans:proof("assume","defn_rat","defn_rat2","ass_low","alg1","alg2","alg3","p2_even","p_even","def_even","sub1","sub2","sub3","sub4","q2_even","q_even","both_even","com_fac","cont");

stack/2025012100/maxima/contrib/proofsamples/set-equality.mac

+/****************************************************************/
+thm:"Let \\(f: X \\to Y\\) be a function, and assume that \\(A,B \\subset X\\), and \\(C,D \\subset Y\\) are all non-empty. Then \\(f^{-1}(Y \\setminus C) = X \\setminus f^{-1}(C)\\).";
+
+/****************************************************************/
+proof_steps: [
+    ["defn_eq",  "To prove set equality \\(V=W\\) we have to prove two cases: (i) \\(V\\subseteq W\\), and (ii) \\(W\\subseteq V\\)."],
+    ["assume_A", "Let \\( x\\in f^{-1}(Y\\setminus C) \\)."],
+    ["step_a",   "Then \\( f(x)\\in Y\\setminus C \\)."],
+    ["step_b",   "This implies \\( f(x)\\not\\in C \\)."],
+    ["step_c",   "Hence \\( x\\not\\in f^{-1}(C) \\)."],
+    ["conc_A",   "Hence \\(x\\in  X \\setminus f^{-1}(C)\\)."],
+    ["assume_B", "Let \\( x\\in X \\setminus f^{-1}(C)\\)."],
+    ["conc_B",   "Hence \\(x\\in  f^{-1}(Y \\setminus C)\\)."]
+];
+
+/****************************************************************/
+/* This is how the teacher defines their answer, as nested proofs. */
+proof_ans:proof_cases(1,proof(2,3,4,5,6),proof(7,5,4,3,8));
+proof_cases("defn_eq",proof("assume_A","step_a","step_b","step_c","conc_A"),proof("assume_B","step_c","step_b","step_a","conc_B"));
+ 

stack/2025012100/maxima/contrib/proofsamples/sum-odd-int.mac

+/****************************************************************/
+thm:"The sum of the first \\(n\\) odd integers, starting from one, is \\(n^2\\).";
+
+
+/****************************************************************/
+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."]
+];
+
+/****************************************************************/
+proof_ans:proof_ind(1,proof(2,3),proof(5,6,7,8),9);
+proof_ans:proof_ind("defn_p",proof("base_hyp","base_conc"),proof("ind_1","ind_2","ind_3","ind_conc"),"concp");
\ No newline at end of file

stack/2025012100/maxima/contrib/validators.mac

+/*  Author Chris Sangwin
+    University of Edinburgh
+    Copyright (C) 2023 Chris Sangwin
+
+    This program is free software: you can redistribute it or modify
+    it under the terms of the GNU General Public License version two.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+    GNU General Public License for details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program. If not, see <http://www.gnu.org/licenses/>. */
+
+/****************************************************************/
+/*  Bespoke validators for STACK inputs                         */
+/*                                                              */
+/*  Chris Sangwin, <C.J.Sangwin@ed.ac.uk>                       */
+/*  V1.0 June 2023                                              */
+/*                                                              */
+/*  Please use this file to add public bespoke validators.      */
+/*                                                              */
+/****************************************************************/
+
+/* The student may not use an underscore anywhere in their input. */
+
+validate_underscore(ex) := if is(sposition("_", string(ex)) = false) then "" 
+        else "Underscore characters are not permitted in this input.";
+
+/* Add in unit-test cases using STACK's s_test_case function.  At least two please! */
+/* Place test cases in validators_test.mac                                          */
+
+/* The student may not use a user-defined function, or arrays, anywhere in their input. */
+validate_nofunctions(ex):= block([op1,opp],
+  if atom(ex) then return(""),
+  op1:ev(op(ex)),
+  opp:apply(properties, [op1]),
+  if ev(emptyp(opp) or is(opp=[noun]),simp) then return(sconcat("User-defined functions are not permitted in this input. In your answer ", stack_disp(op1, "i"), " appears to be used as a function. ")),
+  apply(sconcat, map(validate_nofunctions, args(ex)))
+);
+
+/* The student may only use single-character variable names in their answer. */
+/* This is intended for use when Insert Stars is turned off, but we still want to indicate to students that they may have forgotten a star */
+validate_all_one_letter_variables(ex) := if not(is(ev(lmax(map(lambda([ex2],slength(string(ex2))),listofvars(ex))),simp)>1)) then ""
+        else "Only single-character variable names are permitted in this input. Perhaps you forgot to use an asterisk (*) somewhere, or perhaps you used a Greek letter.";
+
+/* This provides more detailed feedback for students who try to enter fully closed or open intervals using [] or () instead of cc(a,b) or oo(a,b). */
+/* It is intended for early courses where students might be new to using this written notation and STACK. */
+/* This does not work well with "Check type of response" turned on, and provides slightly awkward feedback when students take a union of multiple intervals with incorrect syntax. */
+validate_interval_syntax(ex):= block(
+  if ev(listp(ex),simp) then return(sconcat("To give a closed interval, use <code>cc(",first(args(ex)),",",second(args(ex)),")</code>, not <code>[",first(args(ex)),",",second(args(ex)),"]</code>. "))
+  else if ev(ntuplep(ex),simp) then return(sconcat("To give an open interval, use <code>oo(",first(args(ex)),",",second(args(ex)),")</code>, not <code>(",first(args(ex)),",",second(args(ex)),")</code>. "))
+  else if is(safe_op(ex)="%union") then apply(sconcat, map(validate_interval_syntax, args(ex)))
+  else return("")
+);