Library Coq.Numbers.Natural.BigN.NMake


NMake

From a cyclic Z/nZ representation to arbitrary precision natural numbers.
NB: This file contain the part which is independent from the underlying representation. The representation-dependent (and macro-generated) part is now in NMake_gen.
Let's include the macro-generated part. Even if we can't functorize things (due to Eval red_t below), the rest of the module only uses elements mentionned in interface NAbstract.

 Include NMake_gen.Make W0.

 Open Scope Z_scope.


 Definition eq (x y : t) := [x] = [y].


 Ltac red_t :=
  match goal with |- ?u => let v := (eval red_t in u) in change v end.

Generic results


 Tactic Notation "destr_t" constr(x) "as" simple_intropattern(pat) :=
  destruct (destr_t x) as pat; cbv zeta;
  rewrite ?iter_mk_t, ?spec_mk_t, ?spec_reduce.

 Lemma spec_same_level : forall A (P:Z->Z->A->Prop)
  (f : forall n, dom_t n -> dom_t n -> A),
  (forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)) ->
  forall x y, P [x] [y] (same_level f x y).

 Theorem spec_pos: forall x, 0 <= [x].

 Lemma digits_dom_op_incr : forall n m, (n<=m)%nat ->
  (ZnZ.digits (dom_op n) <= ZnZ.digits (dom_op m))%positive.

 Definition to_N (x : t) := Z.to_N (to_Z x).

Zero, One


 Definition zero := mk_t O ZnZ.zero.
 Definition one := mk_t O ZnZ.one.

 Theorem spec_0: [zero] = 0.

 Theorem spec_1: [one] = 1.

Successor

NB: it is crucial here and for the rest of this file to preserve the let-in's. They allow to pre-compute once and for all the field access to Z/nZ initial structures (when n=0..6).


 Definition succ : t -> t := Eval red_t in iter_t succn.

 Lemma succ_fold : succ = iter_t succn.

 Theorem spec_succ: forall n, [succ n] = [n] + 1.

Two
Not really pretty, but since W0 might be Z/2Z, we're not sure there's a proper 2 there.

 Definition two := succ one.

 Lemma spec_2 : [two] = 2.

Addition



 Definition add : t -> t -> t := Eval red_t in same_level addn.

 Lemma add_fold : add = same_level addn.

 Theorem spec_add: forall x y, [add x y] = [x] + [y].

Predecessor



 Definition pred : t -> t := Eval red_t in iter_t predn.

 Lemma pred_fold : pred = iter_t predn.

 Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1.

 Theorem spec_pred0 : forall x, [x] = 0 -> [pred x] = 0.

 Lemma spec_pred x : [pred x] = Z.max 0 ([x]-1).

Subtraction



 Definition sub : t -> t -> t := Eval red_t in same_level subn.

 Lemma sub_fold : sub = same_level subn.

 Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y].

 Theorem spec_sub0 : forall x y, [x] < [y] -> [sub x y] = 0.

 Lemma spec_sub : forall x y, [sub x y] = Z.max 0 ([x]-[y]).

Comparison


 Definition comparen_m n :
  forall m, word (dom_t n) (S m) -> dom_t n -> comparison :=
  let op := dom_op n in
  let zero := ZnZ.zero (Ops:=op) in
  let compare := ZnZ.compare (Ops:=op) in
  let compare0 := compare zero in
  fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).

 Let spec_comparen_m:
  forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
   comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y).

 Definition comparenm n m wx wy :=
    let mn := Max.max n m in
    let d := diff n m in
    let op := make_op mn in
    ZnZ.compare
       (castm (diff_r n m) (extend_tr wx (snd d)))
       (castm (diff_l n m) (extend_tr wy (fst d))).


 Definition compare : t -> t -> comparison :=
  Eval lazy beta iota delta [iter_sym dom_op dom_t comparen_m] in
  compare_folded.

 Lemma compare_fold : compare = compare_folded.

 Theorem spec_compare : forall x y,
   compare x y = Z.compare [x] [y].

 Definition eqb (x y : t) : bool :=
  match compare x y with
  | Eq => true
  | _ => false
  end.

 Theorem spec_eqb x y : eqb x y = Z.eqb [x] [y].

 Definition lt (n m : t) := [n] < [m].
 Definition le (n m : t) := [n] <= [m].

 Definition ltb (x y : t) : bool :=
  match compare x y with
  | Lt => true
  | _ => false
  end.

 Theorem spec_ltb x y : ltb x y = Z.ltb [x] [y].

 Definition leb (x y : t) : bool :=
  match compare x y with
  | Gt => false
  | _ => true
  end.

 Theorem spec_leb x y : leb x y = Z.leb [x] [y].

 Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
 Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end.

 Theorem spec_max : forall n m, [max n m] = Z.max [n] [m].

 Theorem spec_min : forall n m, [min n m] = Z.min [n] [m].

Multiplication


 Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t :=
  let op := dom_op n in
  let zero := ZnZ.zero in
  let succ := ZnZ.succ (Ops:=op) in
  let add_c := ZnZ.add_c (Ops:=op) in
  let mul_c := ZnZ.mul_c (Ops:=op) in
  let ww := @ZnZ.WW _ op in
  let ow := @ZnZ.OW _ op in
  let eq0 := ZnZ.eq0 in
  let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in
  let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in
  fun m x y =>
   let (w,r) := mul_add_n1 (S m) x y zero in
   if eq0 w then mk_t_w' n m r
   else mk_t_w' n (S m) (WW (extend n m w) r).

 Definition mulnm n m x y :=
    let mn := Max.max n m in
    let d := diff n m in
    let op := make_op mn in
     reduce_n (S mn) (ZnZ.mul_c
       (castm (diff_r n m) (extend_tr x (snd d)))
       (castm (diff_l n m) (extend_tr y (fst d)))).


 Definition mul : t -> t -> t :=
  Eval lazy beta iota delta
   [iter_sym dom_op dom_t reduce succ_t extend zeron
    wn_mul DoubleMul.w_mul_add mk_t_w'] in
  mul_folded.

 Lemma mul_fold : mul = mul_folded.

 Lemma spec_muln:
   forall n (x: word _ (S n)) y,
     [Nn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [Nn n x] * [Nn n y].

 Lemma spec_mul_add_n1: forall n m x y z,
  let (q,r) := DoubleMul.double_mul_add_n1 ZnZ.zero ZnZ.WW ZnZ.OW
          (DoubleMul.w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c)
          (S m) x y z in
  ZnZ.to_Z q * (base (ZnZ.digits (nmake_op _ (dom_op n) (S m))))
   + eval n (S m) r =
  eval n (S m) x * ZnZ.to_Z y + ZnZ.to_Z z.

 Lemma spec_wn_mul : forall n m x y,
   [wn_mul n m x y] = (eval n (S m) x) * ZnZ.to_Z y.

 Theorem spec_mul : forall x y, [mul x y] = [x] * [y].

Division by a smaller number


 Definition wn_divn1 n :=
  let op := dom_op n in
  let zd := ZnZ.zdigits op in
  let zero := ZnZ.zero in
  let ww := ZnZ.WW in
  let head0 := ZnZ.head0 in
  let add_mul_div := ZnZ.add_mul_div in
  let div21 := ZnZ.div21 in
  let compare := ZnZ.compare in
  let sub := ZnZ.sub in
  let ddivn1 :=
    DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
  fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v).

 Definition div_gtnm n m wx wy :=
    let mn := Max.max n m in
    let d := diff n m in
    let op := make_op mn in
    let (q, r):= ZnZ.div_gt
         (castm (diff_r n m) (extend_tr wx (snd d)))
         (castm (diff_l n m) (extend_tr wy (fst d))) in
    (reduce_n mn q, reduce_n mn r).


 Definition div_gt :=
  Eval lazy beta iota delta
   [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t] in
  div_gt_folded.

 Lemma div_gt_fold : div_gt = div_gt_folded.

 Lemma spec_get_endn: forall n m x y,
  eval n m x <= [mk_t n y] ->
   [mk_t n (DoubleBase.get_low (zeron n) m x)] = eval n m x.

 Definition spec_divn1 n :=
   DoubleDivn1.spec_double_divn1
    (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
    ZnZ.WW ZnZ.head0
    ZnZ.add_mul_div ZnZ.div21
    ZnZ.compare ZnZ.sub ZnZ.to_Z
    ZnZ.spec_to_Z
    ZnZ.spec_zdigits
    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
    ZnZ.spec_add_mul_div ZnZ.spec_div21
    ZnZ.spec_compare ZnZ.spec_sub.

 Lemma spec_div_gt_aux : forall x y, [x] > [y] -> 0 < [y] ->
   let (q,r) := div_gt x y in
   [x] = [q] * [y] + [r] /\ 0 <= [r] < [y].

 Theorem spec_div_gt: forall x y, [x] > [y] -> 0 < [y] ->
  let (q,r) := div_gt x y in
  [q] = [x] / [y] /\ [r] = [x] mod [y].

General Division


 Definition div_eucl (x y : t) : t * t :=
  if eqb y zero then (zero,zero) else
  match compare x y with
  | Eq => (one, zero)
  | Lt => (zero, x)
  | Gt => div_gt x y
  end.

 Theorem spec_div_eucl: forall x y,
      let (q,r) := div_eucl x y in
      ([q], [r]) = Z.div_eucl [x] [y].

 Definition div (x y : t) : t := fst (div_eucl x y).

 Theorem spec_div:
   forall x y, [div x y] = [x] / [y].

Modulo by a smaller number


 Definition wn_modn1 n :=
  let op := dom_op n in
  let zd := ZnZ.zdigits op in
  let zero := ZnZ.zero in
  let head0 := ZnZ.head0 in
  let add_mul_div := ZnZ.add_mul_div in
  let div21 := ZnZ.div21 in
  let compare := ZnZ.compare in
  let sub := ZnZ.sub in
  let dmodn1 :=
    DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in
  fun m x y => reduce n (dmodn1 (S m) x y).

 Definition mod_gtnm n m wx wy :=
    let mn := Max.max n m in
    let d := diff n m in
    let op := make_op mn in
    reduce_n mn (ZnZ.modulo_gt
         (castm (diff_r n m) (extend_tr wx (snd d)))
         (castm (diff_l n m) (extend_tr wy (fst d)))).


 Definition mod_gt :=
  Eval lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron] in
  mod_gt_folded.

 Lemma mod_gt_fold : mod_gt = mod_gt_folded.

 Definition spec_modn1 n :=
   DoubleDivn1.spec_double_modn1
    (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
    ZnZ.WW ZnZ.head0
    ZnZ.add_mul_div ZnZ.div21
    ZnZ.compare ZnZ.sub ZnZ.to_Z
    ZnZ.spec_to_Z
    ZnZ.spec_zdigits
    ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
    ZnZ.spec_add_mul_div ZnZ.spec_div21
    ZnZ.spec_compare ZnZ.spec_sub.

 Theorem spec_mod_gt:
   forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].

General Modulo


 Definition modulo (x y : t) : t :=
  if eqb y zero then zero else
  match compare x y with
  | Eq => zero
  | Lt => x
  | Gt => mod_gt x y
  end.

 Theorem spec_modulo:
   forall x y, [modulo x y] = [x] mod [y].

Square



 Definition square : t -> t := Eval red_t in iter_t squaren.

 Lemma square_fold : square = iter_t squaren.

 Theorem spec_square: forall x, [square x] = [x] * [x].

Square Root



 Definition sqrt : t -> t := Eval red_t in iter_t sqrtn.

 Lemma sqrt_fold : sqrt = iter_t sqrtn.

 Theorem spec_sqrt_aux: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.

 Theorem spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].

Power


 Fixpoint pow_pos (x:t)(p:positive) : t :=
  match p with
  | xH => x
  | xO p => square (pow_pos x p)
  | xI p => mul (square (pow_pos x p)) x
  end.

 Theorem spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.

 Definition pow_N (x:t)(n:N) : t := match n with
  | BinNat.N0 => one
  | BinNat.Npos p => pow_pos x p
 end.

 Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n.

 Definition pow (x y:t) : t := pow_N x (to_N y).

 Theorem spec_pow : forall x y, [pow x y] = [x] ^ [y].

digits

Number of digits in the representation of a numbers (including head zero's). NB: This function isn't a morphism for setoid eq.


 Definition digits : t -> positive := Eval red_t in iter_t digitsn.

 Lemma digits_fold : digits = iter_t digitsn.

 Theorem spec_digits: forall x, 0 <= [x] < 2 ^ Zpos (digits x).

 Lemma digits_level : forall x, digits x = ZnZ.digits (dom_op (level x)).

Gcd


 Definition gcd_gt_body a b cont :=
  match compare b zero with
  | Gt =>
    let r := mod_gt a b in
    match compare r zero with
    | Gt => cont r (mod_gt b r)
    | _ => b
    end
  | _ => a
  end.

 Theorem Zspec_gcd_gt_body: forall a b cont p,
    [a] > [b] -> [a] < 2 ^ p ->
      (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] ->
         Zis_gcd [a1] [b1] [cont a1 b1]) ->
      Zis_gcd [a] [b] [gcd_gt_body a b cont].

 Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) : t :=
  gcd_gt_body a b
    (fun a b =>
       match p with
       | xH => cont a b
       | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b
       | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b
       end).

 Theorem Zspec_gcd_gt_aux: forall p n a b cont,
    [a] > [b] -> [a] < 2 ^ (Zpos p + n) ->
      (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] ->
            Zis_gcd [a1] [b1] [cont a1 b1]) ->
          Zis_gcd [a] [b] [gcd_gt_aux p cont a b].

 Definition gcd_cont a b :=
  match compare one b with
  | Eq => one
  | _ => a
  end.

 Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b.

 Theorem spec_gcd_gt: forall a b,
   [a] > [b] -> [gcd_gt a b] = Z.gcd [a] [b].

 Definition gcd (a b : t) : t :=
  match compare a b with
  | Eq => a
  | Lt => gcd_gt b a
  | Gt => gcd_gt a b
  end.

 Theorem spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].

