# Library DLib

Utility definitions by David.

Require Import Utf8.
Require Import Coqlib.

Tactic Notation ">" tactic(t) := t.
Tactic Notation "by" tactic(t) := t; fail "this goal should be proved at this point".

Ltac destruct_bool_in_goal :=
match goal with [ |- context[if ?x then _ else _]] ⇒ destruct x end.
Ltac destruct_option_in_goal :=
match goal with [ |- context[match ?x with Some __ | None_ end]] ⇒ destruct x end.
Ltac case_eq_bool_in_goal :=
match goal with [ |- context[if ?x then _ else _]] ⇒ case_eq x end.
Ltac case_eq_option_in_goal :=
match goal with [ |- context[match ?x with Some __ | None_ end]] ⇒ case_eq x end.
Ltac destruct_bool :=
match goal with
[ _ : context[if ?x then _ else _] |- _] ⇒ destruct x
| [ |- context[if ?x then _ else _]] ⇒ destruct x
end.
Ltac destruct_option :=
match goal with
[ _ : context[match ?x with Some __ | None_ end] |- _] ⇒ destruct x
| [ |- context[match ?x with Some __ | None_ end]] ⇒ destruct x
end.

Ltac simpl_option :=
match goal with
[ id : Some _ = Some _ |- _ ] ⇒ inv id
| [ id : None = Some _ |- _ ] ⇒ inv id
| [ id : Some _ = None |- _ ] ⇒ inv id
end.

Ltac bif :=
match goal with |- context[if ?a then _ else _] ⇒ destruct a end; try congruence.

Ltac bif' :=
match goal with |- context[if ?a then _ else _] ⇒ destruct a eqn: ? end; try congruence.

