%{ 
The big algebraic software is a [[tactical theorem proving|tactical theorem prover]] written as a Twelf [[logic program]] by [[User:Rsimmons|Rob]] at Princeton University as part of the Foundational Proof Carrying Code system. 
}%

%{ == 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. }%

tnum : type.
tform : type.
pf : tform -> type.
imp : tform -> tform -> tform.           %infix right 10 imp.
and : tform -> tform -> tform.           %infix right 12 and.
== : tnum -> tnum -> tform.              %infix none 18 ==.
>= : tnum -> tnum -> tform.              %infix none 18 >=.
< : tnum -> tnum -> tform.         %infix none 18 <.
!= : tnum -> tnum -> tform.        %infix none 18 !=.
> : tnum -> tnum -> tform = [x][y] y < x.         %infix none 18 >.
<= : tnum -> tnum -> tform = [x][y] y >= x.       %infix none 18 <=.


imp_i : (pf A -> pf B) -> pf (A imp B).
imp_e : pf (A imp B) -> pf A -> pf B.
and_i : pf A -> pf B -> pf (A and B).
and_e1 : pf (A and B) -> pf A.
and_e2 : pf (A and B) -> pf B.
cut : pf A -> (pf A -> pf B) -> pf B.
cut2 : pf A -> pf A' -> (pf A -> pf A' -> pf B) -> pf B.
cut3 : pf A -> pf A' -> pf A'' -> (pf A -> pf A' -> pf A'' -> pf B) -> pf B.
congr : {h: tnum -> tform} pf (A == B) -> pf (h B) -> pf (h A).
gt->geq : pf (A > B) -> pf (A >= B).
gt->neq : pf (A > B) -> pf (A != B).
lt->neq : pf (A < B) -> pf (A != B).
eq->geq : pf (A == B) -> pf (A >= B).
eq->leq : pf (A == B) -> pf (A <= B).
not_eie : pf (A != B) -> (pf (C == D) -> pf (A == B)) -> pf (C != D).
not_ein : pf (A < B) -> (pf (C >= D) -> pf (A >= B)) -> pf (C < D).


zero : tnum.
one : tnum.
one>zero : pf (one > zero).
+ : tnum -> tnum -> tnum.                %infix left 22 +.
*  : tnum -> tnum -> tnum.               %infix left 23 *.
neg : tnum -> tnum.
- = [a][b] a + neg b.                    %infix left 22 -.
succ = [x] x + one.
pred = [x] x - one.
two = succ one.


refl : pf (A == A).
symm : pf (A == B) -> pf (B == A).
trans : pf (A == B) -> pf (B == C) -> pf (A == C).
trans3 : pf (A == B) -> pf (B == C) -> pf (C == D) -> pf (A == D).
trans4 : pf (A == B) -> pf (B == C) -> pf (C == D) -> pf (D == E) -> pf (A == E).
trans5 : pf (A == B) -> pf (B == C) -> pf (C == D) -> pf (D == E) -> pf (E == F) -> pf (A == F).
trans_geq_eq : pf (A >= B) -> pf (B == C) -> pf (A >= C).
trans_eq_geq : pf (A == B) -> pf (B >= C) -> pf (A >= C).

comm_plus : pf (A + B == B + A).
plus_zero : pf (A + zero == A).
zero_plus : pf (zero + A == A).
plus_cong : pf (A == B) -> pf (C == D) -> pf (A + C == B + D).
plus_cong2 : pf (A == B) -> pf (C + A == C + B) = [p1] plus_cong refl p1.
plus_cong1 : pf (A == B) -> pf (A + C == B + C) = [p1] plus_cong p1 refl.
plus_assoc : pf (A + B + C == A + (B + C)).
assoc_plus : pf (A + (B + C) == A + B + C) = symm plus_assoc.
neg_plus : pf (neg A + neg B == neg (A + B)).
plus_inv   : pf (A - A == zero).
inv_plus   : pf (neg A + A == zero) = trans comm_plus plus_inv.
geq_plus_cong1 : pf (A >= B) -> pf (A + C >= B + C).

comm_times : pf (A * B == B * A).
times_assoc : pf (A * B * C == A * (B * C)).
assoc_times : pf (A * (B * C) == A * B * C) = symm times_assoc.
times_assoc : pf (A * B * C == A * (B * C)).
times_cong : pf (A == B) -> pf (C == D) -> pf (A * C == B * D).
times_cong2 : pf (A == B) -> pf (C * A == C * B) = [p1] times_cong refl p1.
times_cong1 : pf (A == B) -> pf (A * C == B * C) = [p1] times_cong p1 refl.
neg_times1 : pf (neg A * B == neg (A * B)).
neg_times2 : pf (A * neg B == neg (A * B)).
neg_times : pf (neg A * neg B == A * B).
times_one  : pf (A * one == A).
one_times  : pf (one * A == A) = trans comm_times times_one.
times_zero : pf (A * zero == zero).
times_elim2 : pf (A != zero) -> pf (B * A == C * A) -> pf (B == C).
geq_times_cong1 : pf (A >= zero) -> pf (B >= C) -> pf (B * A >= C * A).
geq_times_elim1 : pf (A > zero) -> pf (A * B >= A * C) -> pf (B >= C).
geq_times_elim2 : pf (A > zero) -> pf (B * A >= C * A) -> pf (B >= C).
geq_times_cong1_neg : pf (A <= zero) -> pf (B >= C) -> pf (B * A <= C * A).
geq_times_elim2_neg : pf (A < zero) -> pf (B * A >= C * A) -> pf (B <= C).

neg_cong : pf (A == B) -> pf (neg A == neg B).
neg_elim : pf (neg A == neg B) -> pf (A == B).
neg_neg_e : pf (neg (neg A) == A).
neg_zero : pf (neg zero == zero).

distrib : pf (A * (B + C) == A * B + A * C).
distrib_right : pf ((A + B) * C == A * C + B * C).

cancel_a+b-b : pf (A + B - B == A) = symm
  (trans3 (symm plus_zero) (plus_cong2 (symm plus_inv)) assoc_plus).
cancel_a+b-b' : pf (A + (B - B) == A) = 
  trans assoc_plus cancel_a+b-b.

cancel_a-b+b : pf (A - B + B == A) = symm
  (trans4 (symm cancel_a+b-b) plus_assoc (plus_cong2 comm_plus) assoc_plus).
cancel_a-b+b' : pf (A + (neg B + B) == A) = 
  trans assoc_plus cancel_a-b+b.

cancel_a+b-a : pf (A + B - A == B) =
  symm (trans3 (symm cancel_a-b+b) comm_plus assoc_plus).
cancel_a+b-a' : pf (A + (B - A) == B) = 
  trans assoc_plus cancel_a+b-a.

cancel_a-a+b : pf (A - A + B == B) = 
  trans3 comm_plus assoc_plus cancel_a+b-b.
cancel_a-a+b' : pf (A + (neg A + B) == B) =
  trans assoc_plus cancel_a-a+b.

cancel_-a+a+b : pf (neg A + A + B == B) = 
  trans (plus_cong1 comm_plus) cancel_a-a+b.
cancel_-a+a+b' : pf (neg A + (A + B) == B) = 
  trans assoc_plus cancel_-a+a+b.

cancel_-a+b+a : pf (neg A + B + A == B) =
  trans4 plus_assoc (plus_cong2 comm_plus) assoc_plus cancel_-a+a+b.
cancel_-a+b+a' : pf (neg A + (B + A) == B) = 
  trans assoc_plus cancel_-a+b+a.


%{ == Parts of the solver == }%

nomatch = zero.
match = one.

listify  : tnum -> tnum -> tnum -> type = [a][pos][neg] pf (a == pos - neg).
%deterministic listify.
%mode listify +A -Pos -Neg.

%{ === Normalization === }%

plusify  : tnum -> tnum -> tnum -> type = 
  [a][x][y] pf (a == x - y).
%deterministic plusify.
%mode plusify +A -X -Y.

timesify : tnum -> tnum -> tnum -> tnum -> type =
  [b][x][y][sign] pf (b * sign == x * y). 
%deterministic timesify.
%mode timesify +B -X -Y -Sign.

catchtimes : 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 +A +B +X +Y +Sign -Pos -Neg.

%{ === Matching === }%

trim : tnum -> tnum -> tnum -> tnum -> type
  = [a][b][c][d] pf (a - b == c - d).
%deterministic trim.
%mode trim +A +B -X -Y.

findarr_mult : tnum -> tnum -> tnum -> tnum -> type
  = [a][b][c][m] pf (a == b * c and m == m).
%deterministic findarr_mult.
%mode findarr_mult +A -B -Z +M.

rearrange : tnum -> tnum -> tnum -> tnum -> type 
  = [a][b][c][d] pf (a - b == c - d).
%deterministic rearrange.
%mode rearrange +A +B +C +D.

%{ === Main solver interface === }%

algebra_solver : tform -> type = [a] pf a.
%deterministic algebra_solver.

algebra_fact : tform -> type = [a] pf a.
%mode algebra_fact -Fact.

atom_replace : tnum -> tnum -> type = [a][b] pf (a == b).
%mode atom_replace -A -B.

