NBits.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Bool NAxioms NSub NPow NDiv NParity NLog.

Derived properties of bitwise operations

Module Type NBitsProp
 (Import A : NAxiomsSig')
 (Import B : NSubProp A)
 (Import C : NParityProp A B)
 (Import D : NPowProp A B C)
 (Import E : NDivProp A B)
 (Import F : NLog2Prop A B C D).

Include BoolEqualityFacts A.

Ltac order_nz := try apply pow_nonzero; order'.
Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz.

Some properties of power and division

Lemma pow_sub_r : forall a b c, a~=0 -> c<=b -> a^(b-c) == a^b / a^c.forall a b c : t,
a ~= 0 -> c <= b -> a ^ (b - c) == a ^ b / a ^ c
Proof.forall a b c : t,
a ~= 0 -> c <= b -> a ^ (b - c) == a ^ b / a ^ c
 intros a b c Ha H.a, b, c:t
Ha:a ~= 0
H:c <= b
a ^ (b - c) == a ^ b / a ^ c
 apply div_unique with 0.a, b, c:t
Ha:a ~= 0
H:c <= b
0 < a ^ c
a, b, c:t
Ha:a ~= 0
H:c <= b
a ^ b == a ^ c * a ^ (b - c) + 0
 generalize (pow_nonzero a c Ha) (le_0_l (a^c)); order'.a, b, c:t
Ha:a ~= 0
H:c <= b
a ^ b == a ^ c * a ^ (b - c) + 0
 nzsimpl.a, b, c:t
Ha:a ~= 0
H:c <= b
a ^ b == a ^ c * a ^ (b - c) now rewrite <- pow_add_r, add_comm, sub_add.
Qed.

Lemma pow_div_l : forall a b c, b~=0 -> a mod b == 0 ->
 (a/b)^c == a^c / b^c.forall a b c : t,
b ~= 0 -> a mod b == 0 -> (a / b) ^ c == a ^ c / b ^ c
Proof.forall a b c : t,
b ~= 0 -> a mod b == 0 -> (a / b) ^ c == a ^ c / b ^ c
 intros a b c Hb H.a, b, c:t
Hb:b ~= 0
H:a mod b == 0
(a / b) ^ c == a ^ c / b ^ c
 apply div_unique with 0.a, b, c:t
Hb:b ~= 0
H:a mod b == 0
0 < b ^ c
a, b, c:t
Hb:b ~= 0
H:a mod b == 0
a ^ c == b ^ c * (a / b) ^ c + 0
 generalize (pow_nonzero b c Hb) (le_0_l (b^c)); order'.a, b, c:t
Hb:b ~= 0
H:a mod b == 0
a ^ c == b ^ c * (a / b) ^ c + 0
 nzsimpl.a, b, c:t
Hb:b ~= 0
H:a mod b == 0
a ^ c == b ^ c * (a / b) ^ c rewrite <- pow_mul_l.a, b, c:t
Hb:b ~= 0
H:a mod b == 0
a ^ c == (b * (a / b)) ^ c f_equiv.a, b, c:t
Hb:b ~= 0
H:a mod b == 0
a == b * (a / b) now apply div_exact.
Qed.

An injection from bits true and false to numbers 1 and 0. We declare it as a (local) coercion for shorter statements.

Definition b2n (b:bool) := if b then 1 else 0.
Coercion b2n : bool >-> t.

Instance b2n_proper : Proper (Logic.eq ==> eq) b2n.Proper (Logic.eq ==> eq) b2n
Proof.Proper (Logic.eq ==> eq) b2n solve_proper. Qed.

Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b.a:t
exists (a' : t) (b : bool), a == 2 * a' + b
Proof.a:t
exists (a' : t) (b : bool), a == 2 * a' + b
 elim (Even_or_Odd a); [intros (a',H)| intros (a',H)].a, a':t
H:a == 2 * a'
exists (a'0 : t) (b : bool), a == 2 * a'0 + b
a, a':t
H:a == 2 * a' + 1
exists (a'0 : t) (b : bool), a == 2 * a'0 + b
 exists a'.a, a':t
H:a == 2 * a'
exists b : bool, a == 2 * a' + b
a, a':t
H:a == 2 * a' + 1
exists (a'0 : t) (b : bool), a == 2 * a'0 + b exists false.a, a':t
H:a == 2 * a'
a == 2 * a' + false
a, a':t
H:a == 2 * a' + 1
exists (a'0 : t) (b : bool), a == 2 * a'0 + b now nzsimpl.a, a':t
H:a == 2 * a' + 1
exists (a'0 : t) (b : bool), a == 2 * a'0 + b
 exists a'.a, a':t
H:a == 2 * a' + 1
exists b : bool, a == 2 * a' + b exists true.a, a':t
H:a == 2 * a' + 1
a == 2 * a' + true now simpl.
Qed.

We can compact testbit_odd_0 testbit_even_0 testbit_even_succ testbit_odd_succ in only two lemmas.

Lemma testbit_0_r a (b:bool) : testbit (2*a+b) 0 = b.a:t
b:bool
(2 * a + b).[0] = b
Proof.a:t
b:bool
(2 * a + b).[0] = b
 destruct b; simpl; rewrite ?add_0_r.a:t
(2 * a + 1).[0] = true
a:t
(2 * a).[0] = false
 apply testbit_odd_0.a:t
(2 * a).[0] = false
 apply testbit_even_0.
Qed.

Lemma testbit_succ_r a (b:bool) n :
 testbit (2*a+b) (succ n) = testbit a n.a:t
b:bool
n:t
(2 * a + b).[S n] = a.[n]
Proof.a:t
b:bool
n:t
(2 * a + b).[S n] = a.[n]
 destruct b; simpl; rewrite ?add_0_r.a, n:t
(2 * a + 1).[S n] = a.[n]
a, n:t
(2 * a).[S n] = a.[n]
 apply testbit_odd_succ, le_0_l.a, n:t
(2 * a).[S n] = a.[n]
 apply testbit_even_succ, le_0_l.
Qed.

Alternative characterisations of testbit

This concise equation could have been taken as specification for testbit in the interface, but it would have been hard to implement with little initial knowledge about div and mod

Lemma testbit_spec' a n : a.[n] == (a / 2^n) mod 2.a, n:t
a.[n] == (a / 2 ^ n) mod 2
Proof.a, n:t
a.[n] == (a / 2 ^ n) mod 2
 revert a.n:t
forall a : t, a.[n] == (a / 2 ^ n) mod 2 induct n.forall a : t, a.[0] == (a / 2 ^ 0) mod 2
forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2
 intros a.a:t
a.[0] == (a / 2 ^ 0) mod 2
forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2 nzsimpl.a:t
a.[0] == a mod 2
forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2
 destruct (exists_div2 a) as (a' & b & H).a, a':t
b:bool
H:a == 2 * a' + b
a.[0] == a mod 2
forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2 rewrite H at 1.a, a':t
b:bool
H:a == 2 * a' + b
(2 * a' + b).[0] == a mod 2
forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2
 rewrite testbit_0_r.a, a':t
b:bool
H:a == 2 * a' + b
b == a mod 2
forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2 apply mod_unique with a'; trivial.a, a':t
b:bool
H:a == 2 * a' + b
b < 2
forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2
 destruct b; order'.forall n : t,
(forall a : t, a.[n] == (a / 2 ^ n) mod 2) ->
forall a : t, a.[S n] == (a / 2 ^ S n) mod 2
 intros n IH a.n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a:t
a.[S n] == (a / 2 ^ S n) mod 2
 destruct (exists_div2 a) as (a' & b & H).n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a, a':t
b:bool
H:a == 2 * a' + b
a.[S n] == (a / 2 ^ S n) mod 2 rewrite H at 1.n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a, a':t
b:bool
H:a == 2 * a' + b
(2 * a' + b).[S n] == (a / 2 ^ S n) mod 2
 rewrite testbit_succ_r, IH.n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a, a':t
b:bool
H:a == 2 * a' + b
(a' / 2 ^ n) mod 2 == (a / 2 ^ S n) mod 2 f_equiv.n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a, a':t
b:bool
H:a == 2 * a' + b
a' / 2 ^ n == a / 2 ^ S n
 rewrite pow_succ_r', <- div_div by order_nz.n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a, a':t
b:bool
H:a == 2 * a' + b
a' / 2 ^ n == a / 2 / 2 ^ n f_equiv.n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a, a':t
b:bool
H:a == 2 * a' + b
a' == a / 2
 apply div_unique with b; trivial.n:t
IH:forall a0 : t, a0.[n] == (a0 / 2 ^ n) mod 2
a, a':t
b:bool
H:a == 2 * a' + b
b < 2
 destruct b; order'.
Qed.

This characterisation that uses only basic operations and power was initially taken as specification for testbit. We describe a as having a low part and a high part, with the corresponding bit in the middle. This characterisation is moderatly complex to implement, but also moderately usable...

Lemma testbit_spec a n :
  exists l h, 0<=l<2^n /\ a == l + (a.[n] + 2*h)*2^n.a, n:t
exists l h : t,
  0 <= l < 2 ^ n /\ a == l + (a.[n] + 2 * h) * 2 ^ n
Proof.a, n:t
exists l h : t,
  0 <= l < 2 ^ n /\ a == l + (a.[n] + 2 * h) * 2 ^ n
 exists (a mod 2^n).a, n:t
exists h : t,
  0 <= a mod 2 ^ n < 2 ^ n /\
  a == a mod 2 ^ n + (a.[n] + 2 * h) * 2 ^ n exists (a / 2^n / 2).a, n:t
0 <= a mod 2 ^ n < 2 ^ n /\
a ==
a mod 2 ^ n + (a.[n] + 2 * (a / 2 ^ n / 2)) * 2 ^ n split.a, n:t
0 <= a mod 2 ^ n < 2 ^ n
a, n:t
a ==
a mod 2 ^ n + (a.[n] + 2 * (a / 2 ^ n / 2)) * 2 ^ n
 split; [apply le_0_l | apply mod_upper_bound; order_nz].a, n:t
a ==
a mod 2 ^ n + (a.[n] + 2 * (a / 2 ^ n / 2)) * 2 ^ n
 rewrite add_comm, mul_comm, (add_comm a.[n]).a, n:t
a ==
2 ^ n * (2 * (a / 2 ^ n / 2) + a.[n]) + a mod 2 ^ n
 rewrite (div_mod a (2^n)) at 1 by order_nz.a, n:t
2 ^ n * (a / 2 ^ n) + a mod 2 ^ n ==
2 ^ n * (2 * (a / 2 ^ n / 2) + a.[n]) + a mod 2 ^ n do 2 f_equiv.a, n:t
a / 2 ^ n == 2 * (a / 2 ^ n / 2) + a.[n]
 rewrite testbit_spec'.a, n:t
a / 2 ^ n == 2 * (a / 2 ^ n / 2) + (a / 2 ^ n) mod 2 apply div_mod.a, n:t
2 ~= 0 order'.
Qed.

Lemma testbit_true : forall a n,
 a.[n] = true <-> (a / 2^n) mod 2 == 1.forall a n : t,
a.[n] = true <-> (a / 2 ^ n) mod 2 == 1
Proof.forall a n : t,
a.[n] = true <-> (a / 2 ^ n) mod 2 == 1
 intros a n.a, n:t
a.[n] = true <-> (a / 2 ^ n) mod 2 == 1
 rewrite <- testbit_spec'; destruct a.[n]; split; simpl; now try order'.
Qed.

Lemma testbit_false : forall a n,
 a.[n] = false <-> (a / 2^n) mod 2 == 0.forall a n : t,
a.[n] = false <-> (a / 2 ^ n) mod 2 == 0
Proof.forall a n : t,
a.[n] = false <-> (a / 2 ^ n) mod 2 == 0
 intros a n.a, n:t
a.[n] = false <-> (a / 2 ^ n) mod 2 == 0
 rewrite <- testbit_spec'; destruct a.[n]; split; simpl; now try order'.
Qed.

Lemma testbit_eqb : forall a n,
 a.[n] = eqb ((a / 2^n) mod 2) 1.forall a n : t, a.[n] = ((a / 2 ^ n) mod 2 =? 1)
Proof.forall a n : t, a.[n] = ((a / 2 ^ n) mod 2 =? 1)
 intros a n.a, n:t
a.[n] = ((a / 2 ^ n) mod 2 =? 1)
 apply eq_true_iff_eq.a, n:t
a.[n] = true <-> ((a / 2 ^ n) mod 2 =? 1) = true now rewrite testbit_true, eqb_eq.
Qed.

Results about the injection b2n

Lemma b2n_inj : forall (a0 b0:bool), a0 == b0 -> a0 = b0.forall a0 b0 : bool, a0 == b0 -> a0 = b0
Proof.forall a0 b0 : bool, a0 == b0 -> a0 = b0
 intros [|] [|]; simpl; trivial; order'.
Qed.

Lemma add_b2n_double_div2 : forall (a0:bool) a, (a0+2*a)/2 == a.forall (a0 : bool) (a : t), (a0 + 2 * a) / 2 == a
Proof.forall (a0 : bool) (a : t), (a0 + 2 * a) / 2 == a
 intros a0 a.a0:bool
a:t
(a0 + 2 * a) / 2 == a rewrite mul_comm, div_add by order'.a0:bool
a:t
a0 / 2 + a == a
 now rewrite div_small, add_0_l by (destruct a0; order').
Qed.

Lemma add_b2n_double_bit0 : forall (a0:bool) a, (a0+2*a).[0] = a0.forall (a0 : bool) (a : t), (a0 + 2 * a).[0] = a0
Proof.forall (a0 : bool) (a : t), (a0 + 2 * a).[0] = a0
 intros a0 a.a0:bool
a:t
(a0 + 2 * a).[0] = a0 apply b2n_inj.a0:bool
a:t
(a0 + 2 * a).[0] == a0
 rewrite testbit_spec'.a0:bool
a:t
((a0 + 2 * a) / 2 ^ 0) mod 2 == a0 nzsimpl.a0:bool
a:t
(a0 + 2 * a) mod 2 == a0 rewrite mul_comm, mod_add by order'.a0:bool
a:t
a0 mod 2 == a0
 now rewrite mod_small by (destruct a0; order').
Qed.

Lemma b2n_div2 : forall (a0:bool), a0/2 == 0.forall a0 : bool, a0 / 2 == 0
Proof.forall a0 : bool, a0 / 2 == 0
 intros a0.a0:bool
a0 / 2 == 0 rewrite <- (add_b2n_double_div2 a0 0).a0:bool
a0 / 2 == (a0 + 2 * 0) / 2 now nzsimpl.
Qed.

Lemma b2n_bit0 : forall (a0:bool), a0.[0] = a0.forall a0 : bool, a0.[0] = a0
Proof.forall a0 : bool, a0.[0] = a0
 intros a0.a0:bool
a0.[0] = a0 rewrite <- (add_b2n_double_bit0 a0 0) at 2.a0:bool
a0.[0] = (a0 + 2 * 0).[0] now nzsimpl.
Qed.

The specification of testbit by low and high parts is complete

Lemma testbit_unique : forall a n (a0:bool) l h,
 l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0.forall (a n : t) (a0 : bool) (l h : t),
l < 2 ^ n ->
a == l + (a0 + 2 * h) * 2 ^ n -> a.[n] = a0
Proof.forall (a n : t) (a0 : bool) (l h : t),
l < 2 ^ n ->
a == l + (a0 + 2 * h) * 2 ^ n -> a.[n] = a0
 intros a n a0 l h Hl EQ.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
a.[n] = a0
 apply b2n_inj.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
a.[n] == a0 rewrite testbit_spec' by trivial.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
(a / 2 ^ n) mod 2 == a0
 symmetry.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
a0 == (a / 2 ^ n) mod 2 apply mod_unique with h.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
a0 < 2
a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
a / 2 ^ n == 2 * h + a0 destruct a0; simpl; order'.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
a / 2 ^ n == 2 * h + a0
 symmetry.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
2 * h + a0 == a / 2 ^ n apply div_unique with l; trivial.a, n:t
a0:bool
l, h:t
Hl:l < 2 ^ n
EQ:a == l + (a0 + 2 * h) * 2 ^ n
a == 2 ^ n * (2 * h + a0) + l
 now rewrite add_comm, (add_comm _ a0), mul_comm.
Qed.

All bits of number 0 are 0

Lemma bits_0 : forall n, 0.[n] = false.forall n : t, 0.[n] = false
Proof.forall n : t, 0.[n] = false
 intros n.n:t
0.[n] = false apply testbit_false.n:t
(0 / 2 ^ n) mod 2 == 0 nzsimpl; order_nz.
Qed.

Various ways to refer to the lowest bit of a number

Lemma bit0_odd : forall a, a.[0] = odd a.forall a : t, a.[0] = odd a
Proof.forall a : t, a.[0] = odd a
 intros.a:t
a.[0] = odd a symmetry.a:t
odd a = a.[0]
 destruct (exists_div2 a) as (a' & b & EQ).a, a':t
b:bool
EQ:a == 2 * a' + b
odd a = a.[0]
 rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2.a, a':t
b:bool
EQ:a == 2 * a' + b
odd b = b
 destruct b; simpl; apply odd_1 || apply odd_0.
Qed.

Lemma bit0_eqb : forall a, a.[0] = eqb (a mod 2) 1.forall a : t, a.[0] = (a mod 2 =? 1)
Proof.forall a : t, a.[0] = (a mod 2 =? 1)
 intros a.a:t
a.[0] = (a mod 2 =? 1) rewrite testbit_eqb.a:t
((a / 2 ^ 0) mod 2 =? 1) = (a mod 2 =? 1) now nzsimpl.
Qed.

Lemma bit0_mod : forall a, a.[0] == a mod 2.forall a : t, a.[0] == a mod 2
Proof.forall a : t, a.[0] == a mod 2
 intros a.a:t
a.[0] == a mod 2 rewrite testbit_spec'.a:t
(a / 2 ^ 0) mod 2 == a mod 2 now nzsimpl.
Qed.

Hence testing a bit is equivalent to shifting and testing parity

Lemma testbit_odd : forall a n, a.[n] = odd (a>>n).forall a n : t, a.[n] = odd (a >> n)
Proof.forall a n : t, a.[n] = odd (a >> n)
 intros.a, n:t
a.[n] = odd (a >> n) now rewrite <- bit0_odd, shiftr_spec, add_0_l.
Qed.

log2 gives the highest nonzero bit

Lemma bit_log2 : forall a, a~=0 -> a.[log2 a] = true.forall a : t, a ~= 0 -> a.[log2 a] = true
Proof.forall a : t, a ~= 0 -> a.[log2 a] = true
 intros a Ha.a:t
Ha:a ~= 0
a.[log2 a] = true
 assert (Ha' : 0 < a) by (generalize (le_0_l a); order).a:t
Ha:a ~= 0
Ha':0 < a
a.[log2 a] = true
 destruct (log2_spec_alt a Ha') as (r & EQ & (_,Hr)).a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
a.[log2 a] = true
 rewrite EQ at 1.a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
(2 ^ log2 a + r).[log2 a] = true
 rewrite testbit_true, add_comm.a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
((r + 2 ^ log2 a) / 2 ^ log2 a) mod 2 == 1
 rewrite <- (mul_1_l (2^log2 a)) at 1.a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
((r + 1 * 2 ^ log2 a) / 2 ^ log2 a) mod 2 == 1
 rewrite div_add by order_nz.a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
(r / 2 ^ log2 a + 1) mod 2 == 1
 rewrite div_small by trivial.a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
(0 + 1) mod 2 == 1
 rewrite add_0_l.a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
1 mod 2 == 1 apply mod_small.a:t
Ha:a ~= 0
Ha':0 < a
r:t
EQ:a == 2 ^ log2 a + r
Hr:r < 2 ^ log2 a
1 < 2 order'.
Qed.

Lemma bits_above_log2 : forall a n, log2 a < n ->
 a.[n] = false.forall a n : t, log2 a < n -> a.[n] = false
Proof.forall a n : t, log2 a < n -> a.[n] = false
 intros a n H.a, n:t
H:log2 a < n
a.[n] = false
 rewrite testbit_false.a, n:t
H:log2 a < n
(a / 2 ^ n) mod 2 == 0
 rewrite div_small.a, n:t
H:log2 a < n
0 mod 2 == 0
a, n:t
H:log2 a < n
a < 2 ^ n nzsimpl; order'.a, n:t
H:log2 a < n
a < 2 ^ n
 apply log2_lt_cancel.a, n:t
H:log2 a < n
log2 a < log2 (2 ^ n) rewrite log2_pow2; trivial using le_0_l.
Qed.

Hence the number of bits of a is 1+log2 a (see Pos.size_nat and Pos.size).

Testing bits after division or multiplication by a power of two

Lemma div2_bits : forall a n, (a/2).[n] = a.[S n].forall a n : t, (a / 2).[n] = a.[S n]
Proof.forall a n : t, (a / 2).[n] = a.[S n]
 intros.a, n:t
(a / 2).[n] = a.[S n] apply eq_true_iff_eq.a, n:t
(a / 2).[n] = true <-> a.[S n] = true
 rewrite 2 testbit_true.a, n:t
(a / 2 / 2 ^ n) mod 2 == 1 <->
(a / 2 ^ S n) mod 2 == 1
 rewrite pow_succ_r by apply le_0_l.a, n:t
(a / 2 / 2 ^ n) mod 2 == 1 <->
(a / (2 * 2 ^ n)) mod 2 == 1
 now rewrite div_div by order_nz.
Qed.

Lemma div_pow2_bits : forall a n m, (a/2^n).[m] = a.[m+n].forall a n m : t, (a / 2 ^ n).[m] = a.[m + n]
Proof.forall a n m : t, (a / 2 ^ n).[m] = a.[m + n]
 intros a n.a, n:t
forall m : t, (a / 2 ^ n).[m] = a.[m + n] revert a.n:t
forall a m : t, (a / 2 ^ n).[m] = a.[m + n] induct n.forall a m : t, (a / 2 ^ 0).[m] = a.[m + 0]
forall n : t,
(forall a m : t, (a / 2 ^ n).[m] = a.[m + n]) ->
forall a m : t, (a / 2 ^ S n).[m] = a.[m + S n]
 intros a m.a, m:t
(a / 2 ^ 0).[m] = a.[m + 0]
forall n : t,
(forall a m : t, (a / 2 ^ n).[m] = a.[m + n]) ->
forall a m : t, (a / 2 ^ S n).[m] = a.[m + S n] now nzsimpl.forall n : t,
(forall a m : t, (a / 2 ^ n).[m] = a.[m + n]) ->
forall a m : t, (a / 2 ^ S n).[m] = a.[m + S n]
 intros n IH a m.n:t
IH:forall a0 m0 : t, (a0 / 2 ^ n).[m0] = a0.[m0 + n]
a, m:t
(a / 2 ^ S n).[m] = a.[m + S n] nzsimpl; try apply le_0_l.n:t
IH:forall a0 m0 : t, (a0 / 2 ^ n).[m0] = a0.[m0 + n]
a, m:t
(a / (2 * 2 ^ n)).[m] = a.[S (m + n)]
 rewrite <- div_div by order_nz.n:t
IH:forall a0 m0 : t, (a0 / 2 ^ n).[m0] = a0.[m0 + n]
a, m:t
(a / 2 / 2 ^ n).[m] = a.[S (m + n)]
 now rewrite IH, div2_bits.
Qed.

Lemma double_bits_succ : forall a n, (2*a).[S n] = a.[n].forall a n : t, (2 * a).[S n] = a.[n]
Proof.forall a n : t, (2 * a).[S n] = a.[n]
 intros.a, n:t
(2 * a).[S n] = a.[n] rewrite <- div2_bits.a, n:t
(2 * a / 2).[n] = a.[n] now rewrite mul_comm, div_mul by order'.
Qed.

Lemma mul_pow2_bits_add : forall a n m, (a*2^n).[m+n] = a.[m].forall a n m : t, (a * 2 ^ n).[m + n] = a.[m]
Proof.forall a n m : t, (a * 2 ^ n).[m + n] = a.[m]
 intros.a, n, m:t
(a * 2 ^ n).[m + n] = a.[m] rewrite <- div_pow2_bits.a, n, m:t
(a * 2 ^ n / 2 ^ n).[m] = a.[m] now rewrite div_mul by order_nz.
Qed.

Lemma mul_pow2_bits_high : forall a n m, n<=m -> (a*2^n).[m] = a.[m-n].forall a n m : t,
n <= m -> (a * 2 ^ n).[m] = a.[m - n]
Proof.forall a n m : t,
n <= m -> (a * 2 ^ n).[m] = a.[m - n]
 intros.a, n, m:t
H:n <= m
(a * 2 ^ n).[m] = a.[m - n]
 rewrite <- (sub_add n m) at 1 by order'.a, n, m:t
H:n <= m
(a * 2 ^ n).[m - n + n] = a.[m - n]
 now rewrite mul_pow2_bits_add.
Qed.

Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false.forall a n m : t, m < n -> (a * 2 ^ n).[m] = false
Proof.forall a n m : t, m < n -> (a * 2 ^ n).[m] = false
 intros.a, n, m:t
H:m < n
(a * 2 ^ n).[m] = false apply testbit_false.a, n, m:t
H:m < n
(a * 2 ^ n / 2 ^ m) mod 2 == 0
 rewrite <- (sub_add m n) by order'.a, n, m:t
H:m < n
(a * 2 ^ (n - m + m) / 2 ^ m) mod 2 == 0 rewrite pow_add_r, mul_assoc.a, n, m:t
H:m < n
(a * 2 ^ (n - m) * 2 ^ m / 2 ^ m) mod 2 == 0
 rewrite div_mul by order_nz.a, n, m:t
H:m < n
(a * 2 ^ (n - m)) mod 2 == 0
 rewrite <- (succ_pred (n-m)).a, n, m:t
H:m < n
(a * 2 ^ S (P (n - m))) mod 2 == 0
a, n, m:t
H:m < n
n - m ~= 0 rewrite pow_succ_r.a, n, m:t
H:m < n
(a * (2 * 2 ^ P (n - m))) mod 2 == 0
a, n, m:t
H:m < n
0 <= P (n - m)
a, n, m:t
H:m < n
n - m ~= 0
 now rewrite (mul_comm 2), mul_assoc, mod_mul by order'.a, n, m:t
H:m < n
0 <= P (n - m)
a, n, m:t
H:m < n
n - m ~= 0
 apply lt_le_pred.a, n, m:t
H:m < n
0 < n - m
a, n, m:t
H:m < n
n - m ~= 0
 apply sub_gt in H.a, n, m:t
H:n - m ~= 0
0 < n - m
a, n, m:t
H:m < n
n - m ~= 0 generalize (le_0_l (n-m)); order.a, n, m:t
H:m < n
n - m ~= 0
 now apply sub_gt.
Qed.

Selecting the low part of a number can be done by a modulo

Lemma mod_pow2_bits_high : forall a n m, n<=m ->
 (a mod 2^n).[m] = false.forall a n m : t, n <= m -> (a mod 2 ^ n).[m] = false
Proof.forall a n m : t, n <= m -> (a mod 2 ^ n).[m] = false
 intros a n m H.a, n, m:t
H:n <= m
(a mod 2 ^ n).[m] = false
 destruct (eq_0_gt_0_cases (a mod 2^n)) as [EQ|LT].a, n, m:t
H:n <= m
EQ:a mod 2 ^ n == 0
(a mod 2 ^ n).[m] = false
a, n, m:t
H:n <= m
LT:0 < a mod 2 ^ n
(a mod 2 ^ n).[m] = false
 now rewrite EQ, bits_0.a, n, m:t
H:n <= m
LT:0 < a mod 2 ^ n
(a mod 2 ^ n).[m] = false
 apply bits_above_log2.a, n, m:t
H:n <= m
LT:0 < a mod 2 ^ n
log2 (a mod 2 ^ n) < m
 apply lt_le_trans with n; trivial.a, n, m:t
H:n <= m
LT:0 < a mod 2 ^ n
log2 (a mod 2 ^ n) < n
 apply log2_lt_pow2; trivial.a, n, m:t
H:n <= m
LT:0 < a mod 2 ^ n
a mod 2 ^ n < 2 ^ n
 apply mod_upper_bound; order_nz.
Qed.

Lemma mod_pow2_bits_low : forall a n m, m<n ->
 (a mod 2^n).[m] = a.[m].forall a n m : t, m < n -> (a mod 2 ^ n).[m] = a.[m]
Proof.forall a n m : t, m < n -> (a mod 2 ^ n).[m] = a.[m]
 intros a n m H.a, n, m:t
H:m < n
(a mod 2 ^ n).[m] = a.[m]
 rewrite testbit_eqb.a, n, m:t
H:m < n
((a mod 2 ^ n / 2 ^ m) mod 2 =? 1) = a.[m]
 rewrite <- (mod_add _ (2^(P (n-m))*(a/2^n))) by order'.a, n, m:t
H:m < n
((a mod 2 ^ n / 2 ^ m +
  2 ^ P (n - m) * (a / 2 ^ n) * 2) mod 2 =? 1) = a.[m]
 rewrite <- div_add by order_nz.a, n, m:t
H:m < n
(((a mod 2 ^ n +
   2 ^ P (n - m) * (a / 2 ^ n) * 2 * 2 ^ m) / 2 ^ m)
 mod 2 =? 1) = a.[m]
 rewrite (mul_comm _ 2), mul_assoc, <- pow_succ_r', succ_pred
   by now apply sub_gt.a, n, m:t
H:m < n
(((a mod 2 ^ n + 2 ^ (n - m) * (a / 2 ^ n) * 2 ^ m) /
  2 ^ m) mod 2 =? 1) = a.[m]
 rewrite mul_comm, mul_assoc, <- pow_add_r, (add_comm m), sub_add
   by order.a, n, m:t
H:m < n
(((a mod 2 ^ n + 2 ^ n * (a / 2 ^ n)) / 2 ^ m) mod 2 =?
 1) = a.[m]
 rewrite add_comm, <- div_mod by order_nz.a, n, m:t
H:m < n
((a / 2 ^ m) mod 2 =? 1) = a.[m]
 symmetry.a, n, m:t
H:m < n
a.[m] = ((a / 2 ^ m) mod 2 =? 1) apply testbit_eqb.
Qed.

We now prove that having the same bits implies equality. For that we use a notion of equality over functional streams of bits.

Definition eqf (f g:t -> bool) := forall n:t, f n = g n.

Instance eqf_equiv : Equivalence eqf.Equivalence eqf
Proof.Equivalence eqf
 split; congruence.
Qed.

Local Infix "===" := eqf (at level 70, no associativity).

Instance testbit_eqf : Proper (eq==>eqf) testbit.Proper (eq ==> eqf) testbit
Proof.Proper (eq ==> eqf) testbit
 intros a a' Ha n.a, a':t
Ha:a == a'
n:t
a.[n] = a'.[n] now rewrite Ha.
Qed.

Only zero corresponds to the always-false stream.

Lemma bits_inj_0 :
 forall a, (forall n, a.[n] = false) -> a == 0.forall a : t, (forall n : t, a.[n] = false) -> a == 0
Proof.forall a : t, (forall n : t, a.[n] = false) -> a == 0
 intros a H.a:t
H:forall n : t, a.[n] = false
a == 0 destruct (eq_decidable a 0) as [EQ|NEQ]; trivial.a:t
H:forall n : t, a.[n] = false
NEQ:a ~= 0
a == 0
 apply bit_log2 in NEQ.a:t
H:forall n : t, a.[n] = false
NEQ:a.[log2 a] = true
a == 0 now rewrite H in NEQ.
Qed.

If two numbers produce the same stream of bits, they are equal.

Lemma bits_inj : forall a b, testbit a === testbit b -> a == b.forall a b : t, testbit a === testbit b -> a == b
Proof.forall a b : t, testbit a === testbit b -> a == b
 intros a.a:t
forall b : t, testbit a === testbit b -> a == b pattern a.a:t
(fun t0 : t =>
 forall b : t, testbit t0 === testbit b -> t0 == b) a
 apply strong_right_induction with 0;[solve_proper|clear a|apply le_0_l].forall n : t,
0 <= n ->
(forall m : t,
 0 <= m ->
 m < n ->
 forall b : t, testbit m === testbit b -> m == b) ->
forall b : t, testbit n === testbit b -> n == b
 intros a _ IH b H.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
a == b
 destruct (eq_0_gt_0_cases a) as [EQ|LT].a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
EQ:a == 0
a == b
a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a == b
 rewrite EQ in H |- *.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit 0 === testbit b
EQ:a == 0
0 == b
a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a == b symmetry.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit 0 === testbit b
EQ:a == 0
b == 0
a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a == b apply bits_inj_0.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit 0 === testbit b
EQ:a == 0
forall n : t, b.[n] = false
a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a == b
 intros n.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit 0 === testbit b
EQ:a == 0
n:t
b.[n] = false
a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a == b now rewrite <- H, bits_0.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a == b
 rewrite (div_mod a 2), (div_mod b 2) by order'.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
2 * (a / 2) + a mod 2 == 2 * (b / 2) + b mod 2
 f_equiv; [ | now rewrite <- 2 bit0_mod, H].a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
2 * (a / 2) == 2 * (b / 2)
 f_equiv.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a / 2 == b / 2
 apply IH; trivial using le_0_l.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
a / 2 < a
a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
testbit (a / 2) === testbit (b / 2)
 apply div_lt; order'.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
testbit (a / 2) === testbit (b / 2)
 intro n.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
n:t
(a / 2).[n] = (b / 2).[n] rewrite 2 div2_bits.a:t
IH:forall m : t,
0 <= m ->
m < a ->
forall b0 : t,
testbit m === testbit b0 -> m == b0
b:t
H:testbit a === testbit b
LT:0 < a
n:t
a.[S n] = b.[S n] apply H.
Qed.

Lemma bits_inj_iff : forall a b, testbit a === testbit b <-> a == b.forall a b : t, testbit a === testbit b <-> a == b
Proof.forall a b : t, testbit a === testbit b <-> a == b
 split.a, b:t
testbit a === testbit b -> a == b
a, b:t
a == b -> testbit a === testbit b apply bits_inj.a, b:t
a == b -> testbit a === testbit b intros EQ; now rewrite EQ.
Qed.

Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.

Ltac bitwise := apply bits_inj; intros ?m; autorewrite with bitwise.

The streams of bits that correspond to a natural numbers are exactly the ones that are always 0 after some point

Lemma are_bits : forall (f:t->bool), Proper (eq==>Logic.eq) f ->
 ((exists n, f === testbit n) <->
  (exists k, forall m, k<=m -> f m = false)).forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(exists n : t, f === testbit n) <->
(exists k : t, forall m : t, k <= m -> f m = false)
Proof.forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(exists n : t, f === testbit n) <->
(exists k : t, forall m : t, k <= m -> f m = false)
 intros f Hf.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists n : t, f === testbit n) <->
(exists k : t, forall m : t, k <= m -> f m = false) split.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists n : t, f === testbit n) ->
exists k : t, forall m : t, k <= m -> f m = false
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists k : t, forall m : t, k <= m -> f m = false) ->
exists n : t, f === testbit n
 intros (a,H).f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
a:t
H:f === testbit a
exists k : t, forall m : t, k <= m -> f m = false
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists k : t, forall m : t, k <= m -> f m = false) ->
exists n : t, f === testbit n
  exists (S (log2 a)).f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
a:t
H:f === testbit a
forall m : t, S (log2 a) <= m -> f m = false
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists k : t, forall m : t, k <= m -> f m = false) ->
exists n : t, f === testbit n intros m Hm.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
a:t
H:f === testbit a
m:t
Hm:S (log2 a) <= m
f m = false
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists k : t, forall m : t, k <= m -> f m = false) ->
exists n : t, f === testbit n apply le_succ_l in Hm.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
a:t
H:f === testbit a
m:t
Hm:log2 a < m
f m = false
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists k : t, forall m : t, k <= m -> f m = false) ->
exists n : t, f === testbit n
  rewrite H, bits_above_log2; trivial using lt_succ_diag_r.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
(exists k : t, forall m : t, k <= m -> f m = false) ->
exists n : t, f === testbit n
 intros (k,Hk).f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
k:t
Hk:forall m : t, k <= m -> f m = false
exists n : t, f === testbit n
  revert f Hf Hk.k:t
forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, k <= m -> f m = false) ->
exists n : t, f === testbit n induct k.forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, 0 <= m -> f m = false) ->
exists n : t, f === testbit n
forall n : t,
(forall f : t -> bool,
 Proper (eq ==> Logic.eq) f ->
 (forall m : t, n <= m -> f m = false) ->
 exists n0 : t, f === testbit n0) ->
forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, S n <= m -> f m = false) ->
exists n0 : t, f === testbit n0
  intros f Hf H0.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
H0:forall m : t, 0 <= m -> f m = false
exists n : t, f === testbit n
forall n : t,
(forall f : t -> bool,
 Proper (eq ==> Logic.eq) f ->
 (forall m : t, n <= m -> f m = false) ->
 exists n0 : t, f === testbit n0) ->
forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, S n <= m -> f m = false) ->
exists n0 : t, f === testbit n0
  exists 0.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
H0:forall m : t, 0 <= m -> f m = false
f === testbit 0
forall n : t,
(forall f : t -> bool,
 Proper (eq ==> Logic.eq) f ->
 (forall m : t, n <= m -> f m = false) ->
 exists n0 : t, f === testbit n0) ->
forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, S n <= m -> f m = false) ->
exists n0 : t, f === testbit n0 intros m.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
H0:forall m0 : t, 0 <= m0 -> f m0 = false
m:t
f m = 0.[m]
forall n : t,
(forall f : t -> bool,
 Proper (eq ==> Logic.eq) f ->
 (forall m : t, n <= m -> f m = false) ->
 exists n0 : t, f === testbit n0) ->
forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, S n <= m -> f m = false) ->
exists n0 : t, f === testbit n0 rewrite bits_0, H0; trivial.f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
H0:forall m0 : t, 0 <= m0 -> f m0 = false
m:t
0 <= m
forall n : t,
(forall f : t -> bool,
 Proper (eq ==> Logic.eq) f ->
 (forall m : t, n <= m -> f m = false) ->
 exists n0 : t, f === testbit n0) ->
forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, S n <= m -> f m = false) ->
exists n0 : t, f === testbit n0 apply le_0_l.forall n : t,
(forall f : t -> bool,
 Proper (eq ==> Logic.eq) f ->
 (forall m : t, n <= m -> f m = false) ->
 exists n0 : t, f === testbit n0) ->
forall f : t -> bool,
Proper (eq ==> Logic.eq) f ->
(forall m : t, S n <= m -> f m = false) ->
exists n0 : t, f === testbit n0
  intros k IH f Hf Hk.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n : t, f0 === testbit n
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
exists n : t, f === testbit n
  destruct (IH (fun m => f (S m))) as (n, Hn).k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n : t, f0 === testbit n
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
Proper (eq ==> Logic.eq) (fun m : t => f (S m))
k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n : t, f0 === testbit n
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
forall m : t, k <= m -> f (S m) = false
k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
n:t
Hn:(fun m : t => f (S m)) === testbit n
exists n0 : t, f === testbit n0
  solve_proper.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n : t, f0 === testbit n
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
forall m : t, k <= m -> f (S m) = false
k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
n:t
Hn:(fun m : t => f (S m)) === testbit n
exists n0 : t, f === testbit n0
  intros m Hm.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n : t, f0 === testbit n
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
m:t
Hm:k <= m
f (S m) = false
k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
n:t
Hn:(fun m : t => f (S m)) === testbit n
exists n0 : t, f === testbit n0 apply Hk.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n : t, f0 === testbit n
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
m:t
Hm:k <= m
S k <= S m
k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
n:t
Hn:(fun m : t => f (S m)) === testbit n
exists n0 : t, f === testbit n0 now rewrite <- succ_le_mono.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
n:t
Hn:(fun m : t => f (S m)) === testbit n
exists n0 : t, f === testbit n0
  exists (f 0 + 2*n).k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m : t, k <= m -> f0 m = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m : t, S k <= m -> f m = false
n:t
Hn:(fun m : t => f (S m)) === testbit n
f === testbit (f 0 + 2 * n) intros m.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m:t
f m = (f 0 + 2 * n).[m]
  destruct (zero_or_succ m) as [Hm|(m', Hm)]; rewrite Hm.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m:t
Hm:m == 0
f 0 = (f 0 + 2 * n).[0]
k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m, m':t
Hm:m == S m'
f (S m') = (f 0 + 2 * n).[S m']
  symmetry.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m:t
Hm:m == 0
(f 0 + 2 * n).[0] = f 0
k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m, m':t
Hm:m == S m'
f (S m') = (f 0 + 2 * n).[S m'] apply add_b2n_double_bit0.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m, m':t
Hm:m == S m'
f (S m') = (f 0 + 2 * n).[S m']
  rewrite Hn, <- div2_bits.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m, m':t
Hm:m == S m'
n.[m'] = ((f 0 + 2 * n) / 2).[m']
  rewrite mul_comm, div_add, b2n_div2, add_0_l; trivial.k:t
IH:forall f0 : t -> bool,
Proper (eq ==> Logic.eq) f0 ->
(forall m0 : t, k <= m0 -> f0 m0 = false) ->
exists n0 : t, f0 === testbit n0
f:t -> bool
Hf:Proper (eq ==> Logic.eq) f
Hk:forall m0 : t, S k <= m0 -> f m0 = false
n:t
Hn:(fun m0 : t => f (S m0)) === testbit n
m, m':t
Hm:m == S m'
2 ~= 0 order'.
Qed.

Properties of shifts

Lemma shiftr_spec' : forall a n m, (a >> n).[m] = a.[m+n].forall a n m : t, (a >> n).[m] = a.[m + n]
Proof.forall a n m : t, (a >> n).[m] = a.[m + n]
 intros.a, n, m:t
(a >> n).[m] = a.[m + n] apply shiftr_spec.a, n, m:t
0 <= m apply le_0_l.
Qed.

Lemma shiftl_spec_high' : forall a n m, n<=m -> (a << n).[m] = a.[m-n].forall a n m : t, n <= m -> (a << n).[m] = a.[m - n]
Proof.forall a n m : t, n <= m -> (a << n).[m] = a.[m - n]
 intros.a, n, m:t
H:n <= m
(a << n).[m] = a.[m - n] apply shiftl_spec_high; trivial.a, n, m:t
H:n <= m
0 <= m apply le_0_l.
Qed.

Lemma shiftr_div_pow2 : forall a n, a >> n == a / 2^n.forall a n : t, a >> n == a / 2 ^ n
Proof.forall a n : t, a >> n == a / 2 ^ n
 intros.a, n:t
a >> n == a / 2 ^ n bitwise.a, n, m:t
(a >> n).[m] = (a / 2 ^ n).[m] rewrite shiftr_spec'.a, n, m:t
a.[m + n] = (a / 2 ^ n).[m]
 symmetry.a, n, m:t
(a / 2 ^ n).[m] = a.[m + n] apply div_pow2_bits.
Qed.

Lemma shiftl_mul_pow2 : forall a n, a << n == a * 2^n.forall a n : t, a << n == a * 2 ^ n
Proof.forall a n : t, a << n == a * 2 ^ n
 intros.a, n:t
a << n == a * 2 ^ n bitwise.a, n, m:t
(a << n).[m] = (a * 2 ^ n).[m]
 destruct (le_gt_cases n m) as [H|H].a, n, m:t
H:n <= m
(a << n).[m] = (a * 2 ^ n).[m]
a, n, m:t
H:m < n
(a << n).[m] = (a * 2 ^ n).[m]
 now rewrite shiftl_spec_high', mul_pow2_bits_high.a, n, m:t
H:m < n
(a << n).[m] = (a * 2 ^ n).[m]
 now rewrite shiftl_spec_low, mul_pow2_bits_low.
Qed.

Lemma shiftl_spec_alt : forall a n m, (a << n).[m+n] = a.[m].forall a n m : t, (a << n).[m + n] = a.[m]
Proof.forall a n m : t, (a << n).[m + n] = a.[m]
 intros.a, n, m:t
(a << n).[m + n] = a.[m] now rewrite shiftl_mul_pow2, mul_pow2_bits_add.
Qed.

Instance shiftr_wd : Proper (eq==>eq==>eq) shiftr.Proper (eq ==> eq ==> eq) shiftr
Proof.Proper (eq ==> eq ==> eq) shiftr
 intros a a' Ha b b' Hb.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
a >> b == a' >> b' now rewrite 2 shiftr_div_pow2, Ha, Hb.
Qed.

Instance shiftl_wd : Proper (eq==>eq==>eq) shiftl.Proper (eq ==> eq ==> eq) shiftl
Proof.Proper (eq ==> eq ==> eq) shiftl
 intros a a' Ha b b' Hb.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
a << b == a' << b' now rewrite 2 shiftl_mul_pow2, Ha, Hb.
Qed.

Lemma shiftl_shiftl : forall a n m,
 (a << n) << m == a << (n+m).forall a n m : t, (a << n) << m == a << (n + m)
Proof.forall a n m : t, (a << n) << m == a << (n + m)
 intros.a, n, m:t
(a << n) << m == a << (n + m) now rewrite !shiftl_mul_pow2, pow_add_r, mul_assoc.
Qed.

Lemma shiftr_shiftr : forall a n m,
 (a >> n) >> m == a >> (n+m).forall a n m : t, (a >> n) >> m == a >> (n + m)
Proof.forall a n m : t, (a >> n) >> m == a >> (n + m)
 intros.a, n, m:t
(a >> n) >> m == a >> (n + m)
 now rewrite !shiftr_div_pow2, pow_add_r, div_div by order_nz.
Qed.

Lemma shiftr_shiftl_l : forall a n m, m<=n ->
 (a << n) >> m == a << (n-m).forall a n m : t,
m <= n -> (a << n) >> m == a << (n - m)
Proof.forall a n m : t,
m <= n -> (a << n) >> m == a << (n - m)
 intros.a, n, m:t
H:m <= n
(a << n) >> m == a << (n - m)
 rewrite shiftr_div_pow2, !shiftl_mul_pow2.a, n, m:t
H:m <= n
a * 2 ^ n / 2 ^ m == a * 2 ^ (n - m)
 rewrite <- (sub_add m n) at 1 by trivial.a, n, m:t
H:m <= n
a * 2 ^ (n - m + m) / 2 ^ m == a * 2 ^ (n - m)
 now rewrite pow_add_r, mul_assoc, div_mul by order_nz.
Qed.

Lemma shiftr_shiftl_r : forall a n m, n<=m ->
 (a << n) >> m == a >> (m-n).forall a n m : t,
n <= m -> (a << n) >> m == a >> (m - n)
Proof.forall a n m : t,
n <= m -> (a << n) >> m == a >> (m - n)
 intros.a, n, m:t
H:n <= m
(a << n) >> m == a >> (m - n)
 rewrite !shiftr_div_pow2, shiftl_mul_pow2.a, n, m:t
H:n <= m
a * 2 ^ n / 2 ^ m == a / 2 ^ (m - n)
 rewrite <- (sub_add n m) at 1 by trivial.a, n, m:t
H:n <= m
a * 2 ^ n / 2 ^ (m - n + n) == a / 2 ^ (m - n)
 rewrite pow_add_r, (mul_comm (2^(m-n))).a, n, m:t
H:n <= m
a * 2 ^ n / (2 ^ n * 2 ^ (m - n)) == a / 2 ^ (m - n)
 now rewrite <- div_div, div_mul by order_nz.
Qed.

shifts and constants

Lemma shiftl_1_l : forall n, 1 << n == 2^n.forall n : t, 1 << n == 2 ^ n
Proof.forall n : t, 1 << n == 2 ^ n
 intros.n:t
1 << n == 2 ^ n now rewrite shiftl_mul_pow2, mul_1_l.
Qed.

Lemma shiftl_0_r : forall a, a << 0 == a.forall a : t, a << 0 == a
Proof.forall a : t, a << 0 == a
 intros.a:t
a << 0 == a rewrite shiftl_mul_pow2.a:t
a * 2 ^ 0 == a now nzsimpl.
Qed.

Lemma shiftr_0_r : forall a, a >> 0 == a.forall a : t, a >> 0 == a
Proof.forall a : t, a >> 0 == a
 intros.a:t
a >> 0 == a rewrite shiftr_div_pow2.a:t
a / 2 ^ 0 == a now nzsimpl.
Qed.

Lemma shiftl_0_l : forall n, 0 << n == 0.forall n : t, 0 << n == 0
Proof.forall n : t, 0 << n == 0
 intros.n:t
0 << n == 0 rewrite shiftl_mul_pow2.n:t
0 * 2 ^ n == 0 now nzsimpl.
Qed.

Lemma shiftr_0_l : forall n, 0 >> n == 0.forall n : t, 0 >> n == 0
Proof.forall n : t, 0 >> n == 0
 intros.n:t
0 >> n == 0 rewrite shiftr_div_pow2.n:t
0 / 2 ^ n == 0 nzsimpl; order_nz.
Qed.

Lemma shiftl_eq_0_iff : forall a n, a << n == 0 <-> a == 0.forall a n : t, a << n == 0 <-> a == 0
Proof.forall a n : t, a << n == 0 <-> a == 0
 intros a n.a, n:t
a << n == 0 <-> a == 0 rewrite shiftl_mul_pow2.a, n:t
a * 2 ^ n == 0 <-> a == 0 rewrite eq_mul_0.a, n:t
a == 0 \/ 2 ^ n == 0 <-> a == 0 split.a, n:t
a == 0 \/ 2 ^ n == 0 -> a == 0
a, n:t
a == 0 -> a == 0 \/ 2 ^ n == 0
 intros [H | H]; trivial.a, n:t
H:2 ^ n == 0
a == 0
a, n:t
a == 0 -> a == 0 \/ 2 ^ n == 0 contradict H; order_nz.a, n:t
a == 0 -> a == 0 \/ 2 ^ n == 0
 intros H.a, n:t
H:a == 0
a == 0 \/ 2 ^ n == 0 now left.
Qed.

Lemma shiftr_eq_0_iff : forall a n,
 a >> n == 0 <-> a==0 \/ (0<a /\ log2 a < n).forall a n : t,
a >> n == 0 <-> a == 0 \/ 0 < a /\ log2 a < n
Proof.forall a n : t,
a >> n == 0 <-> a == 0 \/ 0 < a /\ log2 a < n
 intros a n.a, n:t
a >> n == 0 <-> a == 0 \/ 0 < a /\ log2 a < n
 rewrite shiftr_div_pow2, div_small_iff by order_nz.a, n:t
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n
 destruct (eq_0_gt_0_cases a) as [EQ|LT].a, n:t
EQ:a == 0
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n
a, n:t
LT:0 < a
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n
 rewrite EQ.a, n:t
EQ:a == 0
0 < 2 ^ n <-> 0 == 0 \/ 0 < 0 /\ log2 0 < n
a, n:t
LT:0 < a
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n split.a, n:t
EQ:a == 0
0 < 2 ^ n -> 0 == 0 \/ 0 < 0 /\ log2 0 < n
a, n:t
EQ:a == 0
0 == 0 \/ 0 < 0 /\ log2 0 < n -> 0 < 2 ^ n
a, n:t
LT:0 < a
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n now left.a, n:t
EQ:a == 0
0 == 0 \/ 0 < 0 /\ log2 0 < n -> 0 < 2 ^ n
a, n:t
LT:0 < a
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n intros _.a, n:t
EQ:a == 0
0 < 2 ^ n
a, n:t
LT:0 < a
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n
  assert (H : 2~=0) by order'.a, n:t
EQ:a == 0
H:2 ~= 0
0 < 2 ^ n
a, n:t
LT:0 < a
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n
  generalize (pow_nonzero 2 n H) (le_0_l (2^n)); order.a, n:t
LT:0 < a
a < 2 ^ n <-> a == 0 \/ 0 < a /\ log2 a < n
 rewrite log2_lt_pow2; trivial.a, n:t
LT:0 < a
log2 a < n <-> a == 0 \/ 0 < a /\ log2 a < n
 split.a, n:t
LT:0 < a
log2 a < n -> a == 0 \/ 0 < a /\ log2 a < n
a, n:t
LT:0 < a
a == 0 \/ 0 < a /\ log2 a < n -> log2 a < n right; split; trivial.a, n:t
LT:0 < a
a == 0 \/ 0 < a /\ log2 a < n -> log2 a < n intros [H|[_ H]]; now order.
Qed.

Lemma shiftr_eq_0 : forall a n, log2 a < n -> a >> n == 0.forall a n : t, log2 a < n -> a >> n == 0
Proof.forall a n : t, log2 a < n -> a >> n == 0
 intros a n H.a, n:t
H:log2 a < n
a >> n == 0 rewrite shiftr_eq_0_iff.a, n:t
H:log2 a < n
a == 0 \/ 0 < a /\ log2 a < n
 destruct (eq_0_gt_0_cases a) as [EQ|LT].a, n:t
H:log2 a < n
EQ:a == 0
a == 0 \/ 0 < a /\ log2 a < n
a, n:t
H:log2 a < n
LT:0 < a
a == 0 \/ 0 < a /\ log2 a < n now left.a, n:t
H:log2 a < n
LT:0 < a
a == 0 \/ 0 < a /\ log2 a < n right; now split.
Qed.

Properties of div2.

Lemma div2_div : forall a, div2 a == a/2.forall a : t, div2 a == a / 2
Proof.forall a : t, div2 a == a / 2
 intros.a:t
div2 a == a / 2 rewrite div2_spec, shiftr_div_pow2.a:t
a / 2 ^ 1 == a / 2 now nzsimpl.
Qed.

Instance div2_wd : Proper (eq==>eq) div2.Proper (eq ==> eq) div2
Proof.Proper (eq ==> eq) div2
 intros a a' Ha.a, a':t
Ha:a == a'
div2 a == div2 a' now rewrite 2 div2_div, Ha.
Qed.

Lemma div2_odd : forall a, a == 2*(div2 a) + odd a.forall a : t, a == 2 * div2 a + odd a
Proof.forall a : t, a == 2 * div2 a + odd a
 intros a.a:t
a == 2 * div2 a + odd a rewrite div2_div, <- bit0_odd, bit0_mod.a:t
a == 2 * (a / 2) + a mod 2
 apply div_mod.a:t
2 ~= 0 order'.
Qed.

Properties of lxor and others, directly deduced from properties of xorb and others.

Instance lxor_wd : Proper (eq ==> eq ==> eq) lxor.Proper (eq ==> eq ==> eq) lxor
Proof.Proper (eq ==> eq ==> eq) lxor
 intros a a' Ha b b' Hb.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
lxor a b == lxor a' b' bitwise.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
m:t
xorb a.[m] b.[m] = xorb a'.[m] b'.[m] now rewrite Ha, Hb.
Qed.

Instance land_wd : Proper (eq ==> eq ==> eq) land.Proper (eq ==> eq ==> eq) land
Proof.Proper (eq ==> eq ==> eq) land
 intros a a' Ha b b' Hb.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
land a b == land a' b' bitwise.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
m:t
a.[m] && b.[m] = a'.[m] && b'.[m] now rewrite Ha, Hb.
Qed.

Instance lor_wd : Proper (eq ==> eq ==> eq) lor.Proper (eq ==> eq ==> eq) lor
Proof.Proper (eq ==> eq ==> eq) lor
 intros a a' Ha b b' Hb.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
lor a b == lor a' b' bitwise.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
m:t
a.[m] || b.[m] = a'.[m] || b'.[m] now rewrite Ha, Hb.
Qed.

Instance ldiff_wd : Proper (eq ==> eq ==> eq) ldiff.Proper (eq ==> eq ==> eq) ldiff
Proof.Proper (eq ==> eq ==> eq) ldiff
 intros a a' Ha b b' Hb.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
ldiff a b == ldiff a' b' bitwise.a, a':t
Ha:a == a'
b, b':t
Hb:b == b'
m:t
a.[m] && negb b.[m] = a'.[m] && negb b'.[m] now rewrite Ha, Hb.
Qed.

Lemma lxor_eq : forall a a', lxor a a' == 0 -> a == a'.forall a a' : t, lxor a a' == 0 -> a == a'
Proof.forall a a' : t, lxor a a' == 0 -> a == a'
 intros a a' H.a, a':t
H:lxor a a' == 0
a == a' bitwise.a, a':t
H:lxor a a' == 0
m:t
a.[m] = a'.[m] apply xorb_eq.a, a':t
H:lxor a a' == 0
m:t
xorb a.[m] a'.[m] = false
 now rewrite <- lxor_spec, H, bits_0.
Qed.

Lemma lxor_nilpotent : forall a, lxor a a == 0.forall a : t, lxor a a == 0
Proof.forall a : t, lxor a a == 0
 intros.a:t
lxor a a == 0 bitwise.a, m:t
xorb a.[m] a.[m] = false apply xorb_nilpotent.
Qed.

Lemma lxor_eq_0_iff : forall a a', lxor a a' == 0 <-> a == a'.forall a a' : t, lxor a a' == 0 <-> a == a'
Proof.forall a a' : t, lxor a a' == 0 <-> a == a'
 split.a, a':t
lxor a a' == 0 -> a == a'
a, a':t
a == a' -> lxor a a' == 0 apply lxor_eq.a, a':t
a == a' -> lxor a a' == 0 intros EQ; rewrite EQ; apply lxor_nilpotent.
Qed.

Lemma lxor_0_l : forall a, lxor 0 a == a.forall a : t, lxor 0 a == a
Proof.forall a : t, lxor 0 a == a
 intros.a:t
lxor 0 a == a bitwise.a, m:t
xorb false a.[m] = a.[m] apply xorb_false_l.
Qed.

Lemma lxor_0_r : forall a, lxor a 0 == a.forall a : t, lxor a 0 == a
Proof.forall a : t, lxor a 0 == a
 intros.a:t
lxor a 0 == a bitwise.a, m:t
xorb a.[m] false = a.[m] apply xorb_false_r.
Qed.

Lemma lxor_comm : forall a b, lxor a b == lxor b a.forall a b : t, lxor a b == lxor b a
Proof.forall a b : t, lxor a b == lxor b a
 intros.a, b:t
lxor a b == lxor b a bitwise.a, b, m:t
xorb a.[m] b.[m] = xorb b.[m] a.[m] apply xorb_comm.
Qed.

Lemma lxor_assoc :
 forall a b c, lxor (lxor a b) c == lxor a (lxor b c).forall a b c : t,
lxor (lxor a b) c == lxor a (lxor b c)
Proof.forall a b c : t,
lxor (lxor a b) c == lxor a (lxor b c)
 intros.a, b, c:t
lxor (lxor a b) c == lxor a (lxor b c) bitwise.a, b, c, m:t
xorb (xorb a.[m] b.[m]) c.[m] =
xorb a.[m] (xorb b.[m] c.[m]) apply xorb_assoc.
Qed.

Lemma lor_0_l : forall a, lor 0 a == a.forall a : t, lor 0 a == a
Proof.forall a : t, lor 0 a == a
 intros.a:t
lor 0 a == a bitwise.a, m:t
false || a.[m] = a.[m] trivial.
Qed.

Lemma lor_0_r : forall a, lor a 0 == a.forall a : t, lor a 0 == a
Proof.forall a : t, lor a 0 == a
 intros.a:t
lor a 0 == a bitwise.a, m:t
a.[m] || false = a.[m] apply orb_false_r.
Qed.

Lemma lor_comm : forall a b, lor a b == lor b a.forall a b : t, lor a b == lor b a
Proof.forall a b : t, lor a b == lor b a
 intros.a, b:t
lor a b == lor b a bitwise.a, b, m:t
a.[m] || b.[m] = b.[m] || a.[m] apply orb_comm.
Qed.

Lemma lor_assoc :
 forall a b c, lor a (lor b c) == lor (lor a b) c.forall a b c : t, lor a (lor b c) == lor (lor a b) c
Proof.forall a b c : t, lor a (lor b c) == lor (lor a b) c
 intros.a, b, c:t
lor a (lor b c) == lor (lor a b) c bitwise.a, b, c, m:t
a.[m] || (b.[m] || c.[m]) = a.[m] || b.[m] || c.[m] apply orb_assoc.
Qed.

Lemma lor_diag : forall a, lor a a == a.forall a : t, lor a a == a
Proof.forall a : t, lor a a == a
 intros.a:t
lor a a == a bitwise.a, m:t
a.[m] || a.[m] = a.[m] apply orb_diag.
Qed.

Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0.forall a b : t, lor a b == 0 -> a == 0
Proof.forall a b : t, lor a b == 0 -> a == 0
 intros a b H.a, b:t
H:lor a b == 0
a == 0 bitwise.a, b:t
H:lor a b == 0
m:t
a.[m] = false
 apply (orb_false_iff a.[m] b.[m]).a, b:t
H:lor a b == 0
m:t
a.[m] || b.[m] = false
 now rewrite <- lor_spec, H, bits_0.
Qed.

Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0.forall a b : t, lor a b == 0 <-> a == 0 /\ b == 0
Proof.forall a b : t, lor a b == 0 <-> a == 0 /\ b == 0
 intros a b.a, b:t
lor a b == 0 <-> a == 0 /\ b == 0 split.a, b:t
lor a b == 0 -> a == 0 /\ b == 0
a, b:t
a == 0 /\ b == 0 -> lor a b == 0
 split.a, b:t
H:lor a b == 0
a == 0
a, b:t
H:lor a b == 0
b == 0
a, b:t
a == 0 /\ b == 0 -> lor a b == 0 now apply lor_eq_0_l in H.a, b:t
H:lor a b == 0
b == 0
a, b:t
a == 0 /\ b == 0 -> lor a b == 0
 rewrite lor_comm in H.a, b:t
H:lor b a == 0
b == 0
a, b:t
a == 0 /\ b == 0 -> lor a b == 0 now apply lor_eq_0_l in H.a, b:t
a == 0 /\ b == 0 -> lor a b == 0
 intros (EQ,EQ').a, b:t
EQ:a == 0
EQ':b == 0
lor a b == 0 now rewrite EQ, lor_0_l.
Qed.

Lemma land_0_l : forall a, land 0 a == 0.forall a : t, land 0 a == 0
Proof.forall a : t, land 0 a == 0
 intros.a:t
land 0 a == 0 bitwise.a, m:t
false && a.[m] = false trivial.
Qed.

Lemma land_0_r : forall a, land a 0 == 0.forall a : t, land a 0 == 0
Proof.forall a : t, land a 0 == 0
 intros.a:t
land a 0 == 0 bitwise.a, m:t
a.[m] && false = false apply andb_false_r.
Qed.

Lemma land_comm : forall a b, land a b == land b a.forall a b : t, land a b == land b a
Proof.forall a b : t, land a b == land b a
 intros.a, b:t
land a b == land b a bitwise.a, b, m:t
a.[m] && b.[m] = b.[m] && a.[m] apply andb_comm.
Qed.

Lemma land_assoc :
 forall a b c, land a (land b c) == land (land a b) c.forall a b c : t,
land a (land b c) == land (land a b) c
Proof.forall a b c : t,
land a (land b c) == land (land a b) c
 intros.a, b, c:t
land a (land b c) == land (land a b) c bitwise.a, b, c, m:t
a.[m] && (b.[m] && c.[m]) = a.[m] && b.[m] && c.[m] apply andb_assoc.
Qed.

Lemma land_diag : forall a, land a a == a.forall a : t, land a a == a
Proof.forall a : t, land a a == a
 intros.a:t
land a a == a bitwise.a, m:t
a.[m] && a.[m] = a.[m] apply andb_diag.
Qed.

Lemma ldiff_0_l : forall a, ldiff 0 a == 0.forall a : t, ldiff 0 a == 0
Proof.forall a : t, ldiff 0 a == 0
 intros.a:t
ldiff 0 a == 0 bitwise.a, m:t
false && negb a.[m] = false trivial.
Qed.

Lemma ldiff_0_r : forall a, ldiff a 0 == a.forall a : t, ldiff a 0 == a
Proof.forall a : t, ldiff a 0 == a
 intros.a:t
ldiff a 0 == a bitwise.a, m:t
a.[m] && negb false = a.[m] now rewrite andb_true_r.
Qed.

Lemma ldiff_diag : forall a, ldiff a a == 0.forall a : t, ldiff a a == 0
Proof.forall a : t, ldiff a a == 0
 intros.a:t
ldiff a a == 0 bitwise.a, m:t
a.[m] && negb a.[m] = false apply andb_negb_r.
Qed.

Lemma lor_land_distr_l : forall a b c,
 lor (land a b) c == land (lor a c) (lor b c).forall a b c : t,
lor (land a b) c == land (lor a c) (lor b c)
Proof.forall a b c : t,
lor (land a b) c == land (lor a c) (lor b c)
 intros.a, b, c:t
lor (land a b) c == land (lor a c) (lor b c) bitwise.a, b, c, m:t
a.[m] && b.[m] || c.[m] =
(a.[m] || c.[m]) && (b.[m] || c.[m]) apply orb_andb_distrib_l.
Qed.

Lemma lor_land_distr_r : forall a b c,
 lor a (land b c) == land (lor a b) (lor a c).forall a b c : t,
lor a (land b c) == land (lor a b) (lor a c)
Proof.forall a b c : t,
lor a (land b c) == land (lor a b) (lor a c)
 intros.a, b, c:t
lor a (land b c) == land (lor a b) (lor a c) bitwise.a, b, c, m:t
a.[m] || b.[m] && c.[m] =
(a.[m] || b.[m]) && (a.[m] || c.[m]) apply orb_andb_distrib_r.
Qed.

Lemma land_lor_distr_l : forall a b c,
 land (lor a b) c == lor (land a c) (land b c).forall a b c : t,
land (lor a b) c == lor (land a c) (land b c)
Proof.forall a b c : t,
land (lor a b) c == lor (land a c) (land b c)
 intros.a, b, c:t
land (lor a b) c == lor (land a c) (land b c) bitwise.a, b, c, m:t
(a.[m] || b.[m]) && c.[m] =
a.[m] && c.[m] || b.[m] && c.[m] apply andb_orb_distrib_l.
Qed.

Lemma land_lor_distr_r : forall a b c,
 land a (lor b c) == lor (land a b) (land a c).forall a b c : t,
land a (lor b c) == lor (land a b) (land a c)
Proof.forall a b c : t,
land a (lor b c) == lor (land a b) (land a c)
 intros.a, b, c:t
land a (lor b c) == lor (land a b) (land a c) bitwise.a, b, c, m:t
a.[m] && (b.[m] || c.[m]) =
a.[m] && b.[m] || a.[m] && c.[m] apply andb_orb_distrib_r.
Qed.

Lemma ldiff_ldiff_l : forall a b c,
 ldiff (ldiff a b) c == ldiff a (lor b c).forall a b c : t,
ldiff (ldiff a b) c == ldiff a (lor b c)
Proof.forall a b c : t,
ldiff (ldiff a b) c == ldiff a (lor b c)
 intros.a, b, c:t
ldiff (ldiff a b) c == ldiff a (lor b c) bitwise.a, b, c, m:t
a.[m] && negb b.[m] && negb c.[m] =
a.[m] && negb (b.[m] || c.[m]) now rewrite negb_orb, andb_assoc.
Qed.

Lemma lor_ldiff_and : forall a b,
 lor (ldiff a b) (land a b) == a.forall a b : t, lor (ldiff a b) (land a b) == a
Proof.forall a b : t, lor (ldiff a b) (land a b) == a
 intros.a, b:t
lor (ldiff a b) (land a b) == a bitwise.a, b, m:t
a.[m] && negb b.[m] || a.[m] && b.[m] = a.[m]
 now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r.
Qed.

Lemma land_ldiff : forall a b,
 land (ldiff a b) b == 0.forall a b : t, land (ldiff a b) b == 0
Proof.forall a b : t, land (ldiff a b) b == 0
 intros.a, b:t
land (ldiff a b) b == 0 bitwise.a, b, m:t
a.[m] && negb b.[m] && b.[m] = false
 now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r.
Qed.

Properties of setbit and clearbit

Definition setbit a n := lor a (1<<n).
Definition clearbit a n := ldiff a (1<<n).

Lemma setbit_spec' : forall a n, setbit a n == lor a (2^n).forall a n : t, setbit a n == lor a (2 ^ n)
Proof.forall a n : t, setbit a n == lor a (2 ^ n)
 intros.a, n:t
setbit a n == lor a (2 ^ n) unfold setbit.a, n:t
lor a (1 << n) == lor a (2 ^ n) now rewrite shiftl_1_l.
Qed.

Lemma clearbit_spec' : forall a n, clearbit a n == ldiff a (2^n).forall a n : t, clearbit a n == ldiff a (2 ^ n)
Proof.forall a n : t, clearbit a n == ldiff a (2 ^ n)
 intros.a, n:t
clearbit a n == ldiff a (2 ^ n) unfold clearbit.a, n:t
ldiff a (1 << n) == ldiff a (2 ^ n) now rewrite shiftl_1_l.
Qed.

Instance setbit_wd : Proper (eq==>eq==>eq) setbit.Proper (eq ==> eq ==> eq) setbit
Proof.Proper (eq ==> eq ==> eq) setbit unfold setbit.Proper (eq ==> eq ==> eq)
  (fun a n : t => lor a (1 << n)) solve_proper. Qed.

Instance clearbit_wd : Proper (eq==>eq==>eq) clearbit.Proper (eq ==> eq ==> eq) clearbit
Proof.Proper (eq ==> eq ==> eq) clearbit unfold clearbit.Proper (eq ==> eq ==> eq)
  (fun a n : t => ldiff a (1 << n)) solve_proper. Qed.

Lemma pow2_bits_true : forall n, (2^n).[n] = true.forall n : t, (2 ^ n).[n] = true
Proof.forall n : t, (2 ^ n).[n] = true
 intros.n:t
(2 ^ n).[n] = true rewrite <- (mul_1_l (2^n)).n:t
(1 * 2 ^ n).[n] = true rewrite <- (add_0_l n) at 2.n:t
(1 * 2 ^ n).[0 + n] = true
 now rewrite mul_pow2_bits_add, bit0_odd, odd_1.
Qed.

Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false.forall n m : t, n ~= m -> (2 ^ n).[m] = false
Proof.forall n m : t, n ~= m -> (2 ^ n).[m] = false
 intros.n, m:t
H:n ~= m
(2 ^ n).[m] = false
 rewrite <- (mul_1_l (2^n)).n, m:t
H:n ~= m
(1 * 2 ^ n).[m] = false
 destruct (le_gt_cases n m).n, m:t
H:n ~= m
H0:n <= m
(1 * 2 ^ n).[m] = false
n, m:t
H:n ~= m
H0:m < n
(1 * 2 ^ n).[m] = false
 rewrite mul_pow2_bits_high; trivial.n, m:t
H:n ~= m
H0:n <= m
1.[m - n] = false
n, m:t
H:n ~= m
H0:m < n
(1 * 2 ^ n).[m] = false
 rewrite <- (succ_pred (m-n)) by (apply sub_gt; order).n, m:t
H:n ~= m
H0:n <= m
1.[S (P (m - n))] = false
n, m:t
H:n ~= m
H0:m < n
(1 * 2 ^ n).[m] = false
 now rewrite <- div2_bits, div_small, bits_0 by order'.n, m:t
H:n ~= m
H0:m < n
(1 * 2 ^ n).[m] = false
 rewrite mul_pow2_bits_low; trivial.
Qed.

Lemma pow2_bits_eqb : forall n m, (2^n).[m] = eqb n m.forall n m : t, (2 ^ n).[m] = (n =? m)
Proof.forall n m : t, (2 ^ n).[m] = (n =? m)
 intros.n, m:t
(2 ^ n).[m] = (n =? m) apply eq_true_iff_eq.n, m:t
(2 ^ n).[m] = true <-> (n =? m) = true rewrite eqb_eq.n, m:t
(2 ^ n).[m] = true <-> n == m split.n, m:t
(2 ^ n).[m] = true -> n == m
n, m:t
n == m -> (2 ^ n).[m] = true
 destruct (eq_decidable n m) as [H|H].n, m:t
H:n == m
(2 ^ n).[m] = true -> n == m
n, m:t
H:n ~= m
(2 ^ n).[m] = true -> n == m
n, m:t
n == m -> (2 ^ n).[m] = true trivial.n, m:t
H:n ~= m
(2 ^ n).[m] = true -> n == m
n, m:t
n == m -> (2 ^ n).[m] = true
 now rewrite (pow2_bits_false _ _ H).n, m:t
n == m -> (2 ^ n).[m] = true
 intros EQ.n, m:t
EQ:n == m
(2 ^ n).[m] = true rewrite EQ.n, m:t
EQ:n == m
(2 ^ m).[m] = true apply pow2_bits_true.
Qed.

Lemma setbit_eqb : forall a n m,
 (setbit a n).[m] = eqb n m || a.[m].forall a n m : t, (setbit a n).[m] = (n =? m) || a.[m]
Proof.forall a n m : t, (setbit a n).[m] = (n =? m) || a.[m]
 intros.a, n, m:t
(setbit a n).[m] = (n =? m) || a.[m] now rewrite setbit_spec', lor_spec, pow2_bits_eqb, orb_comm.
Qed.

Lemma setbit_iff : forall a n m,
 (setbit a n).[m] = true <-> n==m \/ a.[m] = true.forall a n m : t,
(setbit a n).[m] = true <-> n == m \/ a.[m] = true
Proof.forall a n m : t,
(setbit a n).[m] = true <-> n == m \/ a.[m] = true
 intros.a, n, m:t
(setbit a n).[m] = true <-> n == m \/ a.[m] = true now rewrite setbit_eqb, orb_true_iff, eqb_eq.
Qed.

Lemma setbit_eq : forall a n, (setbit a n).[n] = true.forall a n : t, (setbit a n).[n] = true
Proof.forall a n : t, (setbit a n).[n] = true
 intros.a, n:t
(setbit a n).[n] = true apply setbit_iff.a, n:t
n == n \/ a.[n] = true now left.
Qed.

Lemma setbit_neq : forall a n m, n~=m ->
 (setbit a n).[m] = a.[m].forall a n m : t, n ~= m -> (setbit a n).[m] = a.[m]
Proof.forall a n m : t, n ~= m -> (setbit a n).[m] = a.[m]
 intros a n m H.a, n, m:t
H:n ~= m
(setbit a n).[m] = a.[m] rewrite setbit_eqb.a, n, m:t
H:n ~= m
(n =? m) || a.[m] = a.[m]
 rewrite <- eqb_eq in H.a, n, m:t
H:(n =? m) <> true
(n =? m) || a.[m] = a.[m] apply not_true_is_false in H.a, n, m:t
H:(n =? m) = false
(n =? m) || a.[m] = a.[m] now rewrite H.
Qed.

Lemma clearbit_eqb : forall a n m,
 (clearbit a n).[m] = a.[m] && negb (eqb n m).forall a n m : t,
(clearbit a n).[m] = a.[m] && negb (n =? m)
Proof.forall a n m : t,
(clearbit a n).[m] = a.[m] && negb (n =? m)
 intros.a, n, m:t
(clearbit a n).[m] = a.[m] && negb (n =? m) now rewrite clearbit_spec', ldiff_spec, pow2_bits_eqb.
Qed.

Lemma clearbit_iff : forall a n m,
 (clearbit a n).[m] = true <-> a.[m] = true /\ n~=m.forall a n m : t,
(clearbit a n).[m] = true <-> a.[m] = true /\ n ~= m
Proof.forall a n m : t,
(clearbit a n).[m] = true <-> a.[m] = true /\ n ~= m
 intros.a, n, m:t
(clearbit a n).[m] = true <-> a.[m] = true /\ n ~= m rewrite clearbit_eqb, andb_true_iff, <- eqb_eq.a, n, m:t
a.[m] = true /\ negb (n =? m) = true <->
a.[m] = true /\ (n =? m) <> true
 now rewrite negb_true_iff, not_true_iff_false.
Qed.

Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false.forall a n : t, (clearbit a n).[n] = false
Proof.forall a n : t, (clearbit a n).[n] = false
 intros.a, n:t
(clearbit a n).[n] = false rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)).a, n:t
a.[n] && negb true = false
 apply andb_false_r.
Qed.

Lemma clearbit_neq : forall a n m, n~=m ->
 (clearbit a n).[m] = a.[m].forall a n m : t, n ~= m -> (clearbit a n).[m] = a.[m]
Proof.forall a n m : t, n ~= m -> (clearbit a n).[m] = a.[m]
 intros a n m H.a, n, m:t
H:n ~= m
(clearbit a n).[m] = a.[m] rewrite clearbit_eqb.a, n, m:t
H:n ~= m
a.[m] && negb (n =? m) = a.[m]
 rewrite <- eqb_eq in H.a, n, m:t
H:(n =? m) <> true
a.[m] && negb (n =? m) = a.[m] apply not_true_is_false in H.a, n, m:t
H:(n =? m) = false
a.[m] && negb (n =? m) = a.[m] rewrite H.a, n, m:t
H:(n =? m) = false
a.[m] && negb false = a.[m]
 apply andb_true_r.
Qed.

Shifts of bitwise operations

Lemma shiftl_lxor : forall a b n,
 (lxor a b) << n == lxor (a << n) (b << n).forall a b n : t,
lxor a b << n == lxor (a << n) (b << n)
Proof.forall a b n : t,
lxor a b << n == lxor (a << n) (b << n)
 intros.a, b, n:t
lxor a b << n == lxor (a << n) (b << n) bitwise.a, b, n, m:t
(lxor a b << n).[m] = xorb (a << n).[m] (b << n).[m]
 destruct (le_gt_cases n m).a, b, n, m:t
H:n <= m
(lxor a b << n).[m] = xorb (a << n).[m] (b << n).[m]
a, b, n, m:t
H:m < n
(lxor a b << n).[m] = xorb (a << n).[m] (b << n).[m]
 now rewrite !shiftl_spec_high', lxor_spec.a, b, n, m:t
H:m < n
(lxor a b << n).[m] = xorb (a << n).[m] (b << n).[m]
 now rewrite !shiftl_spec_low.
Qed.

Lemma shiftr_lxor : forall a b n,
 (lxor a b) >> n == lxor (a >> n) (b >> n).forall a b n : t,
lxor a b >> n == lxor (a >> n) (b >> n)
Proof.forall a b n : t,
lxor a b >> n == lxor (a >> n) (b >> n)
 intros.a, b, n:t
lxor a b >> n == lxor (a >> n) (b >> n) bitwise.a, b, n, m:t
(lxor a b >> n).[m] = xorb (a >> n).[m] (b >> n).[m] now rewrite !shiftr_spec', lxor_spec.
Qed.

Lemma shiftl_land : forall a b n,
 (land a b) << n == land (a << n) (b << n).forall a b n : t,
land a b << n == land (a << n) (b << n)
Proof.forall a b n : t,
land a b << n == land (a << n) (b << n)
 intros.a, b, n:t
land a b << n == land (a << n) (b << n) bitwise.a, b, n, m:t
(land a b << n).[m] = (a << n).[m] && (b << n).[m]
 destruct (le_gt_cases n m).a, b, n, m:t
H:n <= m
(land a b << n).[m] = (a << n).[m] && (b << n).[m]
a, b, n, m:t
H:m < n
(land a b << n).[m] = (a << n).[m] && (b << n).[m]
 now rewrite !shiftl_spec_high', land_spec.a, b, n, m:t
H:m < n
(land a b << n).[m] = (a << n).[m] && (b << n).[m]
 now rewrite !shiftl_spec_low.
Qed.

Lemma shiftr_land : forall a b n,
 (land a b) >> n == land (a >> n) (b >> n).forall a b n : t,
land a b >> n == land (a >> n) (b >> n)
Proof.forall a b n : t,
land a b >> n == land (a >> n) (b >> n)
 intros.a, b, n:t
land a b >> n == land (a >> n) (b >> n) bitwise.a, b, n, m:t
(land a b >> n).[m] = (a >> n).[m] && (b >> n).[m] now rewrite !shiftr_spec', land_spec.
Qed.

Lemma shiftl_lor : forall a b n,
 (lor a b) << n == lor (a << n) (b << n).forall a b n : t,
lor a b << n == lor (a << n) (b << n)
Proof.forall a b n : t,
lor a b << n == lor (a << n) (b << n)
 intros.a, b, n:t
lor a b << n == lor (a << n) (b << n) bitwise.a, b, n, m:t
(lor a b << n).[m] = (a << n).[m] || (b << n).[m]
 destruct (le_gt_cases n m).a, b, n, m:t
H:n <= m
(lor a b << n).[m] = (a << n).[m] || (b << n).[m]
a, b, n, m:t
H:m < n
(lor a b << n).[m] = (a << n).[m] || (b << n).[m]
 now rewrite !shiftl_spec_high', lor_spec.a, b, n, m:t
H:m < n
(lor a b << n).[m] = (a << n).[m] || (b << n).[m]
 now rewrite !shiftl_spec_low.
Qed.

Lemma shiftr_lor : forall a b n,
 (lor a b) >> n == lor (a >> n) (b >> n).forall a b n : t,
lor a b >> n == lor (a >> n) (b >> n)
Proof.forall a b n : t,
lor a b >> n == lor (a >> n) (b >> n)
 intros.a, b, n:t
lor a b >> n == lor (a >> n) (b >> n) bitwise.a, b, n, m:t
(lor a b >> n).[m] = (a >> n).[m] || (b >> n).[m] now rewrite !shiftr_spec', lor_spec.
Qed.

Lemma shiftl_ldiff : forall a b n,
 (ldiff a b) << n == ldiff (a << n) (b << n).forall a b n : t,
ldiff a b << n == ldiff (a << n) (b << n)
Proof.forall a b n : t,
ldiff a b << n == ldiff (a << n) (b << n)
 intros.a, b, n:t
ldiff a b << n == ldiff (a << n) (b << n) bitwise.a, b, n, m:t
(ldiff a b << n).[m] =
(a << n).[m] && negb (b << n).[m]
 destruct (le_gt_cases n m).a, b, n, m:t
H:n <= m
(ldiff a b << n).[m] =
(a << n).[m] && negb (b << n).[m]
a, b, n, m:t
H:m < n
(ldiff a b << n).[m] =
(a << n).[m] && negb (b << n).[m]
 now rewrite !shiftl_spec_high', ldiff_spec.a, b, n, m:t
H:m < n
(ldiff a b << n).[m] =
(a << n).[m] && negb (b << n).[m]
 now rewrite !shiftl_spec_low.
Qed.

Lemma shiftr_ldiff : forall a b n,
 (ldiff a b) >> n == ldiff (a >> n) (b >> n).forall a b n : t,
ldiff a b >> n == ldiff (a >> n) (b >> n)
Proof.forall a b n : t,
ldiff a b >> n == ldiff (a >> n) (b >> n)
 intros.a, b, n:t
ldiff a b >> n == ldiff (a >> n) (b >> n) bitwise.a, b, n, m:t
(ldiff a b >> n).[m] =
(a >> n).[m] && negb (b >> n).[m] now rewrite !shiftr_spec', ldiff_spec.
Qed.

We cannot have a function complementing all bits of a number, otherwise it would have an infinity of bit 1. Nonetheless, we can design a bounded complement

Definition ones n := P (1 << n).

Definition lnot a n := lxor a (ones n).

Instance ones_wd : Proper (eq==>eq) ones.Proper (eq ==> eq) ones
Proof.Proper (eq ==> eq) ones unfold ones.Proper (eq ==> eq) (fun n : t => P (1 << n)) solve_proper. Qed.

Instance lnot_wd : Proper (eq==>eq==>eq) lnot.Proper (eq ==> eq ==> eq) lnot
Proof.Proper (eq ==> eq ==> eq) lnot unfold lnot.Proper (eq ==> eq ==> eq)
  (fun a n : t => lxor a (ones n)) solve_proper. Qed.

Lemma ones_equiv : forall n, ones n == P (2^n).forall n : t, ones n == P (2 ^ n)
Proof.forall n : t, ones n == P (2 ^ n)
 intros; unfold ones; now rewrite shiftl_1_l.
Qed.

Lemma ones_add : forall n m, ones (m+n) == 2^m * ones n + ones m.forall n m : t,
ones (m + n) == 2 ^ m * ones n + ones m
Proof.forall n m : t,
ones (m + n) == 2 ^ m * ones n + ones m
 intros n m.n, m:t
ones (m + n) == 2 ^ m * ones n + ones m rewrite !ones_equiv.n, m:t
P (2 ^ (m + n)) == 2 ^ m * P (2 ^ n) + P (2 ^ m)
 rewrite <- !sub_1_r, mul_sub_distr_l, mul_1_r, <- pow_add_r.n, m:t
2 ^ (m + n) - 1 == 2 ^ (m + n) - 2 ^ m + (2 ^ m - 1)
 rewrite add_sub_assoc, sub_add.n, m:t
2 ^ (m + n) - 1 == 2 ^ (m + n) - 1
n, m:t
2 ^ m <= 2 ^ (m + n)
n, m:t
1 <= 2 ^ m reflexivity.n, m:t
2 ^ m <= 2 ^ (m + n)
n, m:t
1 <= 2 ^ m
 apply pow_le_mono_r.n, m:t
2 ~= 0
n, m:t
m <= m + n
n, m:t
1 <= 2 ^ m order'.n, m:t
m <= m + n
n, m:t
1 <= 2 ^ m
 rewrite <- (add_0_r m) at 1.n, m:t
m + 0 <= m + n
n, m:t
1 <= 2 ^ m apply add_le_mono_l, le_0_l.n, m:t
1 <= 2 ^ m
 rewrite <- (pow_0_r 2).n, m:t
2 ^ 0 <= 2 ^ m apply pow_le_mono_r.n, m:t
2 ~= 0
n, m:t
0 <= m order'.n, m:t
0 <= m apply le_0_l.
Qed.

Lemma ones_div_pow2 : forall n m, m<=n -> ones n / 2^m == ones (n-m).forall n m : t,
m <= n -> ones n / 2 ^ m == ones (n - m)
Proof.forall n m : t,
m <= n -> ones n / 2 ^ m == ones (n - m)
 intros n m H.n, m:t
H:m <= n
ones n / 2 ^ m == ones (n - m) symmetry.n, m:t
H:m <= n
ones (n - m) == ones n / 2 ^ m apply div_unique with (ones m).n, m:t
H:m <= n
ones m < 2 ^ m
n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m
 rewrite ones_equiv.n, m:t
H:m <= n
P (2 ^ m) < 2 ^ m
n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m
 apply le_succ_l.n, m:t
H:m <= n
S (P (2 ^ m)) <= 2 ^ m
n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m rewrite succ_pred; order_nz.n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m
 rewrite <- (sub_add m n H) at 1.n, m:t
H:m <= n
ones (n - m + m) == 2 ^ m * ones (n - m) + ones m rewrite (add_comm _ m).n, m:t
H:m <= n
ones (m + (n - m)) == 2 ^ m * ones (n - m) + ones m
 apply ones_add.
Qed.

Lemma ones_mod_pow2 : forall n m, m<=n -> (ones n) mod (2^m) == ones m.forall n m : t, m <= n -> ones n mod 2 ^ m == ones m
Proof.forall n m : t, m <= n -> ones n mod 2 ^ m == ones m
 intros n m H.n, m:t
H:m <= n
ones n mod 2 ^ m == ones m symmetry.n, m:t
H:m <= n
ones m == ones n mod 2 ^ m apply mod_unique with (ones (n-m)).n, m:t
H:m <= n
ones m < 2 ^ m
n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m
 rewrite ones_equiv.n, m:t
H:m <= n
P (2 ^ m) < 2 ^ m
n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m
 apply le_succ_l.n, m:t
H:m <= n
S (P (2 ^ m)) <= 2 ^ m
n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m rewrite succ_pred; order_nz.n, m:t
H:m <= n
ones n == 2 ^ m * ones (n - m) + ones m
 rewrite <- (sub_add m n H) at 1.n, m:t
H:m <= n
ones (n - m + m) == 2 ^ m * ones (n - m) + ones m rewrite (add_comm _ m).n, m:t
H:m <= n
ones (m + (n - m)) == 2 ^ m * ones (n - m) + ones m
 apply ones_add.
Qed.

Lemma ones_spec_low : forall n m, m<n -> (ones n).[m] = true.forall n m : t, m < n -> (ones n).[m] = true
Proof.forall n m : t, m < n -> (ones n).[m] = true
 intros.n, m:t
H:m < n
(ones n).[m] = true apply testbit_true.n, m:t
H:m < n
(ones n / 2 ^ m) mod 2 == 1 rewrite ones_div_pow2 by order.n, m:t
H:m < n
ones (n - m) mod 2 == 1
 rewrite <- (pow_1_r 2).n, m:t
H:m < n
ones (n - m) mod 2 ^ 1 == 1 rewrite ones_mod_pow2.n, m:t
H:m < n
ones 1 == 1
n, m:t
H:m < n
1 <= n - m
 rewrite ones_equiv.n, m:t
H:m < n
P (2 ^ 1) == 1
n, m:t
H:m < n
1 <= n - m now nzsimpl'.n, m:t
H:m < n
1 <= n - m
 apply le_add_le_sub_r.n, m:t
H:m < n
1 + m <= n nzsimpl.n, m:t
H:m < n
S m <= n now apply le_succ_l.
Qed.

Lemma ones_spec_high : forall n m, n<=m -> (ones n).[m] = false.forall n m : t, n <= m -> (ones n).[m] = false
Proof.forall n m : t, n <= m -> (ones n).[m] = false
 intros.n, m:t
H:n <= m
(ones n).[m] = false
 destruct (eq_0_gt_0_cases n) as [EQ|LT]; rewrite ones_equiv.n, m:t
H:n <= m
EQ:n == 0
(P (2 ^ n)).[m] = false
n, m:t
H:n <= m
LT:0 < n
(P (2 ^ n)).[m] = false
 now rewrite EQ, pow_0_r, one_succ, pred_succ, bits_0.n, m:t
H:n <= m
LT:0 < n
(P (2 ^ n)).[m] = false
 apply bits_above_log2.n, m:t
H:n <= m
LT:0 < n
log2 (P (2 ^ n)) < m
 rewrite log2_pred_pow2; trivial.n, m:t
H:n <= m
LT:0 < n
P n < m rewrite <-le_succ_l, succ_pred; order.
Qed.

Lemma ones_spec_iff : forall n m, (ones n).[m] = true <-> m<n.forall n m : t, (ones n).[m] = true <-> m < n
Proof.forall n m : t, (ones n).[m] = true <-> m < n
 intros.n, m:t
(ones n).[m] = true <-> m < n split.n, m:t
(ones n).[m] = true -> m < n
n, m:t
m < n -> (ones n).[m] = true intros H.n, m:t
H:(ones n).[m] = true
m < n
n, m:t
m < n -> (ones n).[m] = true
 apply lt_nge.n, m:t
H:(ones n).[m] = true
~ n <= m
n, m:t
m < n -> (ones n).[m] = true intro H'.n, m:t
H:(ones n).[m] = true
H':n <= m
False
n, m:t
m < n -> (ones n).[m] = true apply ones_spec_high in H'.n, m:t
H:(ones n).[m] = true
H':(ones n).[m] = false
False
n, m:t
m < n -> (ones n).[m] = true
 rewrite H in H'; discriminate.n, m:t
m < n -> (ones n).[m] = true
 apply ones_spec_low.
Qed.

Lemma lnot_spec_low : forall a n m, m<n ->
 (lnot a n).[m] = negb a.[m].forall a n m : t, m < n -> (lnot a n).[m] = negb a.[m]
Proof.forall a n m : t, m < n -> (lnot a n).[m] = negb a.[m]
 intros.a, n, m:t
H:m < n
(lnot a n).[m] = negb a.[m] unfold lnot.a, n, m:t
H:m < n
(lxor a (ones n)).[m] = negb a.[m] now rewrite lxor_spec, ones_spec_low.
Qed.

Lemma lnot_spec_high : forall a n m, n<=m ->
 (lnot a n).[m] = a.[m].forall a n m : t, n <= m -> (lnot a n).[m] = a.[m]
Proof.forall a n m : t, n <= m -> (lnot a n).[m] = a.[m]
 intros.a, n, m:t
H:n <= m
(lnot a n).[m] = a.[m] unfold lnot.a, n, m:t
H:n <= m
(lxor a (ones n)).[m] = a.[m] now rewrite lxor_spec, ones_spec_high, xorb_false_r.
Qed.

Lemma lnot_involutive : forall a n, lnot (lnot a n) n == a.forall a n : t, lnot (lnot a n) n == a
Proof.forall a n : t, lnot (lnot a n) n == a
 intros a n.a, n:t
lnot (lnot a n) n == a bitwise.a, n, m:t
(lnot (lnot a n) n).[m] = a.[m]
 destruct (le_gt_cases n m).a, n, m:t
H:n <= m
(lnot (lnot a n) n).[m] = a.[m]
a, n, m:t
H:m < n
(lnot (lnot a n) n).[m] = a.[m]
 now rewrite 2 lnot_spec_high.a, n, m:t
H:m < n
(lnot (lnot a n) n).[m] = a.[m]
 now rewrite 2 lnot_spec_low, negb_involutive.
Qed.

Lemma lnot_0_l : forall n, lnot 0 n == ones n.forall n : t, lnot 0 n == ones n
Proof.forall n : t, lnot 0 n == ones n
 intros.n:t
lnot 0 n == ones n unfold lnot.n:t
lxor 0 (ones n) == ones n apply lxor_0_l.
Qed.

Lemma lnot_ones : forall n, lnot (ones n) n == 0.forall n : t, lnot (ones n) n == 0
Proof.forall n : t, lnot (ones n) n == 0
 intros.n:t
lnot (ones n) n == 0 unfold lnot.n:t
lxor (ones n) (ones n) == 0 apply lxor_nilpotent.
Qed.

Bounded complement and other operations

Lemma lor_ones_low : forall a n, log2 a < n ->
 lor a (ones n) == ones n.forall a n : t, log2 a < n -> lor a (ones n) == ones n
Proof.forall a n : t, log2 a < n -> lor a (ones n) == ones n
 intros a n H.a, n:t
H:log2 a < n
lor a (ones n) == ones n bitwise.a, n:t
H:log2 a < n
m:t
a.[m] || (ones n).[m] = (ones n).[m] destruct (le_gt_cases n m).a, n:t
H:log2 a < n
m:t
H0:n <= m
a.[m] || (ones n).[m] = (ones n).[m]
a, n:t
H:log2 a < n
m:t
H0:m < n
a.[m] || (ones n).[m] = (ones n).[m]
 rewrite ones_spec_high, bits_above_log2; trivial.a, n:t
H:log2 a < n
m:t
H0:n <= m
log2 a < m
a, n:t
H:log2 a < n
m:t
H0:m < n
a.[m] || (ones n).[m] = (ones n).[m]
 now apply lt_le_trans with n.a, n:t
H:log2 a < n
m:t
H0:m < n
a.[m] || (ones n).[m] = (ones n).[m]
 now rewrite ones_spec_low, orb_true_r.
Qed.

Lemma land_ones : forall a n, land a (ones n) == a mod 2^n.forall a n : t, land a (ones n) == a mod 2 ^ n
Proof.forall a n : t, land a (ones n) == a mod 2 ^ n
 intros a n.a, n:t
land a (ones n) == a mod 2 ^ n bitwise.a, n, m:t
a.[m] && (ones n).[m] = (a mod 2 ^ n).[m] destruct (le_gt_cases n m).a, n, m:t
H:n <= m
a.[m] && (ones n).[m] = (a mod 2 ^ n).[m]
a, n, m:t
H:m < n
a.[m] && (ones n).[m] = (a mod 2 ^ n).[m]
 now rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r.a, n, m:t
H:m < n
a.[m] && (ones n).[m] = (a mod 2 ^ n).[m]
 now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r.
Qed.

Lemma land_ones_low : forall a n, log2 a < n ->
 land a (ones n) == a.forall a n : t, log2 a < n -> land a (ones n) == a
Proof.forall a n : t, log2 a < n -> land a (ones n) == a
 intros; rewrite land_ones.a, n:t
H:log2 a < n
a mod 2 ^ n == a apply mod_small.a, n:t
H:log2 a < n
a < 2 ^ n
 apply log2_lt_cancel.a, n:t
H:log2 a < n
log2 a < log2 (2 ^ n) rewrite log2_pow2; trivial using le_0_l.
Qed.

Lemma ldiff_ones_r : forall a n,
 ldiff a (ones n) == (a >> n) << n.forall a n : t, ldiff a (ones n) == (a >> n) << n
Proof.forall a n : t, ldiff a (ones n) == (a >> n) << n
 intros a n.a, n:t
ldiff a (ones n) == (a >> n) << n bitwise.a, n, m:t
a.[m] && negb (ones n).[m] = ((a >> n) << n).[m] destruct (le_gt_cases n m).a, n, m:t
H:n <= m
a.[m] && negb (ones n).[m] = ((a >> n) << n).[m]
a, n, m:t
H:m < n
a.[m] && negb (ones n).[m] = ((a >> n) << n).[m]
 rewrite ones_spec_high, shiftl_spec_high', shiftr_spec'; trivial.a, n, m:t
H:n <= m
a.[m] && negb false = a.[m - n + n]
a, n, m:t
H:m < n
a.[m] && negb (ones n).[m] = ((a >> n) << n).[m]
 rewrite sub_add; trivial.a, n, m:t
H:n <= m
a.[m] && negb false = a.[m]
a, n, m:t
H:m < n
a.[m] && negb (ones n).[m] = ((a >> n) << n).[m] apply andb_true_r.a, n, m:t
H:m < n
a.[m] && negb (ones n).[m] = ((a >> n) << n).[m]
 now rewrite ones_spec_low, shiftl_spec_low, andb_false_r.
Qed.

Lemma ldiff_ones_r_low : forall a n, log2 a < n ->
 ldiff a (ones n) == 0.forall a n : t, log2 a < n -> ldiff a (ones n) == 0
Proof.forall a n : t, log2 a < n -> ldiff a (ones n) == 0
 intros a n H.a, n:t
H:log2 a < n
ldiff a (ones n) == 0 bitwise.a, n:t
H:log2 a < n
m:t
a.[m] && negb (ones n).[m] = false destruct (le_gt_cases n m).a, n:t
H:log2 a < n
m:t
H0:n <= m
a.[m] && negb (ones n).[m] = false
a, n:t
H:log2 a < n
m:t
H0:m < n
a.[m] && negb (ones n).[m] = false
 rewrite ones_spec_high, bits_above_log2; trivial.a, n:t
H:log2 a < n
m:t
H0:n <= m
log2 a < m
a, n:t
H:log2 a < n
m:t
H0:m < n
a.[m] && negb (ones n).[m] = false
 now apply lt_le_trans with n.a, n:t
H:log2 a < n
m:t
H0:m < n
a.[m] && negb (ones n).[m] = false
 now rewrite ones_spec_low, andb_false_r.
Qed.

Lemma ldiff_ones_l_low : forall a n, log2 a < n ->
 ldiff (ones n) a == lnot a n.forall a n : t,
log2 a < n -> ldiff (ones n) a == lnot a n
Proof.forall a n : t,
log2 a < n -> ldiff (ones n) a == lnot a n
 intros a n H.a, n:t
H:log2 a < n
ldiff (ones n) a == lnot a n bitwise.a, n:t
H:log2 a < n
m:t
(ones n).[m] && negb a.[m] = (lnot a n).[m] destruct (le_gt_cases n m).a, n:t
H:log2 a < n
m:t
H0:n <= m
(ones n).[m] && negb a.[m] = (lnot a n).[m]
a, n:t
H:log2 a < n
m:t
H0:m < n
(ones n).[m] && negb a.[m] = (lnot a n).[m]
 rewrite ones_spec_high, lnot_spec_high, bits_above_log2; trivial.a, n:t
H:log2 a < n
m:t
H0:n <= m
log2 a < m
a, n:t
H:log2 a < n
m:t
H0:m < n
(ones n).[m] && negb a.[m] = (lnot a n).[m]
 now apply lt_le_trans with n.a, n:t
H:log2 a < n
m:t
H0:m < n
(ones n).[m] && negb a.[m] = (lnot a n).[m]
 now rewrite ones_spec_low, lnot_spec_low.
Qed.

Lemma lor_lnot_diag : forall a n,
 lor a (lnot a n) == lor a (ones n).forall a n : t, lor a (lnot a n) == lor a (ones n)
Proof.forall a n : t, lor a (lnot a n) == lor a (ones n)
 intros a n.a, n:t
lor a (lnot a n) == lor a (ones n) bitwise.a, n, m:t
a.[m] || (lnot a n).[m] = a.[m] || (ones n).[m]
 destruct (le_gt_cases n m).a, n, m:t
H:n <= m
a.[m] || (lnot a n).[m] = a.[m] || (ones n).[m]
a, n, m:t
H:m < n
a.[m] || (lnot a n).[m] = a.[m] || (ones n).[m]
 rewrite lnot_spec_high, ones_spec_high; trivial.a, n, m:t
H:n <= m
a.[m] || a.[m] = a.[m] || false
a, n, m:t
H:m < n
a.[m] || (lnot a n).[m] = a.[m] || (ones n).[m] now destruct a.[m].a, n, m:t
H:m < n
a.[m] || (lnot a n).[m] = a.[m] || (ones n).[m]
 rewrite lnot_spec_low, ones_spec_low; trivial.a, n, m:t
H:m < n
a.[m] || negb a.[m] = a.[m] || true now destruct a.[m].
Qed.

Lemma lor_lnot_diag_low : forall a n, log2 a < n ->
 lor a (lnot a n) == ones n.forall a n : t,
log2 a < n -> lor a (lnot a n) == ones n
Proof.forall a n : t,
log2 a < n -> lor a (lnot a n) == ones n
 intros a n H.a, n:t
H:log2 a < n
lor a (lnot a n) == ones n now rewrite lor_lnot_diag, lor_ones_low.
Qed.

Lemma land_lnot_diag : forall a n,
 land a (lnot a n) == ldiff a (ones n).forall a n : t, land a (lnot a n) == ldiff a (ones n)
Proof.forall a n : t, land a (lnot a n) == ldiff a (ones n)
 intros a n.a, n:t
land a (lnot a n) == ldiff a (ones n) bitwise.a, n, m:t
a.[m] && (lnot a n).[m] = a.[m] && negb (ones n).[m]
 destruct (le_gt_cases n m).a, n, m:t
H:n <= m
a.[m] && (lnot a n).[m] = a.[m] && negb (ones n).[m]
a, n, m:t
H:m < n
a.[m] && (lnot a n).[m] = a.[m] && negb (ones n).[m]
 rewrite lnot_spec_high, ones_spec_high; trivial.a, n, m:t
H:n <= m
a.[m] && a.[m] = a.[m] && negb false
a, n, m:t
H:m < n
a.[m] && (lnot a n).[m] = a.[m] && negb (ones n).[m] now destruct a.[m].a, n, m:t
H:m < n
a.[m] && (lnot a n).[m] = a.[m] && negb (ones n).[m]
 rewrite lnot_spec_low, ones_spec_low; trivial.a, n, m:t
H:m < n
a.[m] && negb a.[m] = a.[m] && negb true now destruct a.[m].
Qed.

Lemma land_lnot_diag_low : forall a n, log2 a < n ->
 land a (lnot a n) == 0.forall a n : t, log2 a < n -> land a (lnot a n) == 0
Proof.forall a n : t, log2 a < n -> land a (lnot a n) == 0
 intros.a, n:t
H:log2 a < n
land a (lnot a n) == 0 now rewrite land_lnot_diag, ldiff_ones_r_low.
Qed.

Lemma lnot_lor_low : forall a b n, log2 a < n -> log2 b < n ->
 lnot (lor a b) n == land (lnot a n) (lnot b n).forall a b n : t,
log2 a < n ->
log2 b < n ->
lnot (lor a b) n == land (lnot a n) (lnot b n)
Proof.forall a b n : t,
log2 a < n ->
log2 b < n ->
lnot (lor a b) n == land (lnot a n) (lnot b n)
 intros a b n Ha Hb.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
lnot (lor a b) n == land (lnot a n) (lnot b n) bitwise.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
(lnot (lor a b) n).[m] =
(lnot a n).[m] && (lnot b n).[m] destruct (le_gt_cases n m).a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
(lnot (lor a b) n).[m] =
(lnot a n).[m] && (lnot b n).[m]
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (lor a b) n).[m] =
(lnot a n).[m] && (lnot b n).[m]
 rewrite !lnot_spec_high, lor_spec, !bits_above_log2; trivial.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 b < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (lor a b) n).[m] =
(lnot a n).[m] && (lnot b n).[m]
 now apply lt_le_trans with n.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (lor a b) n).[m] =
(lnot a n).[m] && (lnot b n).[m]
 now apply lt_le_trans with n.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (lor a b) n).[m] =
(lnot a n).[m] && (lnot b n).[m]
 now rewrite !lnot_spec_low, lor_spec, negb_orb.
Qed.

Lemma lnot_land_low : forall a b n, log2 a < n -> log2 b < n ->
 lnot (land a b) n == lor (lnot a n) (lnot b n).forall a b n : t,
log2 a < n ->
log2 b < n ->
lnot (land a b) n == lor (lnot a n) (lnot b n)
Proof.forall a b n : t,
log2 a < n ->
log2 b < n ->
lnot (land a b) n == lor (lnot a n) (lnot b n)
 intros a b n Ha Hb.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
lnot (land a b) n == lor (lnot a n) (lnot b n) bitwise.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
(lnot (land a b) n).[m] =
(lnot a n).[m] || (lnot b n).[m] destruct (le_gt_cases n m).a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
(lnot (land a b) n).[m] =
(lnot a n).[m] || (lnot b n).[m]
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (land a b) n).[m] =
(lnot a n).[m] || (lnot b n).[m]
 rewrite !lnot_spec_high, land_spec, !bits_above_log2; trivial.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 b < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (land a b) n).[m] =
(lnot a n).[m] || (lnot b n).[m]
 now apply lt_le_trans with n.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (land a b) n).[m] =
(lnot a n).[m] || (lnot b n).[m]
 now apply lt_le_trans with n.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (land a b) n).[m] =
(lnot a n).[m] || (lnot b n).[m]
 now rewrite !lnot_spec_low, land_spec, negb_andb.
Qed.

Lemma ldiff_land_low : forall a b n, log2 a < n ->
 ldiff a b == land a (lnot b n).forall a b n : t,
log2 a < n -> ldiff a b == land a (lnot b n)
Proof.forall a b n : t,
log2 a < n -> ldiff a b == land a (lnot b n)
 intros a b n Ha.a, b, n:t
Ha:log2 a < n
ldiff a b == land a (lnot b n) bitwise.a, b, n:t
Ha:log2 a < n
m:t
a.[m] && negb b.[m] = a.[m] && (lnot b n).[m] destruct (le_gt_cases n m).a, b, n:t
Ha:log2 a < n
m:t
H:n <= m
a.[m] && negb b.[m] = a.[m] && (lnot b n).[m]
a, b, n:t
Ha:log2 a < n
m:t
H:m < n
a.[m] && negb b.[m] = a.[m] && (lnot b n).[m]
 rewrite (bits_above_log2 a m).a, b, n:t
Ha:log2 a < n
m:t
H:n <= m
false && negb b.[m] = false && (lnot b n).[m]
a, b, n:t
Ha:log2 a < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
m:t
H:m < n
a.[m] && negb b.[m] = a.[m] && (lnot b n).[m] trivial.a, b, n:t
Ha:log2 a < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
m:t
H:m < n
a.[m] && negb b.[m] = a.[m] && (lnot b n).[m]
 now apply lt_le_trans with n.a, b, n:t
Ha:log2 a < n
m:t
H:m < n
a.[m] && negb b.[m] = a.[m] && (lnot b n).[m]
 rewrite !lnot_spec_low; trivial.
Qed.

Lemma lnot_ldiff_low : forall a b n, log2 a < n -> log2 b < n ->
 lnot (ldiff a b) n == lor (lnot a n) b.forall a b n : t,
log2 a < n ->
log2 b < n -> lnot (ldiff a b) n == lor (lnot a n) b
Proof.forall a b n : t,
log2 a < n ->
log2 b < n -> lnot (ldiff a b) n == lor (lnot a n) b
 intros a b n Ha Hb.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
lnot (ldiff a b) n == lor (lnot a n) b bitwise.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
(lnot (ldiff a b) n).[m] = (lnot a n).[m] || b.[m] destruct (le_gt_cases n m).a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
(lnot (ldiff a b) n).[m] = (lnot a n).[m] || b.[m]
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (ldiff a b) n).[m] = (lnot a n).[m] || b.[m]
 rewrite !lnot_spec_high, ldiff_spec, !bits_above_log2; trivial.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 b < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (ldiff a b) n).[m] = (lnot a n).[m] || b.[m]
 now apply lt_le_trans with n.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:n <= m
log2 a < m
a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (ldiff a b) n).[m] = (lnot a n).[m] || b.[m]
 now apply lt_le_trans with n.a, b, n:t
Ha:log2 a < n
Hb:log2 b < n
m:t
H:m < n
(lnot (ldiff a b) n).[m] = (lnot a n).[m] || b.[m]
 now rewrite !lnot_spec_low, ldiff_spec, negb_andb, negb_involutive.
Qed.

Lemma lxor_lnot_lnot : forall a b n,
 lxor (lnot a n) (lnot b n) == lxor a b.forall a b n : t,
lxor (lnot a n) (lnot b n) == lxor a b
Proof.forall a b n : t,
lxor (lnot a n) (lnot b n) == lxor a b
 intros a b n.a, b, n:t
lxor (lnot a n) (lnot b n) == lxor a b bitwise.a, b, n, m:t
xorb (lnot a n).[m] (lnot b n).[m] = xorb a.[m] b.[m] destruct (le_gt_cases n m).a, b, n, m:t
H:n <= m
xorb (lnot a n).[m] (lnot b n).[m] = xorb a.[m] b.[m]
a, b, n, m:t
H:m < n
xorb (lnot a n).[m] (lnot b n).[m] = xorb a.[m] b.[m]
 rewrite !lnot_spec_high; trivial.a, b, n, m:t
H:m < n
xorb (lnot a n).[m] (lnot b n).[m] = xorb a.[m] b.[m]
 rewrite !lnot_spec_low, xorb_negb_negb; trivial.
Qed.

Lemma lnot_lxor_l : forall a b n,
 lnot (lxor a b) n == lxor (lnot a n) b.forall a b n : t,
lnot (lxor a b) n == lxor (lnot a n) b
Proof.forall a b n : t,
lnot (lxor a b) n == lxor (lnot a n) b
 intros a b n.a, b, n:t
lnot (lxor a b) n == lxor (lnot a n) b bitwise.a, b, n, m:t
(lnot (lxor a b) n).[m] = xorb (lnot a n).[m] b.[m] destruct (le_gt_cases n m).a, b, n, m:t
H:n <= m
(lnot (lxor a b) n).[m] = xorb (lnot a n).[m] b.[m]
a, b, n, m:t
H:m < n
(lnot (lxor a b) n).[m] = xorb (lnot a n).[m] b.[m]
 rewrite !lnot_spec_high, lxor_spec; trivial.a, b, n, m:t
H:m < n
(lnot (lxor a b) n).[m] = xorb (lnot a n).[m] b.[m]
 rewrite !lnot_spec_low, lxor_spec, negb_xorb_l; trivial.
Qed.

Lemma lnot_lxor_r : forall a b n,
 lnot (lxor a b) n == lxor a (lnot b n).forall a b n : t,
lnot (lxor a b) n == lxor a (lnot b n)
Proof.forall a b n : t,
lnot (lxor a b) n == lxor a (lnot b n)
 intros a b n.a, b, n:t
lnot (lxor a b) n == lxor a (lnot b n) bitwise.a, b, n, m:t
(lnot (lxor a b) n).[m] = xorb a.[m] (lnot b n).[m] destruct (le_gt_cases n m).a, b, n, m:t
H:n <= m
(lnot (lxor a b) n).[m] = xorb a.[m] (lnot b n).[m]
a, b, n, m:t
H:m < n
(lnot (lxor a b) n).[m] = xorb a.[m] (lnot b n).[m]
 rewrite !lnot_spec_high, lxor_spec; trivial.a, b, n, m:t
H:m < n
(lnot (lxor a b) n).[m] = xorb a.[m] (lnot b n).[m]
 rewrite !lnot_spec_low, lxor_spec, negb_xorb_r; trivial.
Qed.

Lemma lxor_lor : forall a b, land a b == 0 ->
 lxor a b == lor a b.forall a b : t, land a b == 0 -> lxor a b == lor a b
Proof.forall a b : t, land a b == 0 -> lxor a b == lor a b
 intros a b H.a, b:t
H:land a b == 0
lxor a b == lor a b bitwise.a, b:t
H:land a b == 0
m:t
xorb a.[m] b.[m] = a.[m] || b.[m]
 assert (a.[m] && b.[m] = false)
   by now rewrite <- land_spec, H, bits_0.a, b:t
H:land a b == 0
m:t
H0:a.[m] && b.[m] = false
xorb a.[m] b.[m] = a.[m] || b.[m]
 now destruct a.[m], b.[m].
Qed.

Bitwise operations and log2

Lemma log2_bits_unique : forall a n,
 a.[n] = true ->
 (forall m, n<m -> a.[m] = false) ->
 log2 a == n.forall a n : t,
a.[n] = true ->
(forall m : t, n < m -> a.[m] = false) -> log2 a == n
Proof.forall a n : t,
a.[n] = true ->
(forall m : t, n < m -> a.[m] = false) -> log2 a == n
 intros a n H H'.a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
log2 a == n
 destruct (eq_0_gt_0_cases a) as [Ha|Ha].a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
Ha:a == 0
log2 a == n
a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
Ha:0 < a
log2 a == n
 now rewrite Ha, bits_0 in H.a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
Ha:0 < a
log2 a == n
 apply le_antisymm; apply le_ngt; intros LT.a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
Ha:0 < a
LT:n < log2 a
False
a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
Ha:0 < a
LT:log2 a < n
False
 specialize (H' _ LT).a, n:t
H:a.[n] = true
H':a.[log2 a] = false
Ha:0 < a
LT:n < log2 a
False
a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
Ha:0 < a
LT:log2 a < n
False now rewrite bit_log2 in H' by order.a, n:t
H:a.[n] = true
H':forall m : t, n < m -> a.[m] = false
Ha:0 < a
LT:log2 a < n
False
 now rewrite bits_above_log2 in H by order.
Qed.

Lemma log2_shiftr : forall a n, log2 (a >> n) == log2 a - n.forall a n : t, log2 (a >> n) == log2 a - n
Proof.forall a n : t, log2 (a >> n) == log2 a - n
 intros a n.a, n:t
log2 (a >> n) == log2 a - n
 destruct (eq_0_gt_0_cases a) as [Ha|Ha].a, n:t
Ha:a == 0
log2 (a >> n) == log2 a - n
a, n:t
Ha:0 < a
log2 (a >> n) == log2 a - n
 now rewrite Ha, shiftr_0_l, log2_nonpos, sub_0_l by order.a, n:t
Ha:0 < a
log2 (a >> n) == log2 a - n
 destruct (lt_ge_cases (log2 a) n).a, n:t
Ha:0 < a
H:log2 a < n
log2 (a >> n) == log2 a - n
a, n:t
Ha:0 < a
H:n <= log2 a
log2 (a >> n) == log2 a - n
 rewrite shiftr_eq_0, log2_nonpos by order.a, n:t
Ha:0 < a
H:log2 a < n
0 == log2 a - n
a, n:t
Ha:0 < a
H:n <= log2 a
log2 (a >> n) == log2 a - n
 symmetry.a, n:t
Ha:0 < a
H:log2 a < n
log2 a - n == 0
a, n:t
Ha:0 < a
H:n <= log2 a
log2 (a >> n) == log2 a - n rewrite sub_0_le; order.a, n:t
Ha:0 < a
H:n <= log2 a
log2 (a >> n) == log2 a - n
 apply log2_bits_unique.a, n:t
Ha:0 < a
H:n <= log2 a
(a >> n).[log2 a - n] = true
a, n:t
Ha:0 < a
H:n <= log2 a
forall m : t, log2 a - n < m -> (a >> n).[m] = false
 now rewrite shiftr_spec', sub_add, bit_log2 by order.a, n:t
Ha:0 < a
H:n <= log2 a
forall m : t, log2 a - n < m -> (a >> n).[m] = false
 intros m Hm.a, n:t
Ha:0 < a
H:n <= log2 a
m:t
Hm:log2 a - n < m
(a >> n).[m] = false
 rewrite shiftr_spec'; trivial.a, n:t
Ha:0 < a
H:n <= log2 a
m:t
Hm:log2 a - n < m
a.[m + n] = false apply bits_above_log2; try order.a, n:t
Ha:0 < a
H:n <= log2 a
m:t
Hm:log2 a - n < m
log2 a < m + n
 now apply lt_sub_lt_add_r.
Qed.

Lemma log2_shiftl : forall a n, a~=0 -> log2 (a << n) == log2 a + n.forall a n : t, a ~= 0 -> log2 (a << n) == log2 a + n
Proof.forall a n : t, a ~= 0 -> log2 (a << n) == log2 a + n
 intros a n Ha.a, n:t
Ha:a ~= 0
log2 (a << n) == log2 a + n
 rewrite shiftl_mul_pow2, add_comm by trivial.a, n:t
Ha:a ~= 0
log2 (a * 2 ^ n) == n + log2 a
 apply log2_mul_pow2.a, n:t
Ha:a ~= 0
0 < a
a, n:t
Ha:a ~= 0
0 <= n generalize (le_0_l a); order.a, n:t
Ha:a ~= 0
0 <= n apply le_0_l.
Qed.

Lemma log2_lor : forall a b,
 log2 (lor a b) == max (log2 a) (log2 b).forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
Proof.forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
 assert (AUX : forall a b, a<=b -> log2 (lor a b) == log2 b).forall a b : t, a <= b -> log2 (lor a b) == log2 b
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
  intros a b H.a, b:t
H:a <= b
log2 (lor a b) == log2 b
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
  destruct (eq_0_gt_0_cases a) as [Ha|Ha].a, b:t
H:a <= b
Ha:a == 0
log2 (lor a b) == log2 b
a, b:t
H:a <= b
Ha:0 < a
log2 (lor a b) == log2 b
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b) now rewrite Ha, lor_0_l.a, b:t
H:a <= b
Ha:0 < a
log2 (lor a b) == log2 b
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
  apply log2_bits_unique.a, b:t
