Skip to content
Snippets Groups Projects
Commit 25398600 authored by Lennart Kramer's avatar Lennart Kramer
Browse files

add stackmaxima 2024012900

parent 7308b822
No related branches found
No related tags found
No related merge requests found
Showing
with 4280 additions and 1 deletion
......@@ -89,6 +89,7 @@ What Stackmaxima version do I need?
| - | `4.4.5` | 2023072101 | 5.44.0 |
| - | `4.4.6` | 2023102700 | 5.44.0 |
| - | `4.5.0` | 2023121100 | 5.44.0 |
| - | `4.5.0-hf2` | 2024012900 | 5.44.0 |
Environment Variables
......
version: "3.3"
services:
maxima:
image: mathinstitut/goemaxima:${STACKMAXIMA_VERSION:-2023121100}-latest
image: mathinstitut/goemaxima:${STACKMAXIMA_VERSION:-2024012900}-latest
ports:
- 0.0.0.0:8080:8080
tmpfs:
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
/****************************************************************/
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");
# 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.
/****************************************************************/
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
/****************************************************************/
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"));
/****************************************************************/
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");
/****************************************************************/
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"));
/****************************************************************/
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");
/****************************************************************/
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"));
/****************************************************************/
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
/* 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! */
s_test_case(validate_underscore(1+a1), "");
s_test_case(validate_underscore(1+a_1), "Underscore characters are not permitted in this input.");
/* The student may not use a user-defined function, or arrays, anywhere in their input. */
validate_nofunctions(ex):= block([op1],
if atom(ex) then return(""),
op1:ev(op(ex)),
op1:apply(properties, [op1]),
if ev(emptyp(op1) or is(op1=[noun]),simp) then return("User-defined functions are not permitted in this input."),
apply(sconcat, map(validate_nofunctions, args(ex)))
);
s_test_case(validate_nofunctions(1+a1), "");
s_test_case(validate_nofunctions(sin(n*x)), "");
s_test_case(validate_nofunctions(-b#pm#sqrt(b^2-4*a*c)), "");
s_test_case(validate_nofunctions(x(2)), "User-defined functions are not permitted in this input.");
s_test_case(validate_nofunctions(x(t)), "User-defined functions are not permitted in this input.");
s_test_case(validate_nofunctions(1+f(x+1)), "User-defined functions are not permitted in this input.");
/* 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.";
s_test_case(validate_all_one_letter_variables(1), "");
s_test_case(validate_all_one_letter_variables((A*x+B)/(x^2+1) + C/x), "");
s_test_case(validate_all_one_letter_variables((Ax+B)/(x^2+1) + C/x), "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.");
s_test_case(validate_all_one_letter_variables((theta*x+B)/(x^2+1) + C/x), "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.");
/* Author Luke Longworth
University of Canterbury
Copyright (C) 2023 Luke Longworth
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/>. */
/****************************************************************/
/* Vector calculus functions for STACK */
/* */
/* V1.0 June 2023 */
/* */
/****************************************************************/
/****************************************************************/
/* Calculate the divergence of a vector-valued function */
/****************************************************************/
div(u, vars):= block([div_vec],
if not(listp(vars)) or emptyp(vars) then error("div: the second argument must be a list of variables."),
if matrixp(u) then funcs: list_matrix_entries(u) else funcs: flatten(u),
/* TODO: confirm div should always simplify? */
div_vec: map(lambda([ex], ev(diff(funcs[ex],vars[ex]), simp)), ev(makelist(ii,ii,1,length(vars)), simp)),
return(apply("+", div_vec))
);
s_test_case(div([x^2*cos(y),y^3],[x,y]), 2*x*cos(y)+3*y^2);
s_test_case(div(transpose(matrix([x^2*cos(y),y^3])),[x,y]), 2*x*cos(y)+3*y^2);
s_test_case(div(matrix([x^2*cos(y),y^3]),[x,y]), 2*x*cos(y)+3*y^2);
/****************************************************************/
/* Calculate the curl of a vector-valued function */
/****************************************************************/
curl(u,vars):= block([cux, cuy, cuz],
if not(listp(vars)) or emptyp(vars) then error("curl: the second argument must be a list of 3 variables."),
if matrixp(u) then [ux,uy,uz]: list_matrix_entries(u) else [ux,uy,uz]: flatten(u),
cux: diff(uz,vars[2]) - diff(uy,vars[3]),
cuy: diff(ux,vars[3]) - diff(uz,vars[1]),
cuz: diff(uy,vars[1]) - diff(ux,vars[2]),
return(transpose(matrix([cux,cuy,cuz])))
);
/* Author Chris Sangwin
University of Birmingham
Copyright (C) 2013 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/>. */
/* THIS IS EXPERIMENTAL CODE */
/* Most of the code is now in noun_simp.mac. This is the remainder. */
/*******************************************/
/* Control functions */
/*******************************************/
DIS_TRANS:["disAddMul"]$
POW_TRANS:["powLaw"]$
BUG_RULES:["buggyPow","buggyNegDistAdd"]$
/* Is the rule applicable at the top level? */
trans_topp(ex,rl):=apply(parse_string(sconcat(rl,"p")),[ex])$
/* Is the rule applicable anywhere in the expression? */
trans_anyp(ex, rl):=block(
if atom(ex) then return(trans_topp(ex,rl)),
if trans_topp(ex,rl) then return(true),
apply("or",maplist(lambda([ex2],trans_anyp(ex2,rl)),args(ex)))
)$
/* Identify applicable rules at the top level */
trans_top(ex):=sublist(ALL_TRANS, lambda([ex2],trans_topp(ex,ex2)))$
/* Identify applicable rules */
trans_any(ex):=sublist(ALL_TRANS, lambda([ex2],trans_anyp(ex,ex2)))$
/*******************************************/
/* Higher level control functions */
/*******************************************/
/* Very inefficient! */
/* Has the advantage that the whole expression is always visible at the top level */
step_through(ex):=block([rls],
rls:trans_any(ex),
if emptyp(rls) then return(ex),
print(string(ex)),
print(rls),
step_through(transr(ex,first(rls)))
)$
/* This only looks at the top level for rules which apply. If none, we look deeper. */
/* This is much more efficient */
step_through2(ex):=block([rls,rl,ex2],
if atom(ex) then return(ex),
rls:trans_top(ex),
if emptyp(rls) then return(block([ex2], ex2:map(step_through2,ex), if ex=ex2 then ex else step_through2(ex2))),
rl:first(rls),
ex2:apply(parse_string(rl),[ex]),
print([ex,rl,ex2]),
if ex=ex2 then ex else step_through2(ex2)
)$
/* Assume some rules are just applied in the background */
step_through3(ex):=block([rls],
rls:sublist(ALG_TRANS, lambda([ex2],trans_anyp(ex,ex2))),
if not(emptyp(rls)) then return(step_through3(transr(ex,first(rls)))),
rls:trans_any(ex),
if emptyp(rls) then return(ex),
print(string(ex)),
print(rls),
step_through3(transr(ex,first(rls)))
)$
/* removes elements of l1 from l2. */
removeoncelist(l1,l2):=block(
if listp(l2)#true or emptyp(l2) then return([]),
if listp(l1)#true or emptyp(l1) then return(l2),
if element_listp(first(l1),l2) then return(removeoncelist(rest(l1),removeonce(first(l1),l2))),
removeoncelist(rest(l1),l2)
)$
/* A special function.
If a\in l1 is also in l2 then remove a and -a from l2.
Used on negDef */
removeoncelist_negDef(l1,l2):=block(
if listp(l2)#true or emptyp(l2) then return([]),
if listp(l1)#true or emptyp(l1) then return(l2),
if element_listp(first(l1),l2) then return(removeoncelist_negDef(rest(l1),removeonce("-"(first(l1)),removeonce(first(l1),l2)))),
removeoncelist_negDef(rest(l1),l2)
)$
/*******************************************/
/* Transformation rules (not used) */
/*******************************************/
/* -1*x -> -x */
negMinusOnep(ex):=block(
if safe_op(ex)#"*" then return(false),
if is(first(args(ex))=negInt(-1)) then return(true) else return(false)
)$
negMinusOne(ex):=block(
if negMinusOnep(ex)#true then return(ex),
if length(args(ex))>2 then "-"(apply("*",rest(args(ex)))) else -second(args(ex))
)$
/* a-a -> 0 */
/* This is a complex function. If "a" and "-a" occur as arguments in the sum
then we remove the first occurance of each. Then we add the remaining arguments.
Hence, this does not flatten arguments or re-order them, but does cope with nary-addition
*/
negDefp(ex):=block([a0,a1,a2,a3],
if safe_op(ex)#"+" then return(false),
a1:maplist(first,sublist(args(ex), lambda([ex2],safe_op(ex2)="-"))),
a2:sublist(args(ex), lambda([ex2],safe_op(ex2)#"-")),
any_listp(lambda([ex2],element_listp(ex2,a2)),a1)
)$
negDef(ex):=block([a0,a1,a2,a3],
if negDefp(ex)#true then return(ex),
a0:args(ex),
a1:maplist(first,sublist(args(ex), lambda([ex2],safe_op(ex2)="-"))),
a2:sublist(args(ex), lambda([ex2],safe_op(ex2)#"-")),
a3:removeoncelist_negDef(a1,a0),
if emptyp(a3) then 0 else apply("+",a3)
)$
/* Distributes "-" over addition */
negDistAddp(ex):=block(
if safe_op(ex)#"-" then return(false),
if safe_op(part((ex),1))="+" then true else false
)$
negDistAdd(ex):=block(
if negDistAddp(ex) then map("-",part((ex),1)) else ex
)$
/*******************************************/
/* Division rules */
/* a/a -> 1 */
idDivp(ex):= if safe_op(ex)="/" and part(ex,1)=part(ex,2) and part(ex,2)#0 then true else false$
idDiv(ex) := if idDivp(ex) then 1 else ex$
/*******************************************/
/* Distribution rules */
/* Write (a+b)*c as a*c+b*c */
disAddMulp(ex):= if safe_op(ex)="*" then
if safe_op(last(ex))="+" then true else false$
disAddMul(ex):= block([S,P],
S:last(ex),
P:reverse(rest(reverse(args(ex)))),
P:if length(P)=1 then first(P) else apply("*", P),
S:map(lambda([ex], P*ex), S)
)$
/*******************************************/
/* Power rules */
/* Write a*a^n as a^(n+m) */
powLawp(ex):= block([B],
if not(safe_op(ex)="*") then return(false),
B:sort(maplist(lambda([ex], if safe_op(ex)="^" then first(args(ex)) else ex), args(ex))),
if emptyp(powLawpduplicates(B)) then return(false) else return(true)
)$
powLawpduplicates(l):=block(
if length(l)<2 then return([]),
if first(l)=second(l) then return([first(l)]),
return(powLawpduplicates(rest(l)))
)$
powLaw(ex):= block([B,l1,l2],
B:sort(maplist(lambda([ex], if safe_op(ex)="^" then first(args(ex)) else ex), args(ex))),
B:first(powLawpduplicates(B)),
l1:sublist(args(ex), lambda([ex], is(ex=B) or (is(safe_op(ex)="^") and is(first(args(ex))=B)))),
l1:maplist(lambda([ex], if is(ex=B) then 1 else second(args(ex))), l1),
l2:sublist(args(ex), lambda([ex], not(is(ex=B) or (is(safe_op(ex)="^") and is(first(args(ex))=B))))),
if l2=[] then return(B^apply("+",l1)),
if length(l2)=1 then l2:first(l2) else l2:apply("*",l2),
return(B^apply("+",l1)*l2)
);
;; Custom version of erromsg() to collect the error as
;; a string after it has been formatted
;; Matti Harjula 2019
(defmfun $errormsgtostring ()
"errormsgtostring() returns the maxima-error message as string."
(apply #'aformat nil (cadr $error) (caddr (process-error-argl (cddr $error))))
)
/* Author Chris Sangwin
University of Birmingham
Copyright (C) 2006 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/>. */
/* Expand tutorial. */
/* This file should take a product and expand out one level in steps */
/* Chris Sangwin, 6/11/2006 */
/* This is experimental code, but may be useful. */
COLOR_LIST:["red", "Blue" , "YellowOrange", "Bittersweet" , "BlueViolet" , "Aquamarine", "BrickRed" , "Apricot" , "Brown" , "BurntOrange", "CadetBlue" , "CarnationPink" , "Cerulean" , "CornflowerBlue" , "CyanDandelion" , "DarkOrchid" , "Emerald" , "ForestGreen" , "Fuchsia", "Goldenrod" , "Gray" , "Green" , "JungleGreen", "Lavender" , "LimeGreen" , "Magenta" , "Mahogany" , "Maroon" , "Melon", "MidnightBlue" , "Mulberry" , "NavyBlue" , "OliveGreen" , "Orange", "OrangeRed" , "Orchid" , "Peach" , "Periwinkle" , "PineGreen" , "Plum", "ProcessBlue" , "Purple" , "RawSienna" , "Red" , "RedOrange" , "RedViolet" , "Rhodamine" , "RoyalBlue" , "RoyalPurple" , "RubineRed", "Salmon" , "SeaGreen" , "Sepia" , "SkyBlue" , "SpringGreen" , "Tan", "TealBlue" , "Thistle" , "Turquoise" , "Violet" , "VioletRed" ,"WildStrawberry" , "Yellow" , "YellowGreen" , "BlueGreen" ]$
COLOR_LIST_LENGTH:length(COLOR_LIST)$
/* We want a list of the summands, but you cannot apply args to an atom */
make_args_sum(ex) := if atom(ex) then [ex] else
if op(ex)#"+" then [ex] else args(ex)$
/* Adds up the elements of a list */
sum_list(ex) := if listp(ex) then
if length(ex)=1 then ex[1] else apply("+",ex)
else ex$
/* Multiplies together the elements of a list */
product_list(ex) := if listp(ex) then
if length(ex)=1 then ex[1] else apply("*",ex)
else ex$
make_product(ex) := product_list(maplist(sum_list,ex))$
/******************************************************************/
/* A "step" is a list representing a row in a three column matrix */
/* eg [ [], [], [] ] */
/* display a single step, returning a string */
display_step(ex) := block([ret,ex1,ex2,ex3],
ex1:" ", ex2:" = ", ex3:" ",
if []#ex[1] then ex1:StackDISP(ex[1][1],""),
if []=ex[2] then ex2:" " else
if ex[2][1]#"=" then ex2:StackDISP(ex[2][1],""),
if []#ex[3] then ex3:StackDISP(ex[3][1],""),
apply(concat,[ex1," & ",ex2," & ",ex3," \\\\ "])
)$
/* Takes a list of steps in a problem, and returns a single LaTeX string */
display_steps(ex) := block([ret],
if atom(ex) then return(StackDISP(ex,"")),
if listp(ex)#true then return(StackDISP(ex,"")),
/* */
steps:map(display_step,ex),
ret:append(["\\begin{array}{rcl}"],flatten(steps),[" \\end{array} "]),
ret:apply(concat,ret)
)$
/******************************************************************/
/* Tutorial expand. This function expands out the expression ex */
/* It returns a list of steps */
tut_expand_one_level(ex) := block([args_ex,args_ex1,cur_step,ret],
/* Make sure we apply this function to a product */
if atom(ex) then return([ [[ex],[],[]] ]),
if op(ex)#"*" then return([ [[ex],[],[]] ]),
/* Get a list of lists with the arguments of ex */
args_ex:args(ex),
args_ex:maplist(make_args_sum,args_ex),
/* colour the first summands */
cur_step:cons(zip_with(texcolor,COLOR_LIST,first(args_ex)),rest(args_ex)),
ret:[ [[ex],["="],[make_product(cur_step)]] ],
/* */
ex1:args_ex[1],
ex2:args_ex[2],
ex3:rest(args_ex,2),
cur_step:maplist(lambda([x],x*sum_list(ex2)),ex1),
cur_step:cons(zip_with(texcolor,COLOR_LIST,cur_step),ex3),
ret:cons([[],["="],[make_product(cur_step)]],ret),
/* */
cur_step:maplist(lambda([x],maplist(lambda([y],x*y),ex2)),ex1),
cur_step:maplist(sum_list,cur_step),
cur_step:zip_with(texcolor,COLOR_LIST,cur_step),
cur_step:make_product(cons(cur_step,ex3)),
ret:cons([[],["="],[cur_step]],ret),
/* */
cur_step:maplist(lambda([x],maplist(lambda([y],x*y),ex2)),ex1),
cur_step:maplist(sum_list,cur_step),
/* BUG: this should only be "one step" of simplification. Currently it does everthing */
cur_step:ev(sum_list(cur_step),simp),
cur_step:if ex3=[] then cur_step else make_product(cons(cur_step,ex3)),
ret:cons([[],["="],[cur_step]],ret),
/* */
reverse(ret)
)$
/* Tutorial expand. This function expands out the expression ex */
tut_expand_all_levels(ex) := block([args_ex,first_ex],
if atom(ex) then return([ [[ex],[],[]] ]),
if op(ex)#"*" then return([ [[ex],[],[]] ]),
/* first step */
args_ex:args(ex),
first_ex:ev(expand(args_ex[1]*args_ex[2]),simp),
if length(args_ex)>2 then
append(tut_expand_one_level(ex), [ [["and"],[],[]] ], tut_expand_all_levels(product_list(cons(first_ex,rest(args_ex,2)))))
else
tut_expand_one_level(ex)
)$
tut_expand_full(ex) := block([ret,seps],
ret:tut_expand_all_levels(ex),
ret:append(ret,[ [["Hence"],[],[]], [[ex],["="],[ev(expand(ex),simp)]] ]),
display_steps(ret)
)$
/* Author Chris Sangwin
Lougborough University
Copyright (C) 2015 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/>. */
/* THIS IS EXPERIMENTAL CODE */
/* Currently this is under development by CJS and is not connected to the main STACK codebase */
/* It sits here because the long-term goal is to incorporate it */
/* More general random function - recurses across the structure.
Notice the use of the dummy "protect()" function to stop further evaluation.
E.g.
rand_recurse((5+protect(2))*x^protect(2)+3*x+7);
rand_recurse(sin([x,y,z]));
*/
rand_recurse(ex) := block(
if (integerp(ex) or floatnump(ex) or matrixp(ex) or listp(ex)) then return(rand(ex)),
if atom(ex) then return(ex),
if op(ex)=protect then return(first(args(ex))),
apply(op(ex), maplist(rand_recurse, args(ex)))
);
/* Truncates a polynomial to only terms of degree "d" or less - always expands out */
poly_truncate(pa,d) := apply("+",maplist(lambda([ex],if hipow(ex,x)>d then 0 else ex), args(expand(pa))));
/****************************************************************/
/* Square root functions for STACK */
/* */
/* Chris Sangwin, <C.J.Sangwin@ed.ac.uk> */
/* V0.1 August 2015 */
/* */
/****************************************************************/
/* With simp:false */
/* Some examples:
p1: (2 + sqrt (2)) * sqrt (2);
p2:distrib(p1);
p3:sqrt(a)*sqrt(b)*sqrt(b)*sqrt(b)*sqrt(a)*1*sqrt(b)+1;
*/
naivesqrt(ex):=block([al],
if atom(ex) then return(ex),
al:args(ex),
if safe_op(ex)="*" then block([alp,alq],
alp:sort(sublist(args(ex), lambda([ex2],equal(safe_op(ex2),"sqrt")))),
alq:sublist(args(ex), lambda([ex2],not(equal(safe_op(ex2),"sqrt")))),
al:append(naivesqrthelper(alp),alq)
),
if safe_op(ex)="*" and length(al)=1 then return(naivesqrt(first(al))),
apply(op(ex), map(naivesqrt, al))
);
naivesqrthelper(ex):=block(
if length(ex)<2 then return(ex),
if equal(first(ex), second(ex)) then return(append([first(args(first(ex)))], naivesqrthelper(rest(rest(ex))))),
append([first(ex)], naivesqrthelper(rest(ex)))
);
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment