Automatically Generated Texts from Nuprl Proofs
The following proof texts were automatically generated by the methods described in the paper Verbalization of HighLevel Formal Proofs. Amanda M. HollandMinkley, Regina Barzilay, and Robert Constable. Sixteenth National Conference on Artificial Intelligence (to appear). A simple tutorial on reading Nuprl proofs and a guide to some of the tactics appeared as part of our corpuscollecting study and can still be seen there.
Automatically Generated Proof Text  Nuprl lemmas and definitions  Formal Nuprl Proof (opens in own window)  
Theorem: For integer a and b and natural number
c, (a  b)  c = a  (b  c). Consider that a and b are integers and c is a natural number. Now, the original expression can be transformed to imax(imax(ab;0)c;0) = imax(a(b+c);0). From the add_com lemma, we conclude imax(c + imax(a + b;0);0) = imax(a + b + c;0). From the imax_assoc lemma, the goal becomes imax(imax((a + b) + c;0 + c);0) = imax(a + b + c;0). There are 2 possible cases. The case 0 + c <= 0 is trivial. Consider 0 < 0 + c. Now, the original expression can be transformed to imax((a + b) + c;0 + c) = imax(a + b + c;0). Equivalently, the original expression can be rewritten as imax((a + b) + c;0) = imax(a + b + c;0). This proves the theorem. 

ndiff_ndiff  
Theorem: For integer x and y, x = y if and
only if x = +/y. Assume x and y are integers. Equivalently, the original expression can be rewritten as x = y if and only if x = +/y. There are 4 possible cases. Consider that 0<=x and 0<=y. Now, the original expression can be rewritten as x=y if and only if x = +/y. Consider that 0<=x and y<0. Equivalently, the original expression can be rewritten as x=y if and only if x = +/y. Assume that x<0 and 0<=y. Equivalently, the original expression can be rewritten as x=y if and only if x=+/y. Consider that x<0 and y<0. Equivalently, the original expression can be rewritten as x=y if and only if x=+/y. 
absval_eq  
Theorem: For integer a and b, if a != 0 if b !=
0 then a*b != 0. Assume that a and b are integers, a != 0 and b != 0. There are 2 possible cases. Consider a*b = 0. By applying the int_entire lemma, we know a*b != 0. Assume a*b != 0. The result follows trivially. This proves the theorem. 

int_entire_a  
Theorem: For natural number a and b, a  (a 
b) = imin(a;b). Consider a and b are natural numbers. From the minus_imax lemma, we conclude imax(a + imax(a + b;0);0) = imin(a;b). Applying the imin_add_r lemma, the goal becomes imax(imin((a + b);0) + a;0) = imin(a;b). There are 2 possible cases. Assume a <= b. By applying the imax lemma, we conclude imax(a;0) = a. Assume b < a. By applying the imax lemma, the goal becomes imax(b;0) = b. This proves the theorem. 

ndiff_ndiff_eq_imin  
Theorem: For integer a and nonzero integer b, a
rem b = a rem b. Consider that a is an integer, b is a nonzero integer, 0 <= a and 0 <= b. Consider that a is an integer, b is a nonzero integer, 0 <= a and 0 <= b. Applying the rem_4_to_1 lemma, the goal becomes a rem b = a rem b. Consider that a is an integer, b is a nonzero integer, 0 <= a and!(0 <= b). From the rem_4_to_1 lemma, we conclude a rem b = a rem b. Consider that a is an integer, b is a nonzero integer!(0 <= a) and 0 <= b. Applying the rem_3_to_1 lemma, the goal becomes a rem b = a rem b. Assume that a is an integer, b is a nonzero integer !(0 <= a) and !(0 <= b). By the rem_3_to_1 lemma, the goal becomes a rem b = a rem b. This proves the theorem. 

rem_sym  
Theorem: For integer i and j, if i>=j then
i <= j. Assume that i and j are integers and i>=j. Now, the original expression can be rewritten as i <= j. By the add_functionality_wrt_le lemma, we know i <= j. This proves the theorem. 

minus_functionality_wrt_le  
Theorem: For integer a and b, a=0 or b=0 then
a*b=0. Assume that a and b are integers and a=0. Consider that a and b are integers and a=0. Equivalently, the original expression can be rewritten as a*b=0. Consider that a and b are integers and b=0. Equivalently, the goal can be transformed to a*b=0. This proves the theorem. 
zero_ann_a  
Theorem: For integer a and b, if !(a*b=0),
!(a=0) and !(b=0). Consider that a and b are integers and a=0. Consider that a and b are integers and a=0. Now, the original expression can be transformed to a*b=0. Consider that a and b are integers and b=0. Now, the original expression can be rewritten as a*b=0. This proves the theorem. 
zero_ann_b  
Theorem: For integer a and b and positive
natural n, if a<b then n*a<n*b. Assume that a and b are integers, n is a positive natural and a<b. There are 2 possible cases. Consider that 0<n and 1=n. Now, the goal can be transformed to n*a < n*b. Assume that 1<n and (n1)*a < (n1)*b. From the lt_to_le_rw lemma, we conclude n*a < n*b. By the add_functionality_wrt_le lemma, the goal becomes n*a < n*b. The result follows trivially. This proves the theorem. 