H:a <= b
Ha:0 < a
(lor a b).[log2 b] = true
a, b:t
H:a <= b
Ha:0 < a
forall m : t, log2 b < m -> (lor a b).[m] = false
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
  now rewrite lor_spec, bit_log2, orb_true_r by order.a, b:t
H:a <= b
Ha:0 < a
forall m : t, log2 b < m -> (lor a b).[m] = false
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
  intros m Hm.a, b:t
H:a <= b
Ha:0 < a
m:t
Hm:log2 b < m
(lor a b).[m] = false
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b) assert (H' := log2_le_mono _ _ H).a, b:t
H:a <= b
Ha:0 < a
m:t
Hm:log2 b < m
H':log2 a <= log2 b
(lor a b).[m] = false
AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
  now rewrite lor_spec, 2 bits_above_log2 by order.AUX:forall a b : t, a <= b -> log2 (lor a b) == log2 b
forall a b : t,
log2 (lor a b) == max (log2 a) (log2 b)
 (* main *)
 intros a b.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
log2 (lor a b) == max (log2 a) (log2 b) destruct (le_ge_cases a b) as [H|H].AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
H:a <= b
log2 (lor a b) == max (log2 a) (log2 b)
AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
H:b <= a
log2 (lor a b) == max (log2 a) (log2 b)
 rewrite max_r by now apply log2_le_mono.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
H:a <= b
log2 (lor a b) == log2 b
AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
H:b <= a
log2 (lor a b) == max (log2 a) (log2 b)
 now apply AUX.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
H:b <= a
log2 (lor a b) == max (log2 a) (log2 b)
 rewrite max_l by now apply log2_le_mono.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
H:b <= a
log2 (lor a b) == log2 a
 rewrite lor_comm.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lor a0 b0) == log2 b0
a, b:t
H:b <= a
log2 (lor b a) == log2 a now apply AUX.
Qed.

Lemma log2_land : forall a b,
 log2 (land a b) <= min (log2 a) (log2 b).forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
Proof.forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
 assert (AUX : forall a b, a<=b -> log2 (land a b) <= log2 a).forall a b : t, a <= b -> log2 (land a b) <= log2 a
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
  intros a b H.a, b:t
H:a <= b
log2 (land a b) <= log2 a
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
  apply le_ngt.a, b:t
H:a <= b
~ log2 a < log2 (land a b)
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b) intros H'.a, b:t
H:a <= b
H':log2 a < log2 (land a b)
False
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
  destruct (eq_decidable (land a b) 0) as [EQ|NEQ].a, b:t
H:a <= b
H':log2 a < log2 (land a b)
EQ:land a b == 0
False
a, b:t
H:a <= b
H':log2 a < log2 (land a b)
NEQ:land a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
  rewrite EQ in H'.a, b:t
H:a <= b
H':log2 a < log2 0
EQ:land a b == 0
False
a, b:t
H:a <= b
H':log2 a < log2 (land a b)
NEQ:land a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b) apply log2_lt_cancel in H'.a, b:t
H:a <= b
H':a < 0
EQ:land a b == 0
False
a, b:t
H:a <= b
H':log2 a < log2 (land a b)
NEQ:land a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b) generalize (le_0_l a); order.a, b:t
H:a <= b
H':log2 a < log2 (land a b)
NEQ:land a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
  generalize (bit_log2 (land a b) NEQ).a, b:t
H:a <= b
H':log2 a < log2 (land a b)
NEQ:land a b ~= 0
(land a b).[log2 (land a b)] = true -> False
AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
  now rewrite land_spec, bits_above_log2.AUX:forall a b : t, a <= b -> log2 (land a b) <= log2 a
forall a b : t,
log2 (land a b) <= min (log2 a) (log2 b)
 (* main *)
 intros a b.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
log2 (land a b) <= min (log2 a) (log2 b)
 destruct (le_ge_cases a b) as [H|H].AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
H:a <= b
log2 (land a b) <= min (log2 a) (log2 b)
AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
H:b <= a
log2 (land a b) <= min (log2 a) (log2 b)
 rewrite min_l by now apply log2_le_mono.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
H:a <= b
log2 (land a b) <= log2 a
AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
H:b <= a
log2 (land a b) <= min (log2 a) (log2 b) now apply AUX.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
H:b <= a
log2 (land a b) <= min (log2 a) (log2 b)
 rewrite min_r by now apply log2_le_mono.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
H:b <= a
log2 (land a b) <= log2 b rewrite land_comm.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (land a0 b0) <= log2 a0
a, b:t
H:b <= a
log2 (land b a) <= log2 b now apply AUX.
Qed.

Lemma log2_lxor : forall a b,
 log2 (lxor a b) <= max (log2 a) (log2 b).forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
Proof.forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
 assert (AUX : forall a b, a<=b -> log2 (lxor a b) <= log2 b).forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
  intros a b H.a, b:t
H:a <= b
log2 (lxor a b) <= log2 b
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
  apply le_ngt.a, b:t
H:a <= b
~ log2 b < log2 (lxor a b)
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b) intros H'.a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
False
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
  destruct (eq_decidable (lxor a b) 0) as [EQ|NEQ].a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
EQ:lxor a b == 0
False
a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
  rewrite EQ in H'.a, b:t
H:a <= b
H':log2 b < log2 0
EQ:lxor a b == 0
False
a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b) apply log2_lt_cancel in H'.a, b:t
H:a <= b
H':b < 0
EQ:lxor a b == 0
False
a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b) generalize (le_0_l a); order.a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
False
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
  generalize (bit_log2 (lxor a b) NEQ).a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
(lxor a b).[log2 (lxor a b)] = true -> False
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
  rewrite lxor_spec, 2 bits_above_log2; try order.a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
xorb false false = true -> False
a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
log2 a < log2 (lxor a b)
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b) discriminate.a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
log2 a < log2 (lxor a b)
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
  apply le_lt_trans with (log2 b); trivial.a, b:t
H:a <= b
H':log2 b < log2 (lxor a b)
NEQ:lxor a b ~= 0
log2 a <= log2 b
AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b) now apply log2_le_mono.AUX:forall a b : t, a <= b -> log2 (lxor a b) <= log2 b
forall a b : t,
log2 (lxor a b) <= max (log2 a) (log2 b)
 (* main *)
 intros a b.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
log2 (lxor a b) <= max (log2 a) (log2 b)
 destruct (le_ge_cases a b) as [H|H].AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
H:a <= b
log2 (lxor a b) <= max (log2 a) (log2 b)
AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
H:b <= a
log2 (lxor a b) <= max (log2 a) (log2 b)
 rewrite max_r by now apply log2_le_mono.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
H:a <= b
log2 (lxor a b) <= log2 b
AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
H:b <= a
log2 (lxor a b) <= max (log2 a) (log2 b) now apply AUX.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
H:b <= a
log2 (lxor a b) <= max (log2 a) (log2 b)
 rewrite max_l by now apply log2_le_mono.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
H:b <= a
log2 (lxor a b) <= log2 a rewrite lxor_comm.AUX:forall a0 b0 : t, a0 <= b0 -> log2 (lxor a0 b0) <= log2 b0
a, b:t
H:b <= a
log2 (lxor b a) <= log2 a now apply AUX.
Qed.

Bitwise operations and arithmetical operations

Notation xor3 a b c := (xorb (xorb a b) c).
Notation lxor3 a b c := (lxor (lxor a b) c).

Notation nextcarry a b c := ((a&&b) || (c && (a||b))).
Notation lnextcarry a b c := (lor (land a b) (land c (lor a b))).

Lemma add_bit0 : forall a b, (a+b).[0] = xorb a.[0] b.[0].forall a b : t, (a + b).[0] = xorb a.[0] b.[0]
Proof.forall a b : t, (a + b).[0] = xorb a.[0] b.[0]
 intros.a, b:t
(a + b).[0] = xorb a.[0] b.[0] now rewrite !bit0_odd, odd_add.
Qed.

Lemma add3_bit0 : forall a b c,
 (a+b+c).[0] = xor3 a.[0] b.[0] c.[0].forall a b c : t,
(a + b + c).[0] = xor3 a.[0] b.[0] c.[0]
Proof.forall a b c : t,
(a + b + c).[0] = xor3 a.[0] b.[0] c.[0]
 intros.a, b, c:t
(a + b + c).[0] = xor3 a.[0] b.[0] c.[0] now rewrite !add_bit0.
Qed.

Lemma add3_bits_div2 : forall (a0 b0 c0 : bool),
 (a0 + b0 + c0)/2 == nextcarry a0 b0 c0.forall a0 b0 c0 : bool,
(a0 + b0 + c0) / 2 == nextcarry a0 b0 c0
Proof.forall a0 b0 c0 : bool,
(a0 + b0 + c0) / 2 == nextcarry a0 b0 c0
 assert (H : 1+1 == 2) by now nzsimpl'.H:1 + 1 == 2
forall a0 b0 c0 : bool,
(a0 + b0 + c0) / 2 == nextcarry a0 b0 c0
 intros [|] [|] [|]; simpl; rewrite ?add_0_l, ?add_0_r, ?H;
  (apply div_same; order') || (apply div_small; order') || idtac.H:1 + 1 == 2
(2 + 1) / 2 == 1
 symmetry.H:1 + 1 == 2
1 == (2 + 1) / 2 apply div_unique with 1.H:1 + 1 == 2
1 < 2
H:1 + 1 == 2
2 + 1 == 2 * 1 + 1 order'.H:1 + 1 == 2
2 + 1 == 2 * 1 + 1 now nzsimpl'.
Qed.

