Big algebraic solver

The big algebraic software is a tactical theorem prover written as a STELF logic program by Rob at Princeton University as part of the Foundational Proof Carrying Code system. It is quite inefficient due to the fact that it doesn’t try to order variables. The [http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.UsingTheRingSolver RingSolver] in the Agda standard library is an example of a more efficient solver.

Preexisting logic

In the Princeton FPCC project where this was developed, many of the definitions below were more general (for instance, equality was on anything, not just numbers) and many things stated here as axioms were lemmas that had corresponding proofs. These are just the definitions and lemmas that were used within the solver.

%sort tnum %.
%sort tform %.
%sort pf {_ tform} %.
%term imp %pi tform %-> tform %-> tform %.
%prec %right 10 imp %.
%term and %pi tform %-> tform %-> tform %.
%prec %right 12 and %.
%term == %pi tnum %-> tnum %-> tform %.
%prec %none 18 == %.
%term >= %pi tnum %-> tnum %-> tform %.
%prec %none 18 >= %.
%term < %pi tnum %-> tnum %-> tform %.
%prec %none 18 < %.
%term != %pi tnum %-> tnum %-> tform %.
%prec %none 18 != %.
%define > (%pi tnum %-> tnum %-> tform) [x] [y] y < x %.
%prec %none 18 > %.
%define <= (%pi tnum %-> tnum %-> tform) [x] [y] y >= x %.
%prec %none 18 <= %.
%term imp_i %pi (%pi (pf A) %-> (pf B)) %-> (pf (A imp B)) %.
%term imp_e %pi (pf (A imp B)) %-> (pf A) %-> (pf B) %.
%term and_i %pi (pf A) %-> (pf B) %-> (pf (A and B)) %.
%term and_e1 %pi (pf (A and B)) %-> (pf A) %.
%term and_e2 %pi (pf (A and B)) %-> (pf B) %.
%term cut %pi (pf A) %-> (%pi (pf A) %-> (pf B)) %-> (pf B) %.
%term cut2 %pi (pf A) %-> (pf A') %-> (%pi (pf A) %-> (pf A') %-> (pf B)) %-> (pf B) %.
%term cut3
  %pi (pf A)
  %-> (pf A')
  %-> (pf A'')
  %-> (%pi (pf A) %-> (pf A') %-> (pf A'') %-> (pf B))
  %-> (pf B) %.
%term congr {h %pi tnum %-> tform} %pi (pf (A == B)) %-> (pf (h B)) %-> (pf (h A)) %.
%term gt->geq %pi (pf (A > B)) %-> (pf (A >= B)) %.
%term gt->neq %pi (pf (A > B)) %-> (pf (A != B)) %.
%term lt->neq %pi (pf (A < B)) %-> (pf (A != B)) %.
%term eq->geq %pi (pf (A == B)) %-> (pf (A >= B)) %.
%term eq->leq %pi (pf (A == B)) %-> (pf (A <= B)) %.
%term not_eie %pi (pf (A != B)) %-> (%pi (pf (C == D)) %-> (pf (A == B))) %-> (pf (C != D)) %.
%term not_ein %pi (pf (A < B)) %-> (%pi (pf (C >= D)) %-> (pf (A >= B))) %-> (pf (C < D)) %.
%term zero tnum %.
%term one tnum %.
%term one>zero pf (one > zero) %.
%term + %pi tnum %-> tnum %-> tnum %.
%prec %left 22 + %.
%term * %pi tnum %-> tnum %-> tnum %.
%prec %left 23 * %.
%term neg %pi tnum %-> tnum %.
%define _ [a] [b] a + neg b %.
%prec %left 22 - %.
%define succ [x] x + one %.
%define pred [x] x - one %.
%define two succ one %.
%term refl pf (A == A) %.
%term symm %pi (pf (A == B)) %-> (pf (B == A)) %.
%term trans %pi (pf (A == B)) %-> (pf (B == C)) %-> (pf (A == C)) %.
%term trans3 %pi (pf (A == B)) %-> (pf (B == C)) %-> (pf (C == D)) %-> (pf (A == D)) %.
%term trans4
  %pi (pf (A == B))
  %-> (pf (B == C))
  %-> (pf (C == D))
  %-> (pf (D == E))
  %-> (pf (A == E)) %.
%term trans5
  %pi (pf (A == B))
  %-> (pf (B == C))
  %-> (pf (C == D))
  %-> (pf (D == E))
  %-> (pf (E == F))
  %-> (pf (A == F)) %.
%term trans_geq_eq %pi (pf (A >= B)) %-> (pf (B == C)) %-> (pf (A >= C)) %.
%term trans_eq_geq %pi (pf (A == B)) %-> (pf (B >= C)) %-> (pf (A >= C)) %.
%term comm_plus pf (A + B == B + A) %.
%term plus_zero pf (A + zero == A) %.
%term zero_plus pf (zero + A == A) %.
%term plus_cong %pi (pf (A == B)) %-> (pf (C == D)) %-> (pf (A + C == B + D)) %.
%define plus_cong2 (%pi (pf (A == B)) %-> (pf (C + A == C + B))) [p1] plus_cong refl p1 %.
%define plus_cong1 (%pi (pf (A == B)) %-> (pf (A + C == B + C))) [p1] plus_cong p1 refl %.
%term plus_assoc pf (A + B + C == A + (B + C)) %.
%define assoc_plus (pf (A + (B + C) == A + B + C)) symm plus_assoc %.
%term neg_plus pf (neg A + neg B == neg (A + B)) %.
%term plus_inv pf (A - A == zero) %.
%define inv_plus (pf (neg A + A == zero)) trans comm_plus plus_inv %.
%term geq_plus_cong1 %pi (pf (A >= B)) %-> (pf (A + C >= B + C)) %.
%term comm_times pf (A * B == B * A) %.
%term times_assoc pf (A * B * C == A * (B * C)) %.
%define assoc_times (pf (A * (B * C) == A * B * C)) symm times_assoc %.
%term times_assoc pf (A * B * C == A * (B * C)) %.
%term times_cong %pi (pf (A == B)) %-> (pf (C == D)) %-> (pf (A * C == B * D)) %.
%define times_cong2 (%pi (pf (A == B)) %-> (pf (C * A == C * B))) [p1] times_cong refl p1 %.
%define times_cong1 (%pi (pf (A == B)) %-> (pf (A * C == B * C))) [p1] times_cong p1 refl %.
%term neg_times1 pf (neg A * B == neg (A * B)) %.
%term neg_times2 pf (A * neg B == neg (A * B)) %.
%term neg_times pf (neg A * neg B == A * B) %.
%term times_one pf (A * one == A) %.
%define one_times (pf (one * A == A)) trans comm_times times_one %.
%term times_zero pf (A * zero == zero) %.
%term times_elim2 %pi (pf (A != zero)) %-> (pf (B * A == C * A)) %-> (pf (B == C)) %.
%term geq_times_cong1 %pi (pf (A >= zero)) %-> (pf (B >= C)) %-> (pf (B * A >= C * A)) %.
%term geq_times_elim1 %pi (pf (A > zero)) %-> (pf (A * B >= A * C)) %-> (pf (B >= C)) %.
%term geq_times_elim2 %pi (pf (A > zero)) %-> (pf (B * A >= C * A)) %-> (pf (B >= C)) %.
%term geq_times_cong1_neg %pi (pf (A <= zero)) %-> (pf (B >= C)) %-> (pf (B * A <= C * A)) %.
%term geq_times_elim2_neg %pi (pf (A < zero)) %-> (pf (B * A >= C * A)) %-> (pf (B <= C)) %.
%term neg_cong %pi (pf (A == B)) %-> (pf (neg A == neg B)) %.
%term neg_elim %pi (pf (neg A == neg B)) %-> (pf (A == B)) %.
%term neg_neg_e pf (neg (neg A) == A) %.
%term neg_zero pf (neg zero == zero) %.
%term distrib pf (A * (B + C) == A * B + A * C) %.
%term distrib_right pf (A + B * C == A * C + B * C) %.
%define cancel_a+b-b (pf (A + B - B == A)) symm (trans3 (symm plus_zero) (plus_cong2 (symm plus_inv)) assoc_plus) %.
%define cancel_a+b-b' (pf (A + (B - B) == A)) trans assoc_plus cancel_a+b-b %.
%define cancel_a-b+b (pf (A - B + B == A)) symm (trans4 (symm cancel_a+b-b) plus_assoc (plus_cong2 comm_plus) assoc_plus) %.
%define cancel_a-b+b' (pf (A + (neg B + B) == A)) trans assoc_plus cancel_a-b+b %.
%define cancel_a+b-a (pf (A + B - A == B)) symm (trans3 (symm cancel_a-b+b) comm_plus assoc_plus) %.
%define cancel_a+b-a' (pf (A + (B - A) == B)) trans assoc_plus cancel_a+b-a %.
%define cancel_a-a+b (pf (A - A + B == B)) trans3 comm_plus assoc_plus cancel_a+b-b %.
%define cancel_a-a+b' (pf (A + (neg A + B) == B)) trans assoc_plus cancel_a-a+b %.
%define cancel_-a+a+b (pf (neg A + A + B == B)) trans (plus_cong1 comm_plus) cancel_a-a+b %.
%define cancel_-a+a+b' (pf (neg A + (A + B) == B)) trans assoc_plus cancel_-a+a+b %.
%define cancel_-a+b+a (pf (neg A + B + A == B)) trans4 plus_assoc (plus_cong2 comm_plus) assoc_plus cancel_-a+a+b %.
%define cancel_-a+b+a' (pf (neg A + (B + A) == B)) trans assoc_plus cancel_-a+b+a %.

Parts of the solver

%define nomatch zero %.
%define match one %.
%define listify (%pi tnum %-> tnum %-> tnum %-> %type) [a] [pos] [neg] pf (a == pos - neg) %.
%deterministic listify %.
%mode listify %in %out %out %.

Normalization

%define plusify (%pi tnum %-> tnum %-> tnum %-> %type) [a] [x] [y] pf (a == x - y) %.
%deterministic plusify %.
%mode plusify %in %out %out %.
%define timesify (%pi tnum %-> tnum %-> tnum %-> tnum %-> %type) [b] [x] [y] [sign] pf (b * sign == x * y) %.
%deterministic timesify %.
%mode timesify %in %out %out %out %.
%define catchtimes (%pi tnum %-> tnum %-> tnum %-> tnum %-> tnum %-> tnum %-> tnum %-> %type) [a] [b] [x] [y] [sign] [pos] [neg] pf (b * sign == x * y imp a + b == pos - neg) %.
%deterministic catchtimes %.
%mode catchtimes %in %in %in %in %in %out %out %.

Matching

%define trim (%pi tnum %-> tnum %-> tnum %-> tnum %-> %type) [a] [b] [c] [d] pf (a - b == c - d) %.
%deterministic trim %.
%mode trim %in %in %out %out %.
%define findarr_mult (%pi tnum %-> tnum %-> tnum %-> tnum %-> %type) [a] [b] [c] [m] pf (a == b * c and m == m) %.
%deterministic findarr_mult %.
%mode findarr_mult %in %out %out %in %.
%define rearrange (%pi tnum %-> tnum %-> tnum %-> tnum %-> %type) [a] [b] [c] [d] pf (a - b == c - d) %.
%deterministic rearrange %.
%mode rearrange %in %in %in %in %.

Main solver interface

%define algebra_solver (%pi tform %-> %type) [a] pf a %.
%deterministic algebra_solver %.
%define algebra_fact (%pi tform %-> %type) [a] pf a %.
%mode algebra_fact %out %.
%define atom_replace (%pi tnum %-> tnum %-> %type) [a] [b] pf (a == b) %.
%mode atom_replace %out %out %.
%define algebra_times_hint_intern (%pi tnum %-> tnum %-> %type) [a] [b] pf (a + b == a + b) %.
%mode algebra_times_hint_intern %out %out %.
%define algebra_times_hint (%pi tnum %-> %type) [a] pf (a == a) %.
%mode algebra_times_hint %out %.

Implementation

Normalization

Listify

Decomposes equations into list form 0 + (1 * A * B * C) + D - E + (1 * F * G) +...

%clause listify_imp (%pi (listify A Pos Neg) %<- (plusify (zero + A) Pos Neg)) [p1 pf (zero + A == Pos - Neg)] trans3 (symm plus_zero) comm_plus p1 %.

Timesify

timesify B X S Z - Creates a one-terminated list (1 * A * B * C * ...)

• B - the input
• X - the output list
• Y - signals a special condition
  • zero if a zero is encountered and the term is equal to zero
  • (P + Q) if a sum is encountered and the product needs to be distributed
  • one if the list is successfully processed
• Sign - takes on all change-of-sign information

%clause timesify_neg (%pi (timesify (B * (neg C)) X Y (neg Sign)) %<- (timesify (B * C) X Y Sign)) [p1 pf (B * C * Sign == X * Y)] trans4 times_assoc (times_cong2 neg_times) (symm times_assoc) p1 %.
%clause timesify_swap (%pi (timesify (B * (C * D)) X Y Sign) %<- (timesify (B * C * D) X Y Sign)) [p1] trans (times_cong1 (symm times_assoc)) p1 %.
%clause timesify_zero (timesify (B * zero) one zero one) trans3 times_one times_zero (symm times_zero) %.
%clause timesify_remove (%pi (timesify (B * one) X Y Sign) %<- (timesify B X Y Sign)) [p1 pf (B * Sign == X * Y)] cut (trans3 times_assoc (times_cong2 comm_times) assoc_times) ([p2 pf (B * one * Sign == B * Sign * one)] trans3 p2 times_one p1) %.
%clause timesify_end_plus (timesify (B * (P + Q)) B (P + Q) one) times_one %.
%clause timesify_step (%pi (timesify (B * C) (X * C) Y Sign) %<- (timesify B X Y Sign)) [p1 pf (B * Sign == X * Y)] trans3 (trans3 times_assoc (times_cong2 comm_times) assoc_times) (times_cong1 p1) (trans3 times_assoc (times_cong2 comm_times) assoc_times) %.
%clause timesify_end_one (timesify one one one one) refl %.

Catchtimes

catchtimes A B X Y Sign Pos Neg - unravels to the correct sign

• A - The as-yet unprocessed bit of the equation
• B - The single term that was passed to timesify
• X - The list returned from timesify
• Y - The signal variable from timesify
• Sign - the correct sign
• Pos - The master positive term list
• Neg - The master negative term list

%clause catch_neg1 (
  %pi (catchtimes A B (neg X) Y (neg Sign) Pos Neg)
  %<- (catchtimes A B X Y Sign Pos Neg)) [p1 pf (B * Sign == X * Y imp A + B == Pos - Neg)] imp_i ([p2 pf (B * neg Sign == neg X * Y)] cut (trans3 (symm neg_times2) p2 neg_times1) ([p3 pf (neg (B * Sign) == neg (X * Y))] imp_e p1 (neg_elim p3))) %.
%clause catch_neg2 (
  %pi (catchtimes A B X Y (neg Sign) Pos Neg)
  %<- (catchtimes A B (neg X) Y Sign Pos Neg)) [p1 pf (B * Sign == neg X * Y imp A + B == Pos - Neg)] imp_i ([p2 pf (B * neg Sign == X * Y)] cut (trans3 (symm neg_neg_e) (neg_cong (trans (symm neg_times2) p2)) (symm neg_times1)) ([p3 pf (B * Sign == neg X * Y)] imp_e p1 p3)) %.
%clause catch_zero (%pi (catchtimes A B X zero one Pos Neg) %<- (plusify A Pos Neg)) [p1 pf (A == Pos - Neg)] imp_i ([p2 pf (B * one == X * zero)] cut (trans3 (symm times_one) p2 times_zero) ([p3 pf (B == zero)] trans3 (plus_cong2 p3) plus_zero p1)) %.
%clause catch_neg_one (%pi (catchtimes A B (neg X) one one Pos (Neg + X)) %<- (plusify A Pos Neg)) [p1 pf (A == Pos - Neg)] imp_i ([p2 pf (B * one == neg X * one)] cut (trans3 (symm times_one) p2 times_one) ([p3 pf (B == neg X)] cut (trans (plus_cong p1 p3) plus_assoc) ([p4 pf (A + B == Pos + (neg Neg - X))] trans p4 (plus_cong2 neg_plus)))) %.
%clause catch_one (%pi (catchtimes A B X one one (Pos + X) Neg) %<- (plusify A Pos Neg)) [p1 pf (A == Pos - Neg)] imp_i ([p2 pf (B * one == X * one)] cut (trans3 (symm times_one) p2 times_one) ([p3 pf (B == X)] trans4 (plus_cong p1 p3) plus_assoc (plus_cong2 comm_plus) assoc_plus)) %.
%clause catch_break (
  %pi (catchtimes A B X (P + Q) one Pos Neg)
  %<- (plusify (A + X * P + X * Q) Pos Neg)) [p1 pf (A + X * P + X * Q == Pos - Neg)] imp_i ([p2 pf (B * one == X * (P + Q))] cut (trans3 (symm times_one) p2 distrib) ([p3 pf (B == X * P + X * Q)] trans3 (plus_cong2 p3) assoc_plus p1)) %.

Plusify

plusify - Creates a zero-termiated list (0 + A + B + C +…)

%clause plusify_minus (%pi (plusify (A - (B + C)) Pos Neg) %<- (plusify (A - B - C) Pos Neg)) [p1] trans3 (plus_cong2 (symm neg_plus)) assoc_plus p1 %.
%clause plusify_swap (%pi (plusify (A + (B + C)) Pos Neg) %<- (plusify (A + B + C) Pos Neg)) [p1] trans assoc_plus p1 %.
%clause plusify_neg_one (%pi (plusify (A + neg one * B) Pos Neg) %<- (plusify (A - B) Pos Neg)) [p1] trans (plus_cong2 (trans neg_times1 (neg_cong one_times))) p1 %.
%clause plusify_neg_one' (%pi (plusify (A + B * (neg one)) Pos Neg) %<- (plusify (A - B) Pos Neg)) [p1] trans (plus_cong2 comm_times) (plusify_neg_one p1) %.
%clause plusify_neg (%pi (plusify (A - (neg B)) Pos Neg) %<- (plusify (A + B) Pos Neg)) [p1] trans (plus_cong2 neg_neg_e) p1 %.
%clause plusify_remove_neg (%pi (plusify (A - zero) Pos Neg) %<- (plusify A Pos Neg)) [p1] trans3 (plus_cong2 neg_zero) plus_zero p1 %.
%clause plusify_remove (%pi (plusify (A + zero) Pos Neg) %<- (plusify A Pos Neg)) [p1] trans plus_zero p1 %.
%clause plusify_step_mult_neg (
  %pi (plusify (A - (B * C)) Pos Neg)
  %<- (timesify (one * B * neg C) X Y Sign)
  %<- (catchtimes A (B * neg C) X Y Sign Pos Neg)) [p1 pf (B * neg C * Sign == X * Y imp A + B * neg C == Pos - Neg)] [p2 pf (one * B * neg C * Sign == X * Y)] cut (trans5 times_assoc (symm one_times) assoc_times assoc_times p2) ([p3 pf (B * neg C * Sign == X * Y)] cut (imp_e p1 p3) ([p4 pf (A + B * neg C == Pos - Neg)] trans (plus_cong2 (symm neg_times2)) p4)) %.
%clause plusify_step_mult (
  %pi (plusify (A + (B * C)) Pos Neg)
  %<- (timesify (one * B * C) X Y Sign)
  %<- (catchtimes A (B * C) X Y Sign Pos Neg)) [p1 pf (B * C * Sign == X * Y imp A + B * C == Pos - Neg)] [p2 pf (one * B * C * Sign == X * Y)] cut (trans5 times_assoc (symm one_times) assoc_times assoc_times p2) ([p3 pf (B * C * Sign == X * Y)] imp_e p1 p3) %.
%clause plusify_step_neg_one (%pi (plusify (A - one) Pos (Neg + one)) %<- (plusify A Pos Neg)) [p1 pf (A == Pos - Neg)] trans3 (plus_cong1 p1) plus_assoc (plus_cong2 neg_plus) %.
%clause plusify_step_one (%pi (plusify (A + one) (Pos + one) Neg) %<- (plusify A Pos Neg)) [p1 pf (A == Pos - Neg)] trans4 (plus_cong1 p1) plus_assoc (plus_cong2 comm_plus) assoc_plus %.
%clause plusify_step_neg (%pi (plusify (A - B) Pos (Neg + (one * B))) %<- (plusify A Pos Neg)) [p1 pf (A == Pos - Neg)] trans3 (plus_cong p1 (neg_cong (symm one_times))) plus_assoc (plus_cong2 neg_plus) %.
%clause plusify_step (%pi (plusify (A + B) (Pos + (one * B)) Neg) %<- (plusify A Pos Neg)) [p1 pf (A == Pos - Neg)] trans (plus_cong p1 (symm one_times)) (trans3 plus_assoc (plus_cong2 comm_plus) assoc_plus) %.
%clause plusify_zero (plusify zero zero zero) symm plus_inv %.

Testing

%solve __P : {a} {b} listify (a * (b - one)) _ _ %.
%solve __P : {a} listify (succ a * pred a) _ _ %.
%solve __P : {a} listify (pred (a * a) + (a - a)) _ _ %.
%solve __P : listify zero _ _ %.
%solve __P : {a} {b} {m} {n} {q} listify (a * one + (a * m + n * b) * q) _ _ %.
%solve __P : {a} {b} {m} {n} {q} listify (a + q * a * m + q * n * b) _ _ %.
%solve __P : {a} {b} listify (zero + (a + b)) _ _ %.
%solve __P : {a} {b} {c} {d} {e} listify (c + (d + e) + (a + b)) _ _ %.
% (zero + c + d + e + a + b).
%solve __P : {a} {b} {d} listify (a * (succ one) + (b * (succ d) + d) * a) _ _ %.
%solve __P : listify (one * (one + one) + (one * (one + one) + one) * one) _ _ %.
%solve __P : {a} {b} listify (a * b) _ _ %.
%solve __P : {a} {b} {c} listify (a + c * (c * c) * one + b * (b * b) * zero) _ _ %.
%solve __P : {a} listify (neg (one * neg a)) _ _ %.
%solve __P : {a} {b} {c} listify (zero - (a + neg b * c) + a * neg b) _ _ %.
%solve __P : {a} {b} {c} listify (zero - (a + b * neg c) + a * neg b) _ _ %.
%solve __P : {a} listify (one * (neg a)) _ _ %.
%solve __P : {a} {b} {c} timesify (one * (neg a * neg (b * neg c))) _ _ _ %.
%solve __P : {a} {b} listify (neg a * neg b) _ _ %.
%solve __P : listify (neg one * neg one * neg one * neg one) _ _ %.
%solve __P : {a} listify a _ _ %.
%solve __P : listify (neg (neg (neg (neg (neg (neg zero))))) * one + zero) _ _ %.
%solve __P : {a} {b} timesify (one * (a + b)) _ _ _ %.
%solve __P : {a} listify (pred a * succ a) _ _ %.

Matching

Trim

TRIM - takes two lists, and makes a single pass at removing items from the first list and putting them in the second list. Fails unless at least one element (the top element in the first list) is trimmed.

%clause trim_get (trim (A + C) (B + C) A B) cut (trans plus_assoc (plus_cong2 (plus_cong2 (symm neg_plus)))) ([p2 pf (A + C - (B + C) == A + (C + (neg B - C)))] cut (trans (plus_cong2 assoc_plus) (plus_cong2 cancel_a+b-a)) ([p3 pf (A + (C + (neg B - C)) == A - B)] trans p2 p3)) %.
%clause trim_getmult (%pi (trim (A + C) (B + D) A B) %<- (findarr_mult C D one nomatch)) [p2 pf (C == D * one and zero == zero)] cut (trans (and_e1 p2) times_one) ([p3 pf (C == D)] cut (congr ([i] C - B - i == neg B) (symm p3) cancel_a+b-a) ([p4 pf (C - B - D == neg B)] cut (trans3 (plus_cong2 (symm neg_plus)) assoc_plus p4) ([p5 pf (C - (B + D) == neg B)] trans plus_assoc (plus_cong2 p5)))) %.
%clause trim_step1 (%pi (trim (A + C) B (X + C) Y) %<- (trim A B X Y)) [p1 pf (A - B == X - Y)] cut (trans3 (trans3 plus_assoc (plus_cong2 comm_plus) assoc_plus) (plus_cong1 p1) (trans3 plus_assoc (plus_cong2 comm_plus) assoc_plus)) ([p2 pf (A + C - B == X + C - Y)] p2) %.
%clause trim_step2 (%pi (trim A (B + C) X (Y + C)) %<- (trim A B X Y)) [p1 pf (A - B == X - Y)] trans3 (plus_cong2 (symm neg_plus)) (trans3 assoc_plus (plus_cong1 p1) plus_assoc) (plus_cong2 neg_plus) %.

Findarr_mult

% FINDARR_MULT - more complex than trim, cycles through a product to
% Uses a quadratic algorithm, but in most cases the length of the proof
% is dominated by the list creation, not the
%clause fam_neg (%pi (findarr_mult (neg X) (neg Y) Z M) %<- (findarr_mult X Y Z M)) [p1 pf (X == Y * Z and M == M)] and_i (trans (neg_cong (and_e1 p1)) (symm neg_times1)) refl %.
%clause fam_step (%pi (findarr_mult (X * B) (Y * B) Z M) %<- (findarr_mult X Y Z match)) [p1 pf (X == Y * Z and match == match)] cut (trans (times_cong1 (and_e1 p1)) (trans3 times_assoc (times_cong2 comm_times) assoc_times)) ([p2 pf (X * B == Y * B * Z)] and_i p2 refl) %.
%clause fam_step2 (
  %pi (findarr_mult (X * B) (Y * C) Z M)
  %<- (atom_replace B C)
  %<- (findarr_mult X Y Z match)) [p1] [p2] congr ([i] X * B == Y * i * Z and M == M) (symm p2) (fam_step p1) %.
%clause fam_step2' (
  %pi (findarr_mult (X * B) (Y * C) Z M)
  %<- (atom_replace C B)
  %<- (findarr_mult X Y Z match)) [p1] [p2] congr ([i] X * B == Y * i * Z and M == M) p2 (fam_step p1) %.
%clause fam_swap (%pi (findarr_mult X (Y * B) Z M) %<- (findarr_mult X Y (Z * B) M)) [p1 pf (X == Y * (Z * B) and M == M)] cut p1 ([_] and_i (trans3 (and_e1 p1) (times_cong2 comm_times) (symm times_assoc)) refl) %.
%clause fam_finish (findarr_mult one one one M) and_i (symm times_one) refl %.
%clause fam_one (%pi (findarr_mult X one Y match) %<- (findarr_mult X Y one nomatch)) [p1 pf (X == Y * one and nomatch == nomatch)] and_i (trans (and_e1 p1) comm_times) refl %.

Rearrange

% REARRANGE
% Handles the finishing steps of the solver
%clause rearr_finish (rearrange zero zero zero zero) refl %.
%clause rearr_end (%pi (rearrange A B zero zero) %<- (trim A B X Y) %<- (rearrange X Y zero zero)) [p1 pf (X - Y == zero - zero)] [p2 pf (A - B == X - Y)] trans p2 p1 %.
%clause rearr_right (%pi (rearrange zero zero C D) %<- (trim C D X Y) %<- (rearrange X Y zero zero)) [p1] [p2] symm (rearr_end p1 p2) %.
%clause rearr_pos (%pi (rearrange A zero C zero) %<- (trim A C X Y) %<- (rearrange X Y zero zero)) [p1 pf (X - Y == zero - zero)] [p2 pf (A - C == X - Y)] cut (trans3 p2 p1 plus_inv) ([p3 pf (A - C == zero)] cut (trans3 (symm cancel_a-b+b) (plus_cong1 p3) zero_plus) ([p4 pf (A == C)] plus_cong1 p4)) %.
%clause rearr_neg (%pi (rearrange zero B zero D) %<- (trim B D X Y) %<- (rearrange X Y zero zero)) [p1 pf (X - Y == zero - zero)] [p2 pf (B - D == X - Y)] cut (trans3 p2 p1 plus_inv) ([p3 pf (B - D == zero)] cut (trans3 (symm cancel_a-b+b) (plus_cong1 p3) zero_plus) ([p4 pf (B == D)] plus_cong2 (neg_cong p4))) %.
%define plus_swap (%pi (pf (A - B == C - D)) %-> (pf (A - C == B - D))) [p1] cut (trans3 (symm cancel_a-b+b) (plus_cong1 p1) comm_plus) ([p2 pf (A == B + (C - D))] cut (trans3 (plus_cong1 p2) plus_assoc (plus_cong2 cancel_a+b-a)) ([p3 pf (A - C == B - D)] p3)) %.
%define plus_swap2 (%pi (pf (A + B == C + D)) %-> (pf (A - D == C - B))) [p1] cut (trans5 (symm cancel_a+b-b) (plus_cong1 p1) plus_assoc (plus_cong2 comm_plus) assoc_plus) ([p2 pf (A == C - B + D)] trans (plus_cong1 p2) cancel_a+b-b) %.
%clause rearr_one (
  %pi (rearrange A B C zero)
  %<- (trim A C X Y)
  %<- (trim X B Z W)
  %<- (rearrange Z W Y zero)) [p1 pf (Z - W == Y - zero)] [p2 pf (X - B == Z - W)] [p3 pf (A - C == X - Y)] cut (plus_swap (trans p2 p1)) ([p4 pf (X - Y == B - zero)] plus_swap (trans p3 p4)) %.
%clause rearr_two (
  %pi (rearrange A B zero D)
  %<- (trim B D X Y)
  %<- (trim A X Z W)
  %<- (rearrange Z W zero Y)) [p1 pf (Z - W == zero - Y)] [p2 pf (A - X == Z - W)] [p3 pf (B - D == X - Y)] cut (plus_swap (trans p2 p1)) ([p4 pf (A - zero == X - Y)] plus_swap (trans p4 (symm p3))) %.
%clause rearr_three (
  %pi (rearrange C zero A B)
  %<- (trim A C X Y)
  %<- (trim X B Z W)
  %<- (rearrange Z W Y zero)) [p1] [p2] [p3] symm (rearr_one p1 p2 p3) %.
%clause rearr_four (
  %pi (rearrange zero D A B)
  %<- (trim B D X Y)
  %<- (trim A X Z W)
  %<- (rearrange Z W zero Y)) [p1] [p2] [p3] symm (rearr_two p1 p2 p3) %.
%clause rearr_any1 (%pi (rearrange A B C D) %<- (trim A B X Y) %<- (rearrange X C Y D)) [p1 pf (X - C == Y - D)] [p2 pf (A - B == X - Y)] trans p2 (plus_swap p1) %.
%clause rearr_any2 (%pi (rearrange A B C D) %<- (trim A C X Y) %<- (rearrange X B Y D)) [p1 pf (X - B == Y - D)] [p2 pf (A - C == X - Y)] plus_swap (trans p2 (plus_swap p1)) %.
%clause solver_short1 (algebra_solver (A == A)) refl %.
%clause solver_short2a (%pi (algebra_solver (A + B == A + C)) %<- (algebra_solver (B == C))) plus_cong2 %.
%clause solver_short2b (%pi (algebra_solver (A + B == C + B)) %<- (algebra_solver (A == C))) plus_cong1 %.
%clause solver_rearrange (
  %pi (algebra_solver (A == B))
  %<- (listify A Pos Neg)
  %<- (listify B Pos' Neg')
  %<- (rearrange Pos Neg Pos' Neg')) [p1] [p2] [p3] trans3 p3 p1 (symm p2) %.
%clause fact_one_gt (algebra_fact (one > zero)) one>zero %.
%clause fact_gt->geq (%pi (algebra_fact (A >= B)) %<- (algebra_fact (A > B))) gt->geq %.
%clause fact_gt->neq (%pi (algebra_fact (A != B)) %<- (algebra_fact (A > B))) gt->neq %.
%clause fact_lt->neq (%pi (algebra_fact (A != B)) %<- (algebra_fact (A < B))) lt->neq %.
%clause fact_eq->geq (%pi (algebra_fact (A >= B)) %<- (algebra_fact (A == B))) eq->geq %.
%clause fact_eq->leq (%pi (algebra_fact (A <= B)) %<- (algebra_fact (A == B))) eq->leq %.
%clause hintmod1 (
  %pi (algebra_times_hint_intern A B)
  %<- (algebra_times_hint A)
  %<- (algebra_times_hint B)) [p1] [p2] cut2 p1 p2 ([_] [_] refl) %.
%clause hintmod2 (%pi (algebra_times_hint_intern A one) %<- (algebra_times_hint A)) [p1] cut p1 ([_] refl) %.
%clause hintmod3 (%pi (algebra_times_hint_intern one A) %<- (algebra_times_hint A)) [p1] cut p1 ([_] refl) %.
%define eq_arrange (%pi (pf (A - B == C - D)) %-> (pf (A == B)) %-> (pf (C == D))) [p1 pf (A - B == C - D)] [p2 pf (A == B)] cut (trans3 (symm p1) (plus_cong1 p2) plus_inv) ([p3 pf (C - D == zero)] trans3 (symm cancel_a-b+b) (plus_cong1 p3) zero_plus) %.
%clause solver_eq (%pi (algebra_solver (A == B imp C == D)) %<- (algebra_solver (A + D == C + B))) [p1] imp_i ([p2] eq_arrange (plus_swap2 p1) p2) %.
%clause solver_eq_times (
  %pi (algebra_solver (A == B imp C == D))
  %<- (algebra_times_hint_intern X Y)
  %<- (algebra_fact (Y != zero))
  %<- (algebra_solver (A * X + D * Y == C * Y + B * X))) [p1] [p2] [p3] cut p3 ([_] imp_i ([p4] cut (imp_e (solver_eq p1) (times_cong1 p4)) ([p5 pf (C * Y == D * Y)] times_elim2 p2 p5))) %.
%clause solver_eq_neg (%pi (algebra_solver (A == B imp C == D)) %<- (algebra_solver (D + B == C + A))) [p1] imp_i ([p2] eq_arrange (plus_swap2 (trans comm_plus (plus_swap2 p1))) (neg_cong p2)) %.
%clause solver_eq_neg_times (
  %pi (algebra_solver (A == B imp C == D))
  %<- (algebra_times_hint_intern X Y)
  %<- (algebra_fact (Y != zero))
  %<- (algebra_solver (D * Y + B * X == C * Y + A * X))) [p1] [p2] [p3] cut p3 ([_] imp_i ([p4] cut (imp_e (solver_eq_neg p1) (times_cong1 p4)) ([p5 pf (C * Y == D * Y)] times_elim2 p2 p5))) %.
%define geq_arrange (%pi (pf (A + D == C + B)) %-> (pf (A >= B)) %-> (pf (C >= D))) [p0 pf (A + D == C + B)] [p1 pf (A >= B)] cut (plus_swap2 p0) ([p2 pf (A - B == C - D)] cut (trans_geq_eq (geq_plus_cong1 p1) plus_inv) ([p3 pf (A - B >= zero)] cut (trans_eq_geq (symm p2) p3) ([p4 pf (C - D >= zero)] cut (trans_eq_geq (symm cancel_a-b+b) (geq_plus_cong1 p4)) ([p5 pf (C >= zero + D)] trans_geq_eq p5 zero_plus)))) %.
%clause solver_geq (%pi (algebra_solver (A >= B imp C >= D)) %<- (algebra_solver (A + D == C + B))) [p1] imp_i ([p2] geq_arrange p1 p2) %.
%clause solver_geq_times1 (
  %pi (algebra_solver (A >= B imp C >= D))
  %<- (algebra_times_hint_intern X Y)
  %<- (algebra_fact (X >= zero))
  %<- (algebra_fact (Y > zero))
  %<- (algebra_solver (A * X + D * Y == C * Y + B * X))) [p1] [p2] [p3] [p4] cut p4 ([_] imp_i ([p5] cut (imp_e (solver_geq p1) (geq_times_cong1 p3 p5)) ([p6 pf (C * Y >= D * Y)] geq_times_elim2 p2 p6))) %.
%clause solver_geq_times2 (
  %pi (algebra_solver (A <= B imp C >= D))
  %<- (algebra_times_hint_intern X Y)
  %<- (algebra_fact (X <= zero))
  %<- (algebra_fact (Y > zero))
  %<- (algebra_solver (A * X + D * Y == C * Y + B * X))) [p1] [p2] [p3] [p4] cut p4 ([_] imp_i ([p5] cut3 p1 p2 p3 ([_] [_] [_] cut (imp_e (solver_geq p1) (geq_times_cong1_neg p3 p5)) ([p6 pf (C * Y >= D * Y)] geq_times_elim2 p2 p6)))) %.
%clause solver_geq_times3 (
  %pi (algebra_solver (A >= B imp C <= D))
  %<- (algebra_times_hint_intern X Y)
  %<- (algebra_fact (X >= zero))
  %<- (algebra_fact (Y < zero))
  %<- (algebra_solver (A * X + D * Y == C * Y + B * X))) [p1] [p2] [p3] [p4] cut p4 ([_] imp_i ([p5] cut3 p1 p2 p3 ([_] [_] [_] cut (imp_e (solver_geq p1) (geq_times_cong1 p3 p5)) ([p6 pf (C * Y >= D * Y)] geq_times_elim2_neg p2 p6)))) %.
%clause solver_geq_times4 (
  %pi (algebra_solver (A <= B imp C <= D))
  %<- (algebra_times_hint_intern X Y)
  %<- (algebra_fact (X <= zero))
  %<- (algebra_fact (Y < zero))
  %<- (algebra_solver (A * X + D * Y == C * Y + B * X))) [p1] [p2] [p3] [p4] cut p4 ([_] imp_i ([p5] cut3 p1 p2 p3 ([_] [_] [_] cut (imp_e (solver_geq p1) (geq_times_cong1_neg p3 p5)) ([p6 pf (C * Y >= D * Y)] geq_times_elim2_neg p2 p6)))) %.
%clause solver_neq (%pi (algebra_solver (A != B imp C != D)) %<- (algebra_solver (C == D imp A == B))) [p1] imp_i ([p2] not_eie p2 (imp_e p1)) %.
%clause solver_gt (%pi (algebra_solver (A < B imp C < D)) %<- (algebra_solver (C >= D imp A >= B))) [p1] imp_i ([p2] not_ein p2 (imp_e p1)) %.

Test cases for the solver

%solve __P : {a} {b} {c} algebra_solver (a > b imp a + c > c + b) %.
%solve __P : {a} {b} {c} algebra_solver (a - b + c >= zero imp a >= b - c) %.
%solve __P : {a} {b} {c} algebra_solver (a >= b imp neg a + c <= neg b + c) %.
%solve __P : algebra_solver (one - one == zero) %.
%solve __P : algebra_solver (one - one == two - two) %.
%solve __P : {a} algebra_solver (two - two + a == one + a * (one + zero) - one) %.
%solve __P : {a} {b} {c} {d} algebra_solver (a - b == c - d imp a - c == b - d) %.
%solve __P : {a} algebra_solver (succ a * pred a == pred (a * a)) %.
%solve __P : {a} {b} {c} algebra_solver (a - (b - c) == (a - b) + (c * one)) %.
%solve __P : {a} {b} {c} algebra_solver (a + b == c * (one - one) + b + a) %.
%solve __P : {a} {b} {c} {d} {e} algebra_solver (a - b + (c - d) + e == e - d + (neg b + c + a)) %.
%solve __P : {a} {b} {c} algebra_solver (c + (a + b) == a + zero + zero + b + zero + c) %.
%solve __P : {a} {b} algebra_solver (neg (a + b) == (neg a) + (neg b)) %.
%solve __P : {a} {b} {c} algebra_solver (a - (b - c) == (a + c) - b) %.
%solve __P : {a} {b} {c} algebra_solver (neg one * (neg one * a + neg one * (b + c)) == neg (neg one * a) - (neg one * (b + c))) %.
%solve __P : {a} {b} {c} {d} {e} {f} {g} {h} {i} algebra_solver (a * (b + (c * (d + (e * (f + (g * (h + i))))))) == a * (b + (c * (d + (e * (f + (g * h)))))) + a * (c * one * e) * g * i) %.
%solve __P : {a} {b} {c} {d} {e} {f} algebra_solver (a + b + c + d + e + f == f + e + d + c + b + a) %.
%solve __P : {a} {b} algebra_solver (a * b == b * a) %.
%solve __P : {a} {b} {c} {d} algebra_solver (a * (b + c) + (d * (c + a)) == c * d + (a * (b + c + d))) %.
%solve __P : {a} {b} {d} algebra_solver (a * (d * (one + b) + one + b) + a == a * (succ one) + (b * (succ d) + d) * a) %.
%solve __P : {a} {b} {c} algebra_solver (c + b + (a - one) * b == c + a * b + b - b) %.
%solve __P : {a} {b} {m} {n} {q} algebra_solver (a * one + (a * m + n * b) * q == a * (one + m * q) + n * b * q) %.
%solve __P : {a} {b} {m} {n} {q} algebra_solver (a * one + (a * m + n * b) * q == a * one + q * a * m + q * n * b) %.
%solve __P : {a} {b} algebra_solver (a * zero + zero == zero * b) %.
%solve __P : {a} {b} algebra_solver (a * (b * b) + a * zero == a * b * b) %.
%solve __P : {a} {b} {c} algebra_solver (a * one * zero * b + c * (a + b) == b * c + zero * a + c * (a + zero)) %.
%solve __P : algebra_solver (neg zero == zero) %.
%solve __P : {a} {b} algebra_solver (a * (b * b) * one + a * zero == a * b * b) %.
%query 0 _ _ %the ({a} {b} algebra_solver (a == b)) __P %.
%solve __P : {a} {b} {c} algebra_solver (a * b * c == c * b * a) %.
%solve __P : {a} {b} {m} {n} {q} algebra_solver (a - (m * a + n * b) * q == (one - q * m) * a + (neg (q * n)) * b) %.
%solve __P : {a} {b} algebra_solver (a == b imp neg a == neg b) %.
%solve __P : {a} {b} algebra_solver (a > b imp neg a < neg b) %.
%solve __P : {a} {b} algebra_solver (a * one == b imp a == b * one) %.
%solve __P : {a} {b} algebra_solver (a * one >= b imp a >= b * one) %.
%solve __P : {a} {b} algebra_solver (a >= b imp neg b >= neg a) %.
%solve __P : {a} {b} algebra_solver (a != b imp neg a != neg b) %.
%solve __P : {a} {b} {c} algebra_solver (a > b imp c < a + (b - c) * neg one) %.
%solve __P : {a} {b} %pi (algebra_times_hint b) %-> (algebra_solver (a == one imp a * b == b)) %.
%query _ 1 _ %the ({a} {b} algebra_solver (a * b + a == a + b * a)) __P %.
%query 1 _ _ %the ({a} {b} algebra_solver (a * b + a == a + b * a)) __P %.
%solve __P : {a} {b} {c} algebra_solver (a - b == a - b + c - c) %.
%solve __P : {a} {b} {c} algebra_solver (a == b imp a + c == b + c) %.
%solve __P : {a} {b} {c} {d}
  %pi (atom_replace a c)
  %-> (atom_replace d c)
  %-> (algebra_solver (a + b + c + c == b + c + c + d)) %.
%solve __P : {a} {b} {c} %pi (atom_replace b c) %-> (algebra_solver (a + b == c + a)) %.
%solve __P : {a} {b} {c} %pi (atom_replace b c) %-> (algebra_solver (a == b imp a - c == zero)) %.
%solve __P : {a} {b} {c} %pi (atom_replace b c) %-> (algebra_solver (a - b == neg c + a)) %.
%solve __P : {a} {b} {c} %pi (atom_replace b c) %-> (algebra_solver (a - a == b - c)) %.
%solve __P : {a} {b} {c} {d}
  %pi (algebra_times_hint c)
  %-> (algebra_solver (a - b == d imp a * c == c * d + c * b)) %.
%solve __P : {a} {b} {c}
  %pi (algebra_times_hint a)
  %-> (algebra_fact (a != zero))
  %-> (algebra_solver (neg a * c == neg (b * a) imp b - c == zero)) %.
%solve __P : {a} {b} {c} {d}
  %pi (algebra_times_hint (a + d))
  %-> (algebra_fact (a + d != zero))
  %-> (atom_replace b d)
  %-> (algebra_solver (neg a - b * c == neg (d * a) - d * b imp b == c)) %.
%solve __P : {a} {b} {c} {d}
  %pi (algebra_times_hint (a + b * c))
  %-> (algebra_fact (a + b * c > zero))
  %-> (algebra_solver (d > one imp a * (d - one) > b * c * (one - d))) %.
%query 0 _ _ %the ({a} {b} {c} {d} {e}
  %pi (algebra_times_hint (a + e))
  %-> (algebra_fact (a + e > zero))
  %-> (algebra_times_hint b)
  %-> (algebra_solver (c * (a + e) == d * a imp b * c == b * d))) __P %.
%solve __P : {a} {b} {c} {d} {e} {f} {g}
  %pi (algebra_times_hint (a + b * c))
  %-> (algebra_fact (a + b * c > zero))
  %-> (algebra_times_hint d)
  %-> (algebra_solver (a + b * c * (e * f - one) == (g + one) * (a + b * c) imp d * (e * f - one) == d * (g + one))) %.
%solve ex_27 : {a} {b} {c} %pi (algebra_times_hint a) %-> (algebra_solver (a * (b - c) != zero imp b != c)) %.
%solve ex_28 : {a} {b} {c}
  %pi (algebra_times_hint (a + b))
  %-> (algebra_fact (a + b < zero))
  %-> (algebra_solver (a * (c - zero) - b == a - b * c imp zero == one - c)) %.
%solve ex_29 : {a} {b} {c} {d}
  %pi (algebra_times_hint a)
  %-> (algebra_fact (a < zero))
  %-> (algebra_times_hint b)
  %-> (algebra_fact (b >= zero))
  %-> (algebra_solver (c * a >= a * (d + zero) imp b * c * one <= b * d)) %.
%define ex_30 (
  %pi (pf (A < zero))
  %-> (pf (B >= zero))
  %-> (pf (C * A >= A * (D + zero)))
  %-> (pf (B * C * one <= B * D))) [p1] [p2] [p3] imp_e (ex_29 A B C D refl p1 refl p2) p3 %.