algebra_times_hint_intern : tnum -> tnum -> type = [a][b] pf (a + b == a + b).
%mode algebra_times_hint_intern -Predicate -Conclusion.

algebra_times_hint : tnum -> type = [a] pf (a == a).
%mode algebra_times_hint -Hint.


%{ == Implementation == }%

%{ === Normalization === }%

%{ ==== Listify ==== }%

%{ Decomposes equations into list form <tt>0 + (1 * A * B * C) + D - E + (1 * F * G) +...</tt> }%

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





%{ ==== Timesify ==== }%

%{ <tt>timesify B X S Z</tt> - Creates a one-terminated list <tt>(1 * A * B * C * ...)</tt>

* 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 : 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 : 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 : 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 : 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 ==== }%
%{ <tt>catchtimes A B X Y Sign Pos Neg</tt> - 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: 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 : 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 : 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 : 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 : 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 : 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 ==== }%
%{ <tt>plusify</tt> - Creates a zero-termiated list (0 + A + B + C +...)  }%

%clause
plusify_minus : 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 : plusify (A + (B + C)) Pos Neg 
                 <- plusify (A + B + C) Pos Neg =
  [p1] trans assoc_plus p1.

%clause
plusify_neg_one : 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' : 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 : plusify (A - (neg B)) Pos Neg <- plusify (A + B) Pos Neg =
  [p1] trans (plus_cong2 neg_neg_e) p1.

%clause
plusify_remove_neg : plusify (A - zero) Pos Neg 
                     <- plusify A Pos Neg = 
  [p1] trans3 (plus_cong2 neg_zero) plus_zero p1.

%clause
plusify_remove : plusify (A + zero) Pos Neg <- plusify A Pos Neg = 
  [p1] trans plus_zero p1.

%clause
plusify_step_mult_neg : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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' : 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 : 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 : 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 : 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 : 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 : 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 : 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).

plus_swap : 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.

plus_swap2 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : algebra_solver (A + B == A + C)  
                   <- algebra_solver (B == C) = plus_cong2.

%clause
solver_short2b : algebra_solver (A + B == C + B)
                   <- algebra_solver (A == C) = plus_cong1.

%clause
solver_rearrange : 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 : algebra_fact (A >= B) <- algebra_fact (A > B) = gt->geq.

%clause
fact_gt->neq : algebra_fact (A != B) <- algebra_fact (A > B) = gt->neq.

%clause
fact_lt->neq : algebra_fact (A != B) <- algebra_fact (A < B) = lt->neq.

%clause
fact_eq->geq : algebra_fact (A >= B) <- algebra_fact (A == B) = eq->geq.

%clause
fact_eq->leq : algebra_fact (A <= B) <- algebra_fact (A == B) = eq->leq.

%clause
hintmod1 : algebra_times_hint_intern A B 
             <- algebra_times_hint A
             <- algebra_times_hint B = [p1][p2] cut2 p1 p2 [_][_] refl.

%clause
hintmod2 : algebra_times_hint_intern A one <- algebra_times_hint A = 
  [p1] cut p1 [_] refl.

%clause
hintmod3 : algebra_times_hint_intern one A <- algebra_times_hint A = 
  [p1] cut p1 [_] refl.

eq_arrange : 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 : 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 : 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 : 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 : 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.  

geq_arrange : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 * __P : {a}{b} algebra_solver (a == b). 
%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} algebra_times_hint b -> algebra_solver (a  == one imp a * b == b ).


%query * 1 __P : {a}{b} algebra_solver (a * b + a == a + b * a). 
%query 1 * __P : {a}{b} algebra_solver (a * b + a == a + b * a). 

%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} atom_replace a c -> atom_replace d c -> 
   algebra_solver (a + b + c + c == b + c + c + d).

%solve __P : {a}{b}{c} atom_replace b c ->
     algebra_solver (a + b == c + a).

%solve __P : {a}{b}{c} atom_replace b c 
    -> algebra_solver (a == b imp a - c == zero).
%solve __P : {a}{b}{c} atom_replace b c -> 
   algebra_solver (a - b == neg c + a).

%solve __P : {a}{b}{c} atom_replace b c -> 
    algebra_solver (a - a == b - c). 

%solve __P : {a}{b}{c}{d} algebra_times_hint c
               -> algebra_solver (a - b == d imp a * c == c * d + c * b).

%solve __P : {a}{b}{c} 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} 
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} 
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 * __P : {a}{b}{c}{d}{e}
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).

%solve __P : {a}{b}{c}{d}{e}{f}{g}
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} algebra_times_hint a
-> algebra_solver (a * (b - c) != zero imp b != c).

%solve ex_28 : {a}{b}{c} 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} 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 ).

ex_30 : 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.