More properties about subtraction and borrow.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 59 insertions, 18 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 49fa48f..88a9683 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1847,6 +1847,24 @@ Proof.
   exists (-1). ring. 
 Qed.
 
+Theorem sub_add_not:
+  forall x y, sub x y = add (add x (not y)) one.
+Proof.
+  intros. rewrite sub_add_opp. rewrite neg_not. 
+  rewrite ! add_assoc. auto.
+Qed.
+
+Theorem sub_add_not_3:
+  forall x y b,
+  b = zero \/ b = one ->
+  sub (sub x y) b = add (add x (not y)) (xor b one).
+Proof.
+  intros. rewrite ! sub_add_not. rewrite ! add_assoc. f_equal. f_equal.
+  rewrite <- neg_not. rewrite <- sub_add_opp. destruct H; subst b.
+  rewrite xor_zero_l. rewrite sub_zero_l. auto.
+  rewrite xor_idem. rewrite sub_idem. auto.
+Qed.
+
 Theorem sub_borrow_add_carry:
   forall x y b,
   b = zero \/ b = one ->
@@ -2898,24 +2916,6 @@ Qed.
 
 (** ** Properties of integer zero extension and sign extension. *)
 
-(*
-Lemma Ziter_ind:
-  forall (A: Type) (f: A -> A) (P: Z -> A -> Prop) n x,
-  (n <= 0 -> P n x) ->
-  (forall n x, 0 <= n -> P n x -> P (Z.succ n) (f x)) ->
-  P n (Z.iter n f x).
-Proof.
-  intros until x; intros BASE SUCC. intros. 
-  unfold Z.iter. destruct n. 
-  - apply BASE. omega.
-  - induction p using Pos.peano_ind.
-    + simpl Pos.iter. apply (SUCC 0). omega. apply BASE. omega. 
-    + rewrite Pos2Z.inj_succ. rewrite Pos.iter_succ. 
-      apply SUCC. compute; intuition congruence. auto.
-  - apply BASE. compute; intuition congruence.
-Qed.
-*)
-
 Lemma Ziter_base:
   forall (A: Type) n (f: A -> A) x, n <= 0 -> Z.iter n f x = x.
 Proof.
@@ -4202,6 +4202,47 @@ Proof.
   apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. 
 Qed.
 
+Lemma decompose_sub:
+  forall xh xl yh yl,
+  sub (ofwords xh xl) (ofwords yh yl) =
+  ofwords (Int.sub (Int.sub xh yh) (Int.sub_borrow xl yl Int.zero))
+          (Int.sub xl yl).
+Proof.
+  intros. symmetry. rewrite ofwords_add.
+  apply eqm_samerepr. 
+  rewrite ! ofwords_add'. rewrite (Int.unsigned_sub_borrow xl yl). 
+  set (bb := Int.sub_borrow xl yl Int.zero).
+  set (Xl := Int.unsigned xl); set (Xh := Int.unsigned xh);
+  set (Yl := Int.unsigned yl); set (Yh := Int.unsigned yh).
+  change Int.modulus with (two_p 32).
+  replace (Xh * two_p 32 + Xl - (Yh * two_p 32 + Yl))
+     with ((Xh - Yh) * two_p 32 + (Xl - Yl)) by ring.
+  replace (Int.unsigned (Int.sub (Int.sub xh yh) bb) * two_p 32 +
+              (Xl - Yl + Int.unsigned bb * two_p 32))
+     with ((Int.unsigned (Int.sub (Int.sub xh yh) bb) + Int.unsigned bb) * two_p 32
+           + (Xl - Yl)) by ring.
+  apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32.
+  replace (Xh - Yh) with ((Xh - Yh - Int.unsigned bb) + Int.unsigned bb) by ring.
+  apply Int.eqm_add. 2: apply Int.eqm_refl.
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. 
+  apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. 
+Qed.
+
+Lemma decompose_sub':
+  forall xh xl yh yl,
+  sub (ofwords xh xl) (ofwords yh yl) =
+  ofwords (Int.add (Int.add xh (Int.not yh)) (Int.add_carry xl (Int.not yl) Int.one))
+          (Int.sub xl yl).
+Proof.
+  intros. rewrite decompose_sub. f_equal. 
+  rewrite Int.sub_borrow_add_carry by auto.
+  rewrite Int.sub_add_not_3. rewrite Int.xor_assoc. rewrite Int.xor_idem. 
+  rewrite Int.xor_zero. auto.
+  rewrite Int.xor_zero_l. unfold Int.add_carry.
+  destruct (zlt (Int.unsigned xl + Int.unsigned (Int.not yl) + Int.unsigned Int.one) Int.modulus);
+  compute; [right|left]; apply Int.mkint_eq; auto.
+Qed.
+
 Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y).
 
 Lemma decompose_mul: