Library BVlib
Non-random bit-vector definitions and lemmas
Set Implicit Arguments.
Require Import Setoid.
Require Import Arith.
Require Import Omega.
Require Export Bvector.
Require Export Bools.
Implicit Arguments Vcons [A n].
Implicit Arguments Vhead [A n].
Implicit Arguments Vtail [A n].
Implicit Arguments Vconst [A].
Implicit Arguments Vunary [A n].
Implicit Arguments Vbinary [A n].
Lemma VS_eq :
forall n, forall w : Bvector (S n),
exists hd, exists tl, w = Vcons hd tl.
Proof.
intros.
exists (Vhead w).
exists (Vtail w).
rewrite (VSn_eq _ _ w).
reflexivity.
Qed.
Ltac VS_rewrite x :=
let hd := fresh x "_hd" in let tl := fresh x "_tl" in let H := fresh x "Heq" in
destruct (VS_eq x) as (hd,(tl,H)); rewrite H in *|-*; clear H; clear x.
Lemma Vcons_injective :
forall a c n (b d : Bvector n), Vcons a b = Vcons c d -> a=c /\ b=d.
Proof.
intros.
split.
change a with (Vhead (Vcons a b)).
change c with (Vhead (Vcons c d)).
f_equal; assumption.
change b with (Vtail (Vcons a b)).
change d with (Vtail (Vcons c d)).
f_equal; assumption.
Qed.
Notation map2 := (Vbinary (A:=bool)).
Notation map := (Vunary (A:=bool)).
Notation BVtrue := (Vconst true).
Notation BVfalse := (Vconst false).
Notation BVand := (map2 andb).
Notation BVor := (map2 orb).
Notation "u && v" := (BVand u v).
Notation "u || v" := (BVor u v).
Notation "u ++ v" := (BVxor _ u v).
Notation "~~ u" := (Bneg _ u) (at level 35).
Theorem map_map :
forall f g n (v : Bvector n), map f (map g v) = map (fun x => f (g x)) v.
Proof.
intros f g n; induction v; simpl.
reflexivity.
rewrite IHv; reflexivity.
Qed.
Theorem map_id : forall n (v : Bvector n), map (fun x:bool => x) v = v.
Proof.
induction v; intros; simpl.
reflexivity.
rewrite IHv; reflexivity.
Qed.
Require Import AAC_tactics.AAC.
Require Import AAC_tactics.Instances.
Import Bool.
Instance xorb_assoc : Associative eq xorb.
Proof.
unfold Associative; intros.
destruct x; destruct y; destruct z; reflexivity.
Qed.
Instance xorb_comm : Commutative eq xorb.
Proof.
unfold Commutative; intros.
destruct x; destruct y; reflexivity.
Qed.
Instance xorb_unit : Unit eq xorb false.
Proof.
constructor; intros; destruct x; reflexivity.
Qed.
Instance le_refl : Reflexive le := le_refl.
Instance le_trans : Transitive le := le_trans.
Instance map2_comm :
forall n f, Commutative eq f -> Commutative eq (map2 f (n:=n)).
Proof.
intros n f H; induction n; unfold Commutative; intros.
trivial.
VS_rewrite x; VS_rewrite y; simpl Vbinary.
congruence.
Qed.
Instance map2_assoc :
forall n f, Associative eq f -> Associative eq (map2 f (n:=n)).
Proof.
intros n f H; induction n; unfold Associative; intros.
trivial.
VS_rewrite x; VS_rewrite y; VS_rewrite z; simpl Vbinary.
congruence.
Qed.
Goal forall n (x y z:Bvector n), x || (y && z) = (z && y) || x.
Proof.
intros; aac_reflexivity.
Qed.
Instance map2_unit :
forall f u, Unit eq f u -> forall n, Unit eq (map2 f (n:=n)) (Vconst u n).
Proof.
intros; induction n; intros.
constructor; intro x; simpl Vbinary; rewrite (V0_eq _ x); reflexivity.
constructor; intro x; VS_rewrite x; simpl Vbinary.
destruct H as [ H _ ]; rewrite H.
destruct IHn as [ IHn _ ]; rewrite IHn; reflexivity.
destruct H as [ _ H ]; rewrite H.
destruct IHn as [ _ IHn ]; rewrite IHn; reflexivity.
Qed.
Goal forall n x, BVxor n x ((BVfalse n) && (BVtrue n)) = x.
Proof.
intros; aac_reflexivity.
Qed.
Class Duality {A} (opp : A -> A) :=
{ involutive : forall x:A, opp (opp x) = x }.
Goal forall A (opp:A->A), Duality opp -> forall x, exists y, x = opp y.
Proof.
intros.
exists (opp x).
rewrite involutive.
reflexivity.
Qed.
Instance proper_map :
Proper (pointwise_relation _ eq ==> forall_relation (fun n => eq ==> eq)) map.
Proof.
unfold Proper.
intros f g H.
intros n u v Huv.
rewrite Huv.
induction u; [ rewrite (V0_eq _ v) | VS_rewrite v ].
reflexivity.
simpl.
rewrite H.
inversion Huv.
rewrite IHu; reflexivity.
Qed.
Instance duality_lift :
forall (opp:bool->bool), Duality opp -> forall n, Duality (map opp (n:=n)).
Proof.
constructor; intros.
rewrite map_map.
rewrite proper_map with (y0:=x) (y:=(fun x:bool=>x)); [
| setoid_rewrite involutive; reflexivity
| reflexivity ].
apply map_id.
Qed.
Class DeMorgan {A} (opp : A -> A) (f : A -> A -> A) (f' : A -> A -> A) :=
{ demorgan : forall x y, opp (f x y) = f' (opp x) (opp y) }.
Instance demorgan_lift :
forall opp f g, DeMorgan opp f g
-> forall n, DeMorgan (map opp (n:=n)) (map2 f (n:=n)) (map2 g (n:=n)).
Proof.
constructor; intros.
induction x; [ rewrite (V0_eq _ y) | VS_rewrite y ]; simpl.
reflexivity.
rewrite demorgan.
rewrite IHx.
reflexivity.
Qed.
Instance negb_duality : Duality negb.
Proof.
constructor.
intros.
destruct x; reflexivity.
Qed.
Instance andb_orb_duals : DeMorgan negb andb orb.
Proof.
constructor.
intros x y.
destruct x; destruct y; reflexivity.
Qed.
Instance orb_andb_duals : DeMorgan negb orb andb.
Proof.
constructor.
intros x y.
destruct x; destruct y; reflexivity.
Qed.
Ltac BVsimpl := repeat first [ rewrite involutive | rewrite demorgan ].
Goal forall n (u v : Bvector n), ~~ (u && ~~ v) = ~~ u || v.
Proof.
intros.
BVsimpl.
reflexivity.
Qed.
Theorem BVxor_nilpotent : forall n v, BVxor n v v = BVfalse n.
Proof.
induction v; intros.
reflexivity.
simpl.
rewrite xorb_nilpotent.
congruence.
Qed.
Theorem and_xor_not : forall a b, andb a (xorb (negb a) b) = andb a b.
Proof.
intros; destruct a; destruct b; reflexivity.
Qed.
Theorem BVand_xor_not :
forall n (a b : Bvector n), a && ((~~ a) ++ b) = a && b.
Proof.
intros; induction a; [ rewrite (V0_eq _ b) | VS_rewrite b ]; simpl.
reflexivity.
rewrite and_xor_not.
congruence.
Qed.
Theorem neg_xor : forall a b, negb (xorb a b) = xorb (negb a) b.
Proof.
intros; destruct a, b; reflexivity.
Qed.
Theorem BVneg_xor : forall n (a b : Bvector n), Bneg _ (BVxor _ a b) = BVxor _ (Bneg _ a) b.
Proof.
intros; induction n.
auto.
VS_rewrite a; VS_rewrite b; simpl; rewrite neg_xor; rewrite IHn; reflexivity.
Qed.
Lemma BVand_empty : forall n (u v : Bvector n), u && v = BVfalse _ -> u && ~~v = u.
Proof.
intros; induction u; intros; [rewrite (V0_eq _ v)|VS_rewrite v]; simpl.
reflexivity.
simpl in H.
destruct (Vcons_injective H).
rewrite (IHu v_tl) by assumption.
destruct a; destruct v_hd; first [discriminate|reflexivity].
Qed.
Theorem BVand_or_distrib_r :
forall n (v1 v2 v3 : Bvector n), v1 && (v2 || v3) = (v1 && v2) || (v1 && v3).
Proof.
induction n; intros;
[ rewrite (V0_eq _ v1); rewrite (V0_eq _ v2); rewrite (V0_eq _ v3)
| VS_rewrite v1; VS_rewrite v2; VS_rewrite v3 ]; simpl.
reflexivity.
rewrite andb_orb_distrib_r; rewrite IHn; reflexivity.
Qed.
Theorem BVand_or_distrib_l :
forall n (v1 v2 v3 : Bvector n), (v1 || v2) && v3 = (v1 && v3) || (v2 && v3).
Proof.
intros.
aac_rewrite (BVand_or_distrib_r v3 v1 v2).
aac_reflexivity.
Qed.
Theorem BVand_neg_false : forall n (v : Bvector n), v && (~~ v) = BVfalse n.
Proof.
induction v; intros; simpl.
reflexivity.
rewrite IHv.
destruct a; reflexivity.
Qed.
Theorem BVor_neg_true : forall n (v : Bvector n), v || (~~ v) = BVtrue n.
Proof.
induction v; intros; simpl.
reflexivity.
rewrite IHv.
destruct a; reflexivity.
Qed.
Theorem BVand_false : forall n (v : Bvector n), (BVfalse n) && v = BVfalse n.
Proof.
induction v; intros; simpl.
reflexivity.
rewrite IHv.
destruct a; reflexivity.
Qed.
Theorem BVor_true : forall n (v : Bvector n), (BVtrue n) || v = BVtrue n.
Proof.
induction v; intros; simpl.
reflexivity.
rewrite IHv.
destruct a; reflexivity.
Qed.
Goal forall n (v v' : Bvector n), v && (v' && ~~ v) = BVfalse _.
Proof.
intros.
aac_rewrite (BVand_neg_false v).
aac_rewrite (BVand_false v').
reflexivity.
Qed.
Goal forall n (y K K' : Bvector n),
y = (~~ K') && K ->
K = K' && (~~ K' || K) || y.
Proof.
intros.
assert (K' && ((~~ K') || K) || y = y || (K && K')).
rewrite (BVand_or_distrib_r K' (~~ K') K).
rewrite (BVand_neg_false K').
aac_reflexivity.
rewrite H0.
rewrite H.
symmetry.
aac_rewrite <- (BVand_or_distrib_r K).
rewrite (BVor_neg_true K').
aac_reflexivity.
Qed.
Fixpoint BVeq n m l l' :=
match l with
| Vnil => true
| Vcons hd m tl =>
match l' with
| Vnil => false
| Vcons hd' m' tl' =>
if bool_eq hd hd' then BVeq m m' tl tl' else false
end
end.
Theorem BVeq_eq_true : forall n (l l' : Bvector n), BVeq l l' = true <-> l = l'.
Proof.
intros; split; intro H.
induction l; [rewrite (@V0_eq _ l')|VS_rewrite l'].
reflexivity.
simpl in H.
destruct (bool_dec a l'_hd) as [ Heq | Hneq ].
rewrite Heq.
rewrite <- bool_eq_eq in Heq.
rewrite Heq in H.
rewrite (IHl l'_tl H).
reflexivity.
rewrite <- bool_eq_neq in Hneq.
rewrite Hneq in H.
discriminate.
rewrite <- H; clear H l'.
induction l.
reflexivity.
simpl; rewrite IHl.
assert (bool_eq a a = true) as H by (apply bool_eq_eq; reflexivity).
rewrite H; reflexivity.
Qed.
Definition Bvector_eq_dec : forall n (l l' : Bvector n), {l=l'}+{l<>l'}.
Proof.
intros.
case_eq (BVeq l l'); intros.
rewrite BVeq_eq_true in H.
left; assumption.
right; intro.
rewrite <- BVeq_eq_true in H0.
rewrite H0 in H.
discriminate.
Qed.
Fixpoint occurrences n (l : Bvector n) b :=
match l in vector _ n return nat with
| Vcons hd m tl => if bool_dec hd b then S (occurrences tl b) else occurrences tl b
| Bnil => O
end.
Definition occs_1 n v := @occurrences n v true.
Lemma occs_1_true : forall n (v:Bvector n), (occurrences (Vcons true v) true) = S (occurrences v true).
Proof.
trivial.
Qed.
Lemma occs_1_false : forall n (v:Bvector n), (occurrences (Vcons false v) true) = occurrences v true.
Proof.
trivial.
Qed.
Lemma occurrences_const :
forall b b' n, occurrences (Vconst b n) b' = if bool_dec b b' then n else 0.
Proof.
intros b b' n.
induction n; simpl.
destruct (bool_dec b b'); reflexivity.
rewrite IHn.
destruct (bool_dec b b'); reflexivity.
Qed.
Lemma occs_1_BVand : forall n (u v : Bvector n), occs_1 (u && v) <= occs_1 u.
Proof.
unfold occs_1.
induction n; intros;
[ rewrite (V0_eq _ u); rewrite (V0_eq _ v) | VS_rewrite u; VS_rewrite v ].
reflexivity.
simpl.
assert (occurrences (u_tl && v_tl) true <= occurrences u_tl true) by apply IHn.
destruct u_hd; destruct v_hd; simpl; omega.
Qed.
Theorem occurrences_length_le : forall n l b, @occurrences n l b <= n.
Proof.
intros; induction l.
trivial.
simpl; case (bool_dec a b); intros _; omega.
Qed.
Theorem occurrences_Vconst :
forall b n (v : Bvector n), occurrences v b = 0 <-> v = Vconst (negb b) n.
Proof.
intros; split.
induction v; simpl; intros.
reflexivity.
destruct (bool_dec a b); [discriminate|].
f_equal.
destruct a, b; simpl; first [reflexivity|elim (n0 (refl_equal _))].
rewrite (IHv H); reflexivity.
intro H; rewrite H; clear H v.
induction n; simpl.
reflexivity.
destruct (bool_dec (negb b) b); [elim (no_fixpoint_negb _ e)|].
exact IHn.
Qed.
Corollary occurrences_true_0 :
forall n w, occurrences w true = 0%nat -> w = Vconst false n.
Proof.
intros.
rewrite occurrences_Vconst in H.
rewrite H; reflexivity.
Qed.
Theorem Bneg_occs_1 : forall n (v : Bvector n), occs_1 (Bneg n v) = n - occs_1 v.
Proof.
unfold occs_1.
intros; induction v.
reflexivity.
destruct a; simpl occurrences; rewrite IHv.
reflexivity.
assert (occurrences v true <= n) by apply occurrences_length_le.
omega.
Qed.
Definition dist n O O' := occs_1 (BVxor n O O').
Theorem dist_BVxor :
forall n, forall (O O' O'' : Bvector n), dist (BVxor _ O O') (BVxor _ O' O'') = dist O O''.
Proof.
intros.
unfold dist; unfold occs_1.
f_equal.
aac_rewrite (BVxor_nilpotent O').
aac_reflexivity.
Qed.
Number of bits set in K but not in K'.
Definition missing n (K K' : Bvector n) := occs_1 (K && (~~ K')).
Theorem missing_true : forall n b (K K' : Bvector n),
missing (Vcons b K) (Vcons true K') = missing K K'.
Proof.
intros.
destruct b; reflexivity.
Qed.
Theorem missing_false : forall n b (K K' : Bvector n),
missing (Vcons false K) (Vcons b K') = missing K K'.
Proof.
intros.
destruct b; reflexivity.
Qed.
Theorem missing_S : forall n (K K' : Bvector n),
missing (Vcons true K) (Vcons false K') = S (missing K K').
Proof.
intros; reflexivity.
Qed.
Theorem missing_le_occs : forall n (K K' : Bvector n), missing K K' <= occs_1 K.
Proof.
unfold missing, occs_1.
intro n; induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); reflexivity.
VS_rewrite K; VS_rewrite K'; destruct K_hd; destruct K'_hd; simpl; auto.
apply le_n_S.
apply IHn.
Qed.
Theorem missing_le_not_occs : forall n (K K' : Bvector n), missing K K' <= n - occs_1 K'.
Proof.
unfold missing, occs_1.
intro n; induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); reflexivity.
VS_rewrite K; VS_rewrite K'; destruct K_hd; destruct K'_hd; simpl BVand; simpl occurrences;
try apply le_n_S; try apply le_trans with (1 := IHn K_tl K'_tl); try omega; auto.
rewrite <- minus_Sn_m by apply occurrences_length_le.
apply le_n_S.
apply IHn.
Qed.
Theorem occs_plus_missing :
forall n (K K' : Bvector n), occs_1 K' + missing K K' = occs_1 K + missing K' K.
Proof.
unfold missing, occs_1.
induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); auto.
VS_rewrite K; VS_rewrite K'.
destruct K_hd, K'_hd; simpl;
repeat first [ rewrite occs_1_true | rewrite occs_1_false | rewrite <- plus_n_Sm ];
rewrite (IHn K_tl K'_tl); reflexivity.
Qed.
Corollary missing_occs_le : forall n K K', @missing n K K' = 0 -> occs_1 K <= occs_1 K'.
Proof.
intros.
assert (occs_1 K' + missing K K' = occs_1 K + missing K' K) by apply occs_plus_missing.
omega.
Qed.
Theorem occs_missing : forall n (K K' : Bvector n),
occs_1 (BVxor _ K K') = missing K' K + missing K K'.
Proof.
unfold missing, occs_1.
induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); auto.
VS_rewrite K; VS_rewrite K'.
destruct K_hd, K'_hd; simpl;
repeat first [ rewrite occs_1_true | rewrite occs_1_false | rewrite <- plus_n_Sm ];
rewrite (IHn K_tl K'_tl); reflexivity.
Qed.
Theorem missing_BVand : forall n (K K' : Bvector n), missing (K && K') K' = 0.
Proof.
unfold missing, occs_1.
induction n; intros; [ rewrite (V0_eq _ K); rewrite (V0_eq _ K') |
VS_rewrite K; VS_rewrite K' ].
reflexivity.
simpl.
rewrite IHn.
destruct K_hd; destruct K'_hd; reflexivity.
Qed.
Theorem missing_0_tl : forall n (K K' : Bvector (S n)),
missing K K' = 0 -> missing (Vtail K) (Vtail K') = 0.
Proof.
unfold missing; unfold occs_1; intros n K K'.
VS_rewrite K; VS_rewrite K'; simpl.
destruct (bool_dec (K_hd && negb K'_hd) true).
discriminate.
intro H; exact H.
Qed.
Theorem missing_true : forall n b (K K' : Bvector n),
missing (Vcons b K) (Vcons true K') = missing K K'.
Proof.
intros.
destruct b; reflexivity.
Qed.
Theorem missing_false : forall n b (K K' : Bvector n),
missing (Vcons false K) (Vcons b K') = missing K K'.
Proof.
intros.
destruct b; reflexivity.
Qed.
Theorem missing_S : forall n (K K' : Bvector n),
missing (Vcons true K) (Vcons false K') = S (missing K K').
Proof.
intros; reflexivity.
Qed.
Theorem missing_le_occs : forall n (K K' : Bvector n), missing K K' <= occs_1 K.
Proof.
unfold missing, occs_1.
intro n; induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); reflexivity.
VS_rewrite K; VS_rewrite K'; destruct K_hd; destruct K'_hd; simpl; auto.
apply le_n_S.
apply IHn.
Qed.
Theorem missing_le_not_occs : forall n (K K' : Bvector n), missing K K' <= n - occs_1 K'.
Proof.
unfold missing, occs_1.
intro n; induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); reflexivity.
VS_rewrite K; VS_rewrite K'; destruct K_hd; destruct K'_hd; simpl BVand; simpl occurrences;
try apply le_n_S; try apply le_trans with (1 := IHn K_tl K'_tl); try omega; auto.
rewrite <- minus_Sn_m by apply occurrences_length_le.
apply le_n_S.
apply IHn.
Qed.
Theorem occs_plus_missing :
forall n (K K' : Bvector n), occs_1 K' + missing K K' = occs_1 K + missing K' K.
Proof.
unfold missing, occs_1.
induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); auto.
VS_rewrite K; VS_rewrite K'.
destruct K_hd, K'_hd; simpl;
repeat first [ rewrite occs_1_true | rewrite occs_1_false | rewrite <- plus_n_Sm ];
rewrite (IHn K_tl K'_tl); reflexivity.
Qed.
Corollary missing_occs_le : forall n K K', @missing n K K' = 0 -> occs_1 K <= occs_1 K'.
Proof.
intros.
assert (occs_1 K' + missing K K' = occs_1 K + missing K' K) by apply occs_plus_missing.
omega.
Qed.
Theorem occs_missing : forall n (K K' : Bvector n),
occs_1 (BVxor _ K K') = missing K' K + missing K K'.
Proof.
unfold missing, occs_1.
induction n; intros.
rewrite (V0_eq _ K); rewrite (V0_eq _ K'); auto.
VS_rewrite K; VS_rewrite K'.
destruct K_hd, K'_hd; simpl;
repeat first [ rewrite occs_1_true | rewrite occs_1_false | rewrite <- plus_n_Sm ];
rewrite (IHn K_tl K'_tl); reflexivity.
Qed.
Theorem missing_BVand : forall n (K K' : Bvector n), missing (K && K') K' = 0.
Proof.
unfold missing, occs_1.
induction n; intros; [ rewrite (V0_eq _ K); rewrite (V0_eq _ K') |
VS_rewrite K; VS_rewrite K' ].
reflexivity.
simpl.
rewrite IHn.
destruct K_hd; destruct K'_hd; reflexivity.
Qed.
Theorem missing_0_tl : forall n (K K' : Bvector (S n)),
missing K K' = 0 -> missing (Vtail K) (Vtail K') = 0.
Proof.
unfold missing; unfold occs_1; intros n K K'.
VS_rewrite K; VS_rewrite K'; simpl.
destruct (bool_dec (K_hd && negb K'_hd) true).
discriminate.
intro H; exact H.
Qed.