Parity test


 Definition even : t -> bool := Eval red_t in
   iter_t (fun n x => ZnZ.is_even x).

 Definition odd x := negb (even x).

 Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x).

 Theorem spec_even_aux: forall x,
   if even x then [x] mod 2 = 0 else [x] mod 2 = 1.

 Theorem spec_even: forall x, even x = Z.even [x].

 Theorem spec_odd: forall x, odd x = Z.odd [x].

Conversion


 Definition pheight p :=
   Peano.pred (Pos.to_nat (get_height (ZnZ.digits (dom_op 0)) (plength p))).

 Theorem pheight_correct: forall p,
    Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z.of_nat (pheight p))).

 Definition of_pos (x:positive) : t :=
  let n := pheight x in
  reduce n (snd (ZnZ.of_pos x)).

 Theorem spec_of_pos: forall x,
   [of_pos x] = Zpos x.

 Definition of_N (x:N) : t :=
  match x with
  | BinNat.N0 => zero
  | Npos p => of_pos p
  end.

 Theorem spec_of_N: forall x,
   [of_N x] = Z.of_N x.

head0 and tail0

Number of zero at the beginning and at the end of the representation of the number. NB: these functions are not morphism for setoid eq.


 Definition head0 : t -> t := Eval red_t in iter_t head0n.

 Lemma head0_fold : head0 = iter_t head0n.

 Theorem spec_head00: forall x, [x] = 0 -> [head0 x] = Zpos (digits x).

 Lemma pow2_pos_minus_1 : forall z, 0<z -> 2^(z-1) = 2^z / 2.

 Theorem spec_head0: forall x, 0 < [x] ->
   2 ^ (Zpos (digits x) - 1) <= 2 ^ [head0 x] * [x] < 2 ^ Zpos (digits x).


 Definition tail0 : t -> t := Eval red_t in iter_t tail0n.

 Lemma tail0_fold : tail0 = iter_t tail0n.

 Theorem spec_tail00: forall x, [x] = 0 -> [tail0 x] = Zpos (digits x).

 Theorem spec_tail0: forall x,
   0 < [x] -> exists y, 0 <= y /\ [x] = (2 * y + 1) * 2 ^ [tail0 x].

Ndigits

Same as digits but encoded using large integers NB: this function is not a morphism for setoid eq.


 Definition Ndigits : t -> t := Eval red_t in iter_t Ndigitsn.

 Lemma Ndigits_fold : Ndigits = iter_t Ndigitsn.

 Theorem spec_Ndigits: forall x, [Ndigits x] = Zpos (digits x).

Binary logarithm



 Definition log2 : t -> t := Eval red_t in
   let log2 := iter_t log2n in
   fun x => if eqb x zero then zero else log2 x.

 Lemma log2_fold :
   log2 = fun x => if eqb x zero then zero else iter_t log2n x.

 Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0.

 Lemma head0_zdigits : forall n (x : dom_t n),
  0 < ZnZ.to_Z x ->
  ZnZ.to_Z (ZnZ.head0 x) < ZnZ.to_Z (ZnZ.zdigits (dom_op n)).

 Lemma spec_log2_pos : forall x, [x]<>0 ->
   2^[log2 x] <= [x] < 2^([log2 x]+1).

 Lemma spec_log2 : forall x, [log2 x] = Z.log2 [x].

 Lemma log2_digits_head0 : forall x, 0 < [x] ->
   [log2 x] = Zpos (digits x) - [head0 x] - 1.

