Automatically Generated Texts from Nuprl Proofs

The following proof texts were automatically generated by the methods described in the paper Verbalization of High-Level Formal Proofs. Amanda M. Holland-Minkley, 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 corpus-collecting 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(a-b;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 a -- b == imax(a - b;0)
imax imax(a;b) == if a z b then b else a fi
imax_add_r a,b,c:. imax(a;b) + c = imax(a + c;b + c)
imax_assoc a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)
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,b:. a * b = 0 a = 0 b = 0
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 a -- b == imax(a - b;0)
imin imin(a;b) == if a z b then a else b fi
imax imax(a;b) == if a z b then b else a fi
minus_imax a,b:. -imax(a;b) = imin(-a;-b)
imin_add_r a,b,c:. imin(a;b) + c = imin(a + c;b + c)
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_4_to_1 a:. n:{...-1}. a rem n = a rem -n
rem_3_to_1 a:{...0}. n:{...-1}. a rem n = -(-a rem -n)
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.
add_functionality_wrt_le i1,i2,j1,j2:. i1 j1 i2 j2 i1 + i2 j1 + j2
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 (n-1)*a < (n-1)*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.
lt_to_le_rw i,j:. {i < j i + 1 j}
add_functionality_wrt_le i1,i2,j1,j2:. i1 j1 i2 j2 i1 + i2 j1 + j2
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_preserves_le a,b:. n:. a b n * a n * b
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.
mul_cancel_in_eq a,b:. n:. n * a = n * b a = b
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.
imin imin(a;b) == if a z b then a else b fi
imax imax(a;b) == if a z b then b else a fi
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.
imin imin(a;b) == if a z b then a else b fi
imax imax(a;b) == if a z b then b else a fi
minus_imin
Theorem: For natural number a, a -- 0 = a.

Assume a is a natural number. By the imax lemma, we know imax(a-0;0) = a. This proves the theorem.
ndiff a -- b == imax(a - b;0)
imax imax(a;b) == if a z b then b else a fi
ndiff_id_r
Theorem: For natural number a, 0 -- a = 0.

Consider a is a natural number. Applying the imax lemma, we know imax(0-a;0) = 0. This proves the theorem.
ndiff a -- b == imax(a - b;0)
imax imax(a;b) == if a z b then b else a fi
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 a -- b == imax(a - b;0)
imax imax(a;b) == if a z b then b else a fi
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(a-b;0) + b = imax(a;b). This proves the theorem.
ndiff a -- b == imax(a - b;0)
imax imax(a;b) == if a z b then b else a fi
imax_add_r a,b,c:. imax(a;b) + c = imax(a + c;b + c)
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 (a-b)<=0 then 0 else a fi = 0 if and only if a<=b. This proves the theorem.
ndiff a -- b == imax(a - b;0)
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.
add_cancel_in_eq a,b,n:. a + n = b + n a = b
div_rem_sum a,b,n:. a + n = b + n a = b
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 Div(a;n;q) == n * q a < n * (q + 1)
rem_bounds_1 a:. n:. 0 a rem n a rem n < n
add_mono_wrt_le_rw a,b,n:. {a b a + n b + n}
add_mono_wrt_lt_rw a,b,n:. {a < b a + n < b + n}
add_com a,b:. a + b = b + a
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_to_div a:. n:. a rem n = a - (a n) * n
div_base_case a:. n:. a < n a n = 0
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_to_div a:. n:. a rem n = a - (a n) * n
div_rec_case a:. n:. a n a n = (a - n) n + 1
rem_rec_case

Questions or comments about this project? E-mail Amanda Holland-Minkley at hollandm@cs.cornell.edu
Return to Amanda's Research Page, or Amanda's Home Page.