Ltac pairs :=
repeat
match goal with
| |- context[let '(_,_) := ?x in _] ⇒
case_eq x; intros ? ?
end.

Ltac autorw :=
match goal with
| [H: _ = _ |- _] ⇒ rewrite H in ×
end.

Ltac autorw' := repeat (progress (autorw; subst)).

Ltac inj :=
repeat
match goal with
| [H : ?f _ = ?f _ |- _] ⇒ injection H; intros ?; subst; clear H
| [H : ?f _ _ = ?f _ _ |- _] ⇒ injection H; intros ? ?; subst; clear H
end.

Require Import ZArith.
Require Psatz.

Open Scope Z_scope.

Ltac elim_div :=
unfold Zdiv, Zmod;
repeat
match goal with
| H : context[ Zdiv_eucl ?X ?Y ] |- _
generalize (Z_div_mod_full X Y) ; destruct (Zdiv_eucl X Y)
| |- context[ Zdiv_eucl ?X ?Y ] ⇒
generalize (Z_div_mod_full X Y) ; destruct (Zdiv_eucl X Y)
end; unfold Remainder.

Definition znegb (x: Z) : { x < 0 } + { x 0 }.

Definition z2n (z: Z) : { n : N | Z.of_N n = z } + {z < 0} :=
match z with
| Zpos pinleft (exist _ (Npos p) eq_refl)
| Z0inleft (exist _ N0 eq_refl)
| _inright eq_refl
end.

Lemma Zmult_bounds1 : x1 x2 y1 y2 : Z,
0 x1 x2
0 y1 y2
x1 × y1 x2 × y2.

Lemma Zmult_opp : x y : Z, x×y=(-x)*(-y).

Lemma Zmult_bounds2 : x1 x2 y1 y2 : Z,
x1 x2 0->
y1 y2 0 →
x2 × y2 x1 × y1.

Lemma Zmult_interval_right_right : a b c d x y,
a x b
c y d
0 a → 0 c
a×c x×y b×d.

Lemma Zmult_ineq1 : a b c d,
c*(-d) a*(-b)a×b c×d.

Lemma Zmult_ineq2 : a b c d,
(-c)*d (-a)*ba×b c×d.

Lemma Zmult_split : a b c d,
a×b 0 → 0 c×da×b c×d.
Hint Resolve Zmult_split Zmult_ineq1.

Lemma sign_rule1 : x y : Z,
x 0 → y 0 → x × y 0.
Lemma sign_rule2 : x y : Z,
x 0 → y 0 → 0 x × y.
Lemma sign_rule3 : x y : Z,
x 0 → y 0 → 0 x × y.
Lemma sign_rule4 : x y : Z,
x 0 → y 0 → x × y 0.
Hint Resolve sign_rule1 sign_rule2 sign_rule3 sign_rule4 : sign.

Lemma Zpos_or_not : x : Z, {x0}+{x<0}.

Lemma Zpos_strict_or_not : x : Z, {x>0}+{x0}.

Hint Resolve Zmult_bounds1 Zmult_ineq1.

Lemma Zmult_interval_right_mid : a b c d x y,
a x b
c y d
0 ac < 0 → 0 d
b×c x×y b×d.

Hint Resolve Zmult_bounds2 Zmult_ineq2.

Lemma Zmult_interval_left_mid : a b c d x y,
a x b
c y d
b < 0 → c < 0 → 0 d
a×d x×y a×c.

Lemma Zmult_interval_right_left : a b c d x y,
a x b
c y d
b×c x×y a×d.

Lemma Zmult_interval_left_left : a b c d x y,
a x b
c y d
b < 0 → d < 0 →
b×d x×y a×c.

Lemma Z_max_le_r : x y : Z, y (Zmax x y).

Lemma Z_max_le_l : x y : Z, x (Zmax x y).

Hint Resolve Zle_min_l Zle_min_r Z_max_le_l Z_max_le_r.

Lemma ineq_trans : a b c d e : Z,
a bc d
b e c
a e d.

Lemma Z_min4_le_1 : x y z t: Z, Zmin (Zmin x y) (Zmin z t) x.

Lemma Z_min4_le_2 : x y z t: Z, Zmin (Zmin x y) (Zmin z t) y.

Lemma Z_min4_le_3 : x y z t: Z, Zmin (Zmin x y) (Zmin z t) z.

Lemma Z_min4_le_4 : x y z t: Z, Zmin (Zmin x y) (Zmin z t) t.

Lemma Z_max4_le_1 : x y z t: Z, x Zmax (Zmax x y) (Zmax z t).

Lemma Z_max4_le_2 : x y z t: Z, y Zmax (Zmax x y) (Zmax z t).

Lemma Z_max4_le_3 : x y z t: Z, z Zmax (Zmax x y) (Zmax z t).

Lemma Z_max4_le_4 : x y z t: Z, t Zmax (Zmax x y) (Zmax z t).

Hint Resolve Z_max4_le_1 Z_max4_le_2 Z_max4_le_3 Z_max4_le_4
Z_min4_le_1 Z_min4_le_2 Z_min4_le_3 Z_min4_le_4.

Require Import compcert.Integers.

Ltac compute_this val :=
let x := fresh in set val as x in *; vm_compute in x; subst x.

Ltac smart_omega :=
compute_this Int.modulus; compute_this Int.half_modulus;
compute_this Int.max_unsigned;
compute_this Int.min_signed; compute_this Int.max_signed;
omega.

Lemma repr_mod_prop: x y,
Int.repr (x + y × Int.modulus) = Int.repr x.

Lemma Z_of_nat_gt: n, (n > 0)%natZ_of_nat n > 0.

Lemma sign_ext_same : n m i,
(m > 0)%nat
Int.wordsize = ((S n)+m)%nat
-(two_power_nat n) Int.signed i (two_power_nat n) -1 →
Int.sign_ext (Z_of_nat (S n)) i = i.

Lemma zero_ext_same : n m i,
(m > 0)%nat
Int.wordsize = (n+m)%nat
0 Int.signed i (two_power_nat n) -1 →
Int.zero_ext (Z_of_nat n) i = i.

Lemma two_power_nat_div2 : n,
two_power_nat (S n) / 2 = two_power_nat n.

Lemma pow2_pos n : n > 0 2 ^ n > 0.

Lemma neg_signed_unsigned : x,
Int.repr (- (Int.signed x)) = Int.repr (- (Int.unsigned x)).

Lemma zle_and_case: x y z t,
zle x y && zle z t = falsex > y z > t.

Int.repr (Int.signed x + Int.signed y) = Int.repr (Int.unsigned x + Int.unsigned y).

Lemma sub_signed_unsigned : x y,
Int.repr (Int.signed x - Int.signed y) = Int.repr (Int.unsigned x - Int.unsigned y).

Lemma mult_signed_unsigned : x y,
Int.repr (Int.signed x × Int.signed y) = Int.repr (Int.unsigned x × Int.unsigned y).

Lemma zle_true_iff : x y: Z,
proj_sumbool (zle x y) = true x y.

Lemma unsigned_inj i j : i j Int.unsigned i Int.unsigned j.

Lemma signed_inj i j : i j Int.signed i Int.signed j.

Lemma signed_le_unsigned x :
Int.signed x Int.unsigned x.

Lemma signed_pos_unsigned {x} :
0 Int.signed x Int.signed x = Int.unsigned x.

Lemma mod_sub : x M, M > 0
M x < M + M - 1
x mod M = x - M.

Lemma z_lt_neg_gt x y : - x < - yy < x.

Lemma z_le_neg_ge x y : - x - yy x.

Lemma zdiv_lt : x y z, z > 0 → x < 0 yx / z < y / z.

Lemma zdiv_mono : x z : Z, x < -1 z > 0 x x / z.

Lemma ltlt i j :
Int.min_signed i Int.max_signed
Int.lt (Int.repr i) j = false
Int.signed j i.

Lemma ltlt' i j :
Int.min_signed i Int.max_signed
Int.lt j (Int.repr i) = false
i Int.signed j.

Require Import Errors.
Require Import String.

Definition get_opt {A} (a:option A) (msg:string) : res A :=
match a with
| NoneError (MSG msg::nil)
| Some aOK a
end.

Lemma fold_left_cons_map_app {A B:Type} (f: AB) :
(l: list A) (k: list B),
fold_left (fun acc af a :: acc) l k = rev (map f l) ++ k.

Lemma flat_map_app {A B: Type} (f: Alist B) :
l m,
flat_map f (l ++ m) = flat_map f l ++ flat_map f m.

Lemma aux {A B C:Type} (f: ABC) :
(l: list A) (m: list B) (k: list C),
fold_left (fun acc arev (map (f a) m) ++ acc) l k =
rev (flat_map (fun amap (f a) m) l) ++ k.

Lemma aux' {A B C D: Type} (f: ABCD) :
(l: list A) (m: list B) (n: list C) (k: list D),
fold_left (fun acc arev (flat_map (fun bmap (f a b) n) m) ++ acc) l k =
rev (flat_map (fun aflat_map (fun bmap (f a b) n) m) l) ++ k.

Lemma minus_4_lt (p: positive) :
(Z.to_nat (Zpos p - 4) < Z.to_nat (Zpos p))%nat.

Lemma case_Zmin : (P:ZType) x y,
(xyP x) → (yxP y )-> P (Zmin x y).

Lemma case_Zmax : (P:ZType) x y,
(yxP x) → (xyP y )-> P (Zmax x y).

Lemma Zmult_interval_mid_mid : a b c d x y,
a x b
c y d
a < 0 → 0 bc < 0 → 0 d
Zmin (b×c) (a×d) x×y Zmax (a×c) (b×d).

Lemma Mult_interval_correct_min_max : a b c d x y : Z,
a x b
c y d
Zmin (Zmin (a×c) (b×d)) (Zmin (b×c) (a×d)) x × y
Zmax (Zmax (a×c) (b×d)) (Zmax (b×c) (a×d)).