Right shift



 Definition shiftr : t -> t -> t := Eval red_t in
   same_level shiftrn.

 Lemma shiftr_fold : shiftr = same_level shiftrn.

 Lemma div_pow2_bound :forall x y z,
   0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z.

 Theorem spec_shiftr_pow2 : forall x n,
  [shiftr x n] = [x] / 2 ^ [n].
Subtraction without underflow : p <= digits
Subtraction with underflow : digits < p

 Lemma spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].

Left shift

First an unsafe version, working correctly only if the representation is large enough


 Definition unsafe_shiftl : t -> t -> t := Eval red_t in
   same_level unsafe_shiftln.

 Lemma unsafe_shiftl_fold : unsafe_shiftl = same_level unsafe_shiftln.

 Theorem spec_unsafe_shiftl_aux : forall x p K,
  0 <= K ->
  [x] < 2^K ->
  [p] + K <= Zpos (digits x) ->
  [unsafe_shiftl x p] = [x] * 2 ^ [p].

 Theorem spec_unsafe_shiftl: forall x p,
  [p] <= [head0 x] -> [unsafe_shiftl x p] = [x] * 2 ^ [p].

Then we define a function doubling the size of the representation but without changing the value of the number.


 Definition double_size : t -> t := Eval red_t in
   iter_t double_size_n.

 Lemma double_size_fold : double_size = iter_t double_size_n.

 Lemma double_size_level : forall x, level (double_size x) = S (level x).

 Theorem spec_double_size_digits:
   forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)).

 Theorem spec_double_size: forall x, [double_size x] = [x].

 Theorem spec_double_size_head0:
   forall x, 2 * [head0 x] <= [head0 (double_size x)].

 Theorem spec_double_size_head0_pos:
   forall x, 0 < [head0 (double_size x)].

Finally we iterate double_size enough before unsafe_shiftl in order to get a fully correct shiftl.

 Definition shiftl_aux_body cont x n :=
   match compare n (head0 x) with
      Gt => cont (double_size x) n
   | _ => unsafe_shiftl x n
   end.

 Theorem spec_shiftl_aux_body: forall n x p cont,
       2^ Zpos p <= [head0 x] ->
      (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->
         [cont x n] = [x] * 2 ^ [n]) ->
      [shiftl_aux_body cont x n] = [x] * 2 ^ [n].

 Fixpoint shiftl_aux p cont x n :=
   shiftl_aux_body
       (fun x n => match p with
        | xH => cont x n
        | xO p => shiftl_aux p (shiftl_aux p cont) x n
        | xI p => shiftl_aux p (shiftl_aux p cont) x n
        end) x n.

 Theorem spec_shiftl_aux: forall p q x n cont,
    2 ^ (Zpos q) <= [head0 x] ->
      (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->
         [cont x n] = [x] * 2 ^ [n]) ->
      [shiftl_aux p cont x n] = [x] * 2 ^ [n].

 Definition shiftl x n :=
  shiftl_aux_body
   (shiftl_aux_body
    (shiftl_aux (digits n) unsafe_shiftl)) x n.

 Theorem spec_shiftl_pow2 : forall x n,
   [shiftl x n] = [x] * 2 ^ [n].

 Lemma spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].

Other bitwise operations

 Definition testbit x n := odd (shiftr x n).

 Lemma spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].

 Definition div2 x := shiftr x one.

 Lemma spec_div2: forall x, [div2 x] = Z.div2 [x].


 Definition lor : t -> t -> t := Eval red_t in same_level lorn.

 Lemma lor_fold : lor = same_level lorn.

 Theorem spec_lor x y : [lor x y] = Z.lor [x] [y].


 Definition land : t -> t -> t := Eval red_t in same_level landn.

 Lemma land_fold : land = same_level landn.

 Theorem spec_land x y : [land x y] = Z.land [x] [y].


 Definition lxor : t -> t -> t := Eval red_t in same_level lxorn.

 Lemma lxor_fold : lxor = same_level lxorn.

 Theorem spec_lxor x y : [lxor x y] = Z.lxor [x] [y].


 Definition ldiff : t -> t -> t := Eval red_t in same_level ldiffn.

 Lemma ldiff_fold : ldiff = same_level ldiffn.

 Lemma ldiff_alt x y p :
  0 <= x < 2^p -> 0 <= y < 2^p ->
  Z.ldiff x y = Z.land x (Z.lxor y (2^p - 1)).

 Theorem spec_ldiff x y : [ldiff x y] = Z.ldiff [x] [y].

End Make.