Lemma add_carry_div2 : forall a b (c0:bool),
 (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0.forall (a b : t) (c0 : bool),
(a + b + c0) / 2 ==
a / 2 + b / 2 + nextcarry a.[0] b.[0] c0
Proof.forall (a b : t) (c0 : bool),
(a + b + c0) / 2 ==
a / 2 + b / 2 + nextcarry a.[0] b.[0] c0
 intros.a, b:t
c0:bool
(a + b + c0) / 2 ==
a / 2 + b / 2 + nextcarry a.[0] b.[0] c0
 rewrite <- add3_bits_div2.a, b:t
c0:bool
(a + b + c0) / 2 ==
a / 2 + b / 2 + (a.[0] + b.[0] + c0) / 2
 rewrite (add_comm ((a/2)+_)).a, b:t
c0:bool
(a + b + c0) / 2 ==
(a.[0] + b.[0] + c0) / 2 + (a / 2 + b / 2)
 rewrite <- div_add by order'.a, b:t
c0:bool
(a + b + c0) / 2 ==
(a.[0] + b.[0] + c0 + (a / 2 + b / 2) * 2) / 2
 f_equiv.a, b:t
c0:bool
a + b + c0 == a.[0] + b.[0] + c0 + (a / 2 + b / 2) * 2
 rewrite <- !div2_div, mul_comm, mul_add_distr_l.a, b:t
c0:bool
a + b + c0 ==
a.[0] + b.[0] + c0 + (2 * div2 a + 2 * div2 b)
 rewrite (div2_odd a), <- bit0_odd at 1.a, b:t
c0:bool
2 * div2 a + a.[0] + b + c0 ==
a.[0] + b.[0] + c0 + (2 * div2 a + 2 * div2 b) fold (b2n a.[0]).a, b:t
c0:bool
2 * div2 a + a.[0] + b + c0 ==
a.[0] + b.[0] + c0 + (2 * div2 a + 2 * div2 b)
 rewrite (div2_odd b), <- bit0_odd at 1.a, b:t
c0:bool
2 * div2 a + a.[0] + (2 * div2 b + b.[0]) + c0 ==
a.[0] + b.[0] + c0 + (2 * div2 a + 2 * div2 b) fold (b2n b.[0]).a, b:t
c0:bool
2 * div2 a + a.[0] + (2 * div2 b + b.[0]) + c0 ==
a.[0] + b.[0] + c0 + (2 * div2 a + 2 * div2 b)
 rewrite add_shuffle1.a, b:t
c0:bool
2 * div2 a + 2 * div2 b + (a.[0] + b.[0]) + c0 ==
a.[0] + b.[0] + c0 + (2 * div2 a + 2 * div2 b)
 rewrite <-(add_assoc _ _ c0).a, b:t
c0:bool
2 * div2 a + 2 * div2 b + (a.[0] + b.[0] + c0) ==
a.[0] + b.[0] + c0 + (2 * div2 a + 2 * div2 b) apply add_comm.
Qed.

The main result concerning addition: we express the bits of the sum in term of bits of a and b and of some carry stream which is also recursively determined by another equation.

Lemma add_carry_bits : forall a b (c0:bool), exists c,
 a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0.forall (a b : t) (c0 : bool),
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
Proof.forall (a b : t) (c0 : bool),
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 intros a b c0.a, b:t
c0:bool
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 (* induction over some n such that [a<2^n] and [b<2^n] *)
 set (n:=max a b).a, b:t
c0:bool
n:=max a b:t
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 assert (Ha : a<2^n).a, b:t
c0:bool
n:=max a b:t
a < 2 ^ n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
  apply lt_le_trans with (2^a).a, b:t
c0:bool
n:=max a b:t
a < 2 ^ a
a, b:t
c0:bool
n:=max a b:t
2 ^ a <= 2 ^ n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 apply pow_gt_lin_r, lt_1_2.a, b:t
c0:bool
n:=max a b:t
2 ^ a <= 2 ^ n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
  apply pow_le_mono_r.a, b:t
c0:bool
n:=max a b:t
2 ~= 0
a, b:t
c0:bool
n:=max a b:t
a <= n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 order'.a, b:t
c0:bool
n:=max a b:t
a <= n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 unfold n.a, b:t
c0:bool
n:=max a b:t
a <= max a b
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
  destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'.a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 assert (Hb : b<2^n).a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
b < 2 ^ n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
  apply lt_le_trans with (2^b).a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
b < 2 ^ b
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
2 ^ b <= 2 ^ n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 apply pow_gt_lin_r, lt_1_2.a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
2 ^ b <= 2 ^ n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
  apply pow_le_mono_r.a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
2 ~= 0
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
b <= n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 order'.a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
b <= n
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 unfold n.a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
b <= max a b
a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
  destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'.a, b:t
c0:bool
n:=max a b:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 clearbody n.a, b:t
c0:bool
n:t
Ha:a < 2 ^ n
Hb:b < 2 ^ n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 revert a b c0 Ha Hb.n:t
forall (a b : t) (c0 : bool),
a < 2 ^ n ->
b < 2 ^ n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 induct n.forall (a b : t) (c0 : bool),
a < 2 ^ 0 ->
b < 2 ^ 0 ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 (*base*)
 intros a b c0.a, b:t
c0:bool
a < 2 ^ 0 ->
b < 2 ^ 0 ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 rewrite !pow_0_r, !one_succ, !lt_succ_r.a, b:t
c0:bool
a <= 0 ->
b <= 0 ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0 intros Ha Hb.a, b:t
c0:bool
Ha:a <= 0
Hb:b <= 0
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 exists c0.a, b:t
c0:bool
Ha:a <= 0
Hb:b <= 0
a + b + c0 == lxor3 a b c0 /\
c0 / 2 == lnextcarry a b c0 /\ c0.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 setoid_replace a with 0 by (generalize (le_0_l a); order').a, b:t
c0:bool
Ha:a <= 0
Hb:b <= 0
0 + b + c0 == lxor3 0 b c0 /\
c0 / 2 == lnextcarry 0 b c0 /\ c0.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 setoid_replace b with 0 by (generalize (le_0_l b); order').a, b:t
c0:bool
Ha:a <= 0
Hb:b <= 0
0 + 0 + c0 == lxor3 0 0 c0 /\
c0 / 2 == lnextcarry 0 0 c0 /\ c0.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 rewrite !add_0_l, !lxor_0_l, !lor_0_r, !land_0_r, !lor_0_r.a, b:t
c0:bool
Ha:a <= 0
Hb:b <= 0
c0 == c0 /\ c0 / 2 == 0 /\ c0.[0] = c0
forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 rewrite b2n_div2, b2n_bit0; now repeat split.forall n : t,
(forall (a b : t) (c0 : bool),
 a < 2 ^ n ->
 b < 2 ^ n ->
 exists c : t,
   a + b + c0 == lxor3 a b c /\
   c / 2 == lnextcarry a b c /\ c.[0] = c0) ->
forall (a b : t) (c0 : bool),
a < 2 ^ S n ->
b < 2 ^ S n ->
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 (*step*)
 intros n IH a b c0 Ha Hb.n:t
IH:forall (a0 b0 : t) (c1 : bool),
a0 < 2 ^ n ->
b0 < 2 ^ n ->
exists c : t,
  a0 + b0 + c1 == lxor3 a0 b0 c /\
  c / 2 == lnextcarry a0 b0 c /\ c.[0] = c1
a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 set (c1:=nextcarry a.[0] b.[0] c0).n:t
IH:forall (a0 b0 : t) (c2 : bool),
a0 < 2 ^ n ->
b0 < 2 ^ n ->
exists c : t,
  a0 + b0 + c2 == lxor3 a0 b0 c /\
  c / 2 == lnextcarry a0 b0 c /\ c.[0] = c2
a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
exists c : t,
  a + b + c0 == lxor3 a b c /\
  c / 2 == lnextcarry a b c /\ c.[0] = c0
 destruct (IH (a/2) (b/2) c1) as (c & IH1 & IH2 & Hc); clear IH.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
a / 2 < 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
b / 2 < 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
exists c2 : t,
  a + b + c0 == lxor3 a b c2 /\
  c2 / 2 == lnextcarry a b c2 /\ c2.[0] = c0
 apply div_lt_upper_bound; trivial.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
2 ~= 0
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
a < 2 * 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
b / 2 < 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
exists c2 : t,
  a + b + c0 == lxor3 a b c2 /\
  c2 / 2 == lnextcarry a b c2 /\ c2.[0] = c0 order'.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
a < 2 * 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
b / 2 < 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
exists c2 : t,
  a + b + c0 == lxor3 a b c2 /\
  c2 / 2 == lnextcarry a b c2 /\ c2.[0] = c0 now rewrite <- pow_succ_r'.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
b / 2 < 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
exists c2 : t,
  a + b + c0 == lxor3 a b c2 /\
  c2 / 2 == lnextcarry a b c2 /\ c2.[0] = c0
 apply div_lt_upper_bound; trivial.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
2 ~= 0
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
b < 2 * 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
exists c2 : t,
  a + b + c0 == lxor3 a b c2 /\
  c2 / 2 == lnextcarry a b c2 /\ c2.[0] = c0 order'.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
b < 2 * 2 ^ n
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
exists c2 : t,
  a + b + c0 == lxor3 a b c2 /\
  c2 / 2 == lnextcarry a b c2 /\ c2.[0] = c0 now rewrite <- pow_succ_r'.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
exists c2 : t,
  a + b + c0 == lxor3 a b c2 /\
  c2 / 2 == lnextcarry a b c2 /\ c2.[0] = c0
 exists (c0 + 2*c).n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
a + b + c0 == lxor3 a b (c0 + 2 * c) /\
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c) /\
(c0 + 2 * c).[0] = c0 repeat split.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
a + b + c0 == lxor3 a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 (* - add *)
 bitwise.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m:t
(a + b + c0).[m] = xor3 a.[m] b.[m] (c0 + 2 * c).[m]
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m:t
(a + b + c0).[0] = xor3 a.[0] b.[0] (c0 + 2 * c).[0]
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
(a + b + c0).[S m'] =
xor3 a.[S m'] b.[S m'] (c0 + 2 * c).[S m']
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
(a + b + c0).[S m'] =
xor3 a.[S m'] b.[S m'] (c0 + 2 * c).[S m']
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 rewrite <- !div2_bits, <- 2 lxor_spec.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
((a + b + c0) / 2).[m'] =
(lxor3 (a / 2) (b / 2) ((c0 + 2 * c) / 2)).[m']
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 f_equiv.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
(a + b + c0) / 2 ==
lxor3 (a / 2) (b / 2) ((c0 + 2 * c) / 2)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 rewrite add_b2n_double_div2, <- IH1.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
(a + b + c0) / 2 == a / 2 + b / 2 + c1
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0 apply add_carry_div2.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c) / 2 == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 (* - carry *)
 rewrite add_b2n_double_div2.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
c == lnextcarry a b (c0 + 2 * c)
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 bitwise.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m:t
c.[m] = nextcarry a.[m] b.[m] (c0 + 2 * c).[m]
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m:t
c.[0] = nextcarry a.[0] b.[0] (c0 + 2 * c).[0]
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
c.[S m'] =
nextcarry a.[S m'] b.[S m'] (c0 + 2 * c).[S m']
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 now rewrite add_b2n_double_bit0.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
c.[S m'] =
nextcarry a.[S m'] b.[S m'] (c0 + 2 * c).[S m']
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 rewrite <- !div2_bits, IH2.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
(lnextcarry (a / 2) (b / 2) c).[m'] =
nextcarry (a / 2).[m'] (b / 2).[m']
  ((c0 + 2 * c) / 2).[m']
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0 autorewrite with bitwise.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
m, m':t
nextcarry (a / 2).[m'] (b / 2).[m'] c.[m'] =
nextcarry (a / 2).[m'] (b / 2).[m']
  ((c0 + 2 * c) / 2).[m']
n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 now rewrite add_b2n_double_div2.n, a, b:t
c0:bool
Ha:a < 2 ^ S n
Hb:b < 2 ^ S n
c1:=nextcarry a.[0] b.[0] c0:bool
c:t
IH1:a / 2 + b / 2 + c1 == lxor3 (a / 2) (b / 2) c
IH2:c / 2 == lnextcarry (a / 2) (b / 2) c
Hc:c.[0] = c1
(c0 + 2 * c).[0] = c0
 (* - carry0 *)
 apply add_b2n_double_bit0.
Qed.

Particular case : the second bit of an addition

Lemma add_bit1 : forall a b,
 (a+b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0]).forall a b : t,
(a + b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0])
Proof.forall a b : t,
(a + b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0])
 intros a b.a, b:t
(a + b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0])
 destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc).a, b, c:t
EQ1:a + b + false == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
(a + b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0])
 simpl in EQ1; rewrite add_0_r in EQ1.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
(a + b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0]) rewrite EQ1.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
(lxor3 a b c).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0])
 autorewrite with bitwise.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
xor3 a.[1] b.[1] c.[1] =
xor3 a.[1] b.[1] (a.[0] && b.[0]) f_equal.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
c.[1] = a.[0] && b.[0]
 rewrite one_succ, <- div2_bits, EQ2.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
(lnextcarry a b c).[0] = a.[0] && b.[0]
 autorewrite with bitwise.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
nextcarry a.[0] b.[0] c.[0] = a.[0] && b.[0]
 rewrite Hc.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
nextcarry a.[0] b.[0] false = a.[0] && b.[0] simpl.a, b, c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
a.[0] && b.[0] || false = a.[0] && b.[0] apply orb_false_r.
Qed.

In an addition, there will be no carries iff there is no common bits in the numbers to add

Lemma nocarry_equiv : forall a b c,
 c/2 == lnextcarry a b c -> c.[0] = false ->
 (c == 0 <-> land a b == 0).forall a b c : t,
c / 2 == lnextcarry a b c ->
c.[0] = false -> c == 0 <-> land a b == 0
Proof.forall a b c : t,
c / 2 == lnextcarry a b c ->
c.[0] = false -> c == 0 <-> land a b == 0
 intros a b c H H'.a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
c == 0 <-> land a b == 0
 split.a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
c == 0 -> land a b == 0
a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
land a b == 0 -> c == 0 intros EQ; rewrite EQ in *.a, b, c:t
H:0 / 2 == lnextcarry a b 0
H':0.[0] = false
EQ:c == 0
land a b == 0
a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
land a b == 0 -> c == 0
 rewrite div_0_l in H by order'.a, b, c:t
H:0 == lnextcarry a b 0
H':0.[0] = false
EQ:c == 0
land a b == 0
a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
land a b == 0 -> c == 0
 symmetry in H.a, b, c:t
H:lnextcarry a b 0 == 0
H':0.[0] = false
EQ:c == 0
land a b == 0
a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
land a b == 0 -> c == 0 now apply lor_eq_0_l in H.a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
land a b == 0 -> c == 0
 intros EQ.a, b, c:t
H:c / 2 == lnextcarry a b c
H':c.[0] = false
EQ:land a b == 0
c == 0 rewrite EQ, lor_0_l in H.a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
c == 0
 apply bits_inj_0.a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
forall n : t, c.[n] = false
 induct n.a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
c.[0] = false
a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
forall n : t, c.[n] = false -> c.[S n] = false trivial.a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
forall n : t, c.[n] = false -> c.[S n] = false
 intros n IH.a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
n:t
IH:c.[n] = false
c.[S n] = false
 rewrite <- div2_bits, H.a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
n:t
IH:c.[n] = false
(land c (lor a b)).[n] = false
 autorewrite with bitwise.a, b, c:t
H:c / 2 == land c (lor a b)
H':c.[0] = false
EQ:land a b == 0
n:t
IH:c.[n] = false
c.[n] && (a.[n] || b.[n]) = false
 now rewrite IH.
Qed.

When there is no common bits, the addition is just a xor

Lemma add_nocarry_lxor : forall a b, land a b == 0 ->
 a+b == lxor a b.forall a b : t, land a b == 0 -> a + b == lxor a b
Proof.forall a b : t, land a b == 0 -> a + b == lxor a b
 intros a b H.a, b:t
H:land a b == 0
a + b == lxor a b
 destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc).a, b:t
H:land a b == 0
c:t
EQ1:a + b + false == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
a + b == lxor a b
 simpl in EQ1; rewrite add_0_r in EQ1.a, b:t
H:land a b == 0
c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
a + b == lxor a b rewrite EQ1.a, b:t
H:land a b == 0
c:t
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
lxor3 a b c == lxor a b
 apply (nocarry_equiv a b c) in H; trivial.a, b, c:t
H:c == 0
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
lxor3 a b c == lxor a b
 rewrite H.a, b, c:t
H:c == 0
EQ1:a + b == lxor3 a b c
EQ2:c / 2 == lnextcarry a b c
Hc:c.[0] = false
lxor3 a b 0 == lxor a b now rewrite lxor_0_r.
Qed.

A null ldiff implies being smaller

Lemma ldiff_le : forall a b, ldiff a b == 0 -> a <= b.forall a b : t, ldiff a b == 0 -> a <= b
Proof.forall a b : t, ldiff a b == 0 -> a <= b
 cut (forall n a b, a < 2^n -> ldiff a b == 0 -> a <= b).(forall n a b : t,
 a < 2 ^ n -> ldiff a b == 0 -> a <= b) ->
forall a b : t, ldiff a b == 0 -> a <= b
forall n a b : t,
a < 2 ^ n -> ldiff a b == 0 -> a <= b
 intros H a b.H:forall n a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
ldiff a b == 0 -> a <= b
forall n a b : t,
a < 2 ^ n -> ldiff a b == 0 -> a <= b apply (H a), pow_gt_lin_r; order'.forall n a b : t,
a < 2 ^ n -> ldiff a b == 0 -> a <= b
 induct n.forall a b : t, a < 2 ^ 0 -> ldiff a b == 0 -> a <= b
forall n : t,
(forall a b : t, a < 2 ^ n -> ldiff a b == 0 -> a <= b) ->
forall a b : t,
a < 2 ^ S n -> ldiff a b == 0 -> a <= b
 intros a b Ha _.a, b:t
Ha:a < 2 ^ 0
a <= b
forall n : t,
(forall a b : t, a < 2 ^ n -> ldiff a b == 0 -> a <= b) ->
forall a b : t,
a < 2 ^ S n -> ldiff a b == 0 -> a <= b rewrite pow_0_r, one_succ, lt_succ_r in Ha.a, b:t
Ha:a <= 0
a <= b
forall n : t,
(forall a b : t, a < 2 ^ n -> ldiff a b == 0 -> a <= b) ->
forall a b : t,
a < 2 ^ S n -> ldiff a b == 0 -> a <= b
 assert (Ha' : a == 0) by (generalize (le_0_l a); order').a, b:t
Ha:a <= 0
Ha':a == 0
a <= b
forall n : t,
(forall a b : t, a < 2 ^ n -> ldiff a b == 0 -> a <= b) ->
forall a b : t,
a < 2 ^ S n -> ldiff a b == 0 -> a <= b
 rewrite Ha'.a, b:t
Ha:a <= 0
Ha':a == 0
0 <= b
forall n : t,
(forall a b : t, a < 2 ^ n -> ldiff a b == 0 -> a <= b) ->
forall a b : t,
a < 2 ^ S n -> ldiff a b == 0 -> a <= b apply le_0_l.forall n : t,
(forall a b : t, a < 2 ^ n -> ldiff a b == 0 -> a <= b) ->
forall a b : t,
a < 2 ^ S n -> ldiff a b == 0 -> a <= b
 intros n IH a b Ha H.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
a <= b
 assert (NEQ : 2 ~= 0) by order'.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a <= b
 rewrite (div_mod a 2 NEQ), (div_mod b 2 NEQ).n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
2 * (a / 2) + a mod 2 <= 2 * (b / 2) + b mod 2
 apply add_le_mono.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
2 * (a / 2) <= 2 * (b / 2)
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a mod 2 <= b mod 2
 apply mul_le_mono_l.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a / 2 <= b / 2
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a mod 2 <= b mod 2
 apply IH.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a / 2 < 2 ^ n
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
ldiff (a / 2) (b / 2) == 0
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a mod 2 <= b mod 2
 apply div_lt_upper_bound; trivial.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a < 2 * 2 ^ n
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
ldiff (a / 2) (b / 2) == 0
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a mod 2 <= b mod 2 now rewrite <- pow_succ_r'.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
ldiff (a / 2) (b / 2) == 0
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a mod 2 <= b mod 2
 rewrite <- (pow_1_r 2), <- 2 shiftr_div_pow2.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
ldiff (a >> 1) (b >> 1) == 0
n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a mod 2 <= b mod 2
 now rewrite <- shiftr_ldiff, H, shiftr_div_pow2, pow_1_r, div_0_l.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a mod 2 <= b mod 2
 rewrite <- 2 bit0_mod.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:ldiff a b == 0
NEQ:2 ~= 0
a.[0] <= b.[0]
 apply bits_inj_iff in H.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:testbit (ldiff a b) === testbit 0
NEQ:2 ~= 0
a.[0] <= b.[0] specialize (H 0).n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:(ldiff a b).[0] = 0.[0]
NEQ:2 ~= 0
a.[0] <= b.[0]
 rewrite ldiff_spec, bits_0 in H.n:t
IH:forall a0 b0 : t,
a0 < 2 ^ n -> ldiff a0 b0 == 0 -> a0 <= b0
a, b:t
Ha:a < 2 ^ S n
H:a.[0] && negb b.[0] = false
NEQ:2 ~= 0
a.[0] <= b.[0]
 destruct a.[0], b.[0]; try discriminate; simpl; order'.
Qed.

Subtraction can be a ldiff when the opposite ldiff is null.

Lemma sub_nocarry_ldiff : forall a b, ldiff b a == 0 ->
 a-b == ldiff a b.forall a b : t, ldiff b a == 0 -> a - b == ldiff a b
Proof.forall a b : t, ldiff b a == 0 -> a - b == ldiff a b
 intros a b H.a, b:t
H:ldiff b a == 0
a - b == ldiff a b
 apply add_cancel_r with b.a, b:t
H:ldiff b a == 0
a - b + b == ldiff a b + b
 rewrite sub_add.a, b:t
H:ldiff b a == 0
a == ldiff a b + b
a, b:t
H:ldiff b a == 0
b <= a
 symmetry.a, b:t
H:ldiff b a == 0
ldiff a b + b == a
a, b:t
H:ldiff b a == 0
b <= a
 rewrite add_nocarry_lxor.a, b:t
H:ldiff b a == 0
lxor (ldiff a b) b == a
a, b:t
H:ldiff b a == 0
land (ldiff a b) b == 0
a, b:t
H:ldiff b a == 0
b <= a
 bitwise.a, b:t
H:ldiff b a == 0
m:t
xorb (a.[m] && negb b.[m]) b.[m] = a.[m]
a, b:t
H:ldiff b a == 0
land (ldiff a b) b == 0
a, b:t
H:ldiff b a == 0
b <= a
 apply bits_inj_iff in H.a, b:t
H:testbit (ldiff b a) === testbit 0
m:t
xorb (a.[m] && negb b.[m]) b.[m] = a.[m]
a, b:t
H:ldiff b a == 0
land (ldiff a b) b == 0
a, b:t
H:ldiff b a == 0
b <= a specialize (H m).a, b, m:t
H:(ldiff b a).[m] = 0.[m]
xorb (a.[m] && negb b.[m]) b.[m] = a.[m]
a, b:t
H:ldiff b a == 0
land (ldiff a b) b == 0
a, b:t
H:ldiff b a == 0
b <= a
 rewrite ldiff_spec, bits_0 in H.a, b, m:t
H:b.[m] && negb a.[m] = false
xorb (a.[m] && negb b.[m]) b.[m] = a.[m]
a, b:t
H:ldiff b a == 0
land (ldiff a b) b == 0
a, b:t
H:ldiff b a == 0
b <= a
 now destruct a.[m], b.[m].a, b:t
H:ldiff b a == 0
land (ldiff a b) b == 0
a, b:t
H:ldiff b a == 0
b <= a
 apply land_ldiff.a, b:t
H:ldiff b a == 0
b <= a
 now apply ldiff_le.
Qed.

We can express lnot in term of subtraction

Lemma add_lnot_diag_low : forall a n, log2 a < n ->
 a + lnot a n == ones n.forall a n : t, log2 a < n -> a + lnot a n == ones n
Proof.forall a n : t, log2 a < n -> a + lnot a n == ones n
 intros a n H.a, n:t
H:log2 a < n
a + lnot a n == ones n
 assert (H' := land_lnot_diag_low a n H).a, n:t
H:log2 a < n
H':land a (lnot a n) == 0
a + lnot a n == ones n
 rewrite add_nocarry_lxor, lxor_lor by trivial.a, n:t
H:log2 a < n
H':land a (lnot a n) == 0
lor a (lnot a n) == ones n
 now apply lor_lnot_diag_low.
Qed.

Lemma lnot_sub_low : forall a n, log2 a < n ->
 lnot a n == ones n - a.forall a n : t, log2 a < n -> lnot a n == ones n - a
Proof.forall a n : t, log2 a < n -> lnot a n == ones n - a
 intros a n H.a, n:t
H:log2 a < n
lnot a n == ones n - a
 now rewrite <- (add_lnot_diag_low a n H), add_comm, add_sub.
Qed.

Adding numbers with no common bits cannot lead to a much bigger number

Lemma add_nocarry_lt_pow2 : forall a b n, land a b == 0 ->
 a < 2^n -> b < 2^n -> a+b < 2^n.forall a b n : t,
land a b == 0 ->
a < 2 ^ n -> b < 2 ^ n -> a + b < 2 ^ n
Proof.forall a b n : t,
land a b == 0 ->
a < 2 ^ n -> b < 2 ^ n -> a + b < 2 ^ n
 intros a b n H Ha Hb.a, b, n:t
H:land a b == 0
Ha:a < 2 ^ n
Hb:b < 2 ^ n
a + b < 2 ^ n
 rewrite add_nocarry_lxor by trivial.a, b, n:t
H:land a b == 0
Ha:a < 2 ^ n
Hb:b < 2 ^ n
lxor a b < 2 ^ n
 apply div_small_iff.a, b, n:t
H:land a b == 0
Ha:a < 2 ^ n
Hb:b < 2 ^ n
2 ^ n ~= 0
a, b, n:t
H:land a b == 0
Ha:a < 2 ^ n
Hb:b < 2 ^ n
lxor a b / 2 ^ n == 0 order_nz.a, b, n:t
H:land a b == 0
Ha:a < 2 ^ n
Hb:b < 2 ^ n
lxor a b / 2 ^ n == 0
 rewrite <- shiftr_div_pow2, shiftr_lxor, !shiftr_div_pow2.a, b, n:t
H:land a b == 0
Ha:a < 2 ^ n
Hb:b < 2 ^ n
lxor (a / 2 ^ n) (b / 2 ^ n) == 0
 rewrite 2 div_small by trivial.a, b, n:t
H:land a b == 0
Ha:a < 2 ^ n
Hb:b < 2 ^ n
lxor 0 0 == 0
 apply lxor_0_l.
Qed.

Lemma add_nocarry_mod_lt_pow2 : forall a b n, land a b == 0 ->
 a mod 2^n + b mod 2^n < 2^n.forall a b n : t,
land a b == 0 -> a mod 2 ^ n + b mod 2 ^ n < 2 ^ n
Proof.forall a b n : t,
land a b == 0 -> a mod 2 ^ n + b mod 2 ^ n < 2 ^ n
 intros a b n H.a, b, n:t
H:land a b == 0
a mod 2 ^ n + b mod 2 ^ n < 2 ^ n
 apply add_nocarry_lt_pow2.a, b, n:t
H:land a b == 0
land (a mod 2 ^ n) (b mod 2 ^ n) == 0
a, b, n:t
H:land a b == 0
a mod 2 ^ n < 2 ^ n
a, b, n:t
H:land a b == 0
b mod 2 ^ n < 2 ^ n
 bitwise.a, b, n:t
H:land a b == 0
m:t
(a mod 2 ^ n).[m] && (b mod 2 ^ n).[m] = false
a, b, n:t
H:land a b == 0
a mod 2 ^ n < 2 ^ n
a, b, n:t
H:land a b == 0
b mod 2 ^ n < 2 ^ n
 destruct (le_gt_cases n m).a, b, n:t
H:land a b == 0
m:t
H0:n <= m
(a mod 2 ^ n).[m] && (b mod 2 ^ n).[m] = false
a, b, n:t
H:land a b == 0
m:t
H0:m < n
(a mod 2 ^ n).[m] && (b mod 2 ^ n).[m] = false
a, b, n:t
H:land a b == 0
a mod 2 ^ n < 2 ^ n
a, b, n:t
H:land a b == 0
b mod 2 ^ n < 2 ^ n
 now rewrite mod_pow2_bits_high.a, b, n:t
H:land a b == 0
m:t
H0:m < n
(a mod 2 ^ n).[m] && (b mod 2 ^ n).[m] = false
a, b, n:t
H:land a b == 0
a mod 2 ^ n < 2 ^ n
a, b, n:t
H:land a b == 0
b mod 2 ^ n < 2 ^ n
 now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0.a, b, n:t
H:land a b == 0
a mod 2 ^ n < 2 ^ n
a, b, n:t
H:land a b == 0
b mod 2 ^ n < 2 ^ n
 apply mod_upper_bound; order_nz.a, b, n:t
H:land a b == 0
b mod 2 ^ n < 2 ^ n
 apply mod_upper_bound; order_nz.
Qed.

End NBitsProp.