mul_preserves_lt  
Theorem: For integer a and b and positive
natural n, if n*a < n*b then a<b. Consider that a and b are integers, n is a positive natural and n*a < n*b. Equivalently, the original expression can be rewritten as a<b. By applying the mul_preserves_le lemma, the goal becomes a<b. This proves the theorem. 

mul_cancel_in_lt  
Theorem: For integer a and b, if a*b=0 a=0 or
b=0. Assume that a and b are integers and a*b=0. There are 2 possible cases. Assume b=0. Now, the goal can be transformed to a=0 or b=0. Consider !(b=0). Now, the original expression can be rewritten as a=0 or b=0. By applying the mul_cancel_in_eq lemma, the goal becomes a=0. The result follows trivially. This proves the theorem. 

int_entire  
Theorem: For integer i, i=0 if and only if
i=0. Assume i is an integer. There are 2 possible cases. Consider 0<=i. Now, the original expression can be transformed to i=0 if and only if i=0. Assume i<0. Equivalently, the original expression can be rewritten as i=0 if and only if i=0. This proves the theorem. 
absval_zero  
Theorem: For integer a and b,
imax(a;b)=imin(a;b). Assume a and b are integers. Equivalently, the original expression can be rewritten as if a<=b then b else a fi = if (a)<=(b) then a else b fi. This proves the theorem. 

minus_imax  
Theorem: For integer a and b,
imin(a;b)=imax(a;b). Consider a and b are integers. Equivalently, the original expression can be rewritten as if a<=b then a else b fi = if (a)<=(b) then b else a fi. This proves the theorem. 

minus_imin  
Theorem: For natural number a, a  0 = a. Assume a is a natural number. By the imax lemma, we know imax(a0;0) = a. This proves the theorem. 

ndiff_id_r  
Theorem: For natural number a, 0  a = 0. Consider a is a natural number. Applying the imax lemma, we know imax(0a;0) = 0. This proves the theorem. 

ndiff_ann_l  
Theorem: For natural number a and integer b,
(a+b)  b = a. Assume that a is a natural number and b is an integer. From the imax lemma, the goal becomes imax((a+b)  b;0) = a. This proves the theorem. 

ndiff_inv  
Theorem: For integer a and b, (a  b) + b =
imax(a;b). Assume a and b are integers. From the imax_add_r lemma, we know imax(ab;0) + b = imax(a;b). This proves the theorem. 

ndiff_add_eq_imax  
Theorem: For integer a and b, a  b = 0 if and
only if a<=b. Consider a and b are integers. Equivalently, the goal can be rewritten as if (ab)<=0 then 0 else a fi = 0 if and only if a<=b. This proves the theorem. 

ndiff_zero  
Theorem: For integer a and nonzero integer n, a
rem n = a  (a/n)*n. Assume that a is an integer and n is a nonzero integer. From the add_cancel_in_eq lemma, we conclude a rem n = a  (a/n)*n. By the div_rem_sum lemma, the goal becomes a rem n + (a/n)*n = (a  (a/n)*n) + (a/n)*n. This proves the theorem. 

rem_to_div  
Theorem: For natural number a and positive
natural n, Div(a;n;a/n). Consider that a is a natural number and n is a positive natural. Using the rem_bounds_1 lemma, the goal becomes n*(a/n) <= a < n*(a/n + 1). Equivalently, the goal can be rewritten as n*(a/n) <= a < n*(a/n + 1). By the add_mono_wrt_le_rw lemma, the goal becomes n*(a/n) <= a < n*(a/n + 1). Applying the add_mono_wrt_lt_rw lemma, we conclude n*(a/n) <= a < n*(a/n + 1). By the add_com lemma, the goal becomes n*(a/n) <= a < n*(a/n + 1). Applying the add_com lemma, the goal becomes n*(a/n) <= a < n*(a/n + 1). Equivalently, the goal can be transformed to n*(a/n) <= a < n*(a/n + 1). This proves the theorem. 

div_fun_sat_div_nrel  
Theorem: For natural number a and positive
natural n, if a<n then a rem n = a. Consider that a is a natural number, n is a positive natural and a<n. Using the rem_to_div lemma, we know a rem n = a. From the div_base_case lemma, we conclude a  (a/n)*n = a. This proves the theorem. 

rem_base_case  
Theorem: For natural number a and positive
natural n, if a>=n then a rem b = (a  n) rem n. Consider that a is a natural number, n is a positive natural and a>=n. Using the rem_to_div lemma, we know a rem n = (a  n) rem n. From the div_rec_case lemma, the goal becomes a  (a/n)*n = a  n  ((a  n)/n)*n. Equivalently, the goal can be transformed to a  ((a  n)/n + 1)*n = a  n  ((a  n)/n)*n. The result follows trivially. This proves the theorem. 

rem_rec_case 
Questions or comments about this project? Email Amanda
HollandMinkley at hollandm@cs.cornell.edu
Return to Amanda's Research Page, or Amanda's Home Page.