Increase precision of abstract subtraction for parity (thanks to Aleksejs Popovs for the suggestion)

This commit is contained in:
Adam Chlipala 2018-03-20 17:18:31 -04:00
parent f46bed19bb
commit 4bf1c3fc7c

View file

@ -187,6 +187,7 @@ Definition parity_add (x y : parity) :=
Definition parity_subtract (x y : parity) :=
match x, y with
| Even, Even => Even
| Odd, Odd => Even
| _, _ => Either
end.
(* Note subtleties with [Either]s above, to deal with underflow at zero! *)
@ -304,6 +305,7 @@ Proof.
exists (x0 + x); ring.
exists (x0 + x + 1); ring.
exists (x - x0); linear_arithmetic.
exists (x - x0); linear_arithmetic.
exists (x * x0 * 2); ring.
exists ((x * 2 + 1) * x0); ring.
exists (n * x); ring.
@ -327,6 +329,7 @@ Proof.
exists x; ring.
exists x; ring.
exists x; ring.
exists x; ring.
exists x0; ring.
exists x0; ring.
Qed.