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 p ⇒ inleft (exist _ (Npos p) eq_refl)
| Z0 ⇒ inleft (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)*b → a×b ≤ c×d.
Lemma Zmult_split : ∀ a b c d,
a×b ≤ 0 → 0 ≤ c×d → a×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, {x≥0}+{x<0}.
Lemma Zpos_strict_or_not : ∀ x : Z, {x>0}+{x≤0}.
Hint Resolve Zmult_bounds1 Zmult_ineq1.
Lemma Zmult_interval_right_mid : ∀ a b c d x y,
a ≤ x ≤ b →
c ≤ y ≤ d →
0 ≤ a → c < 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 →
0 ≤ a → d < 0 →
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 ≤ b → c ≤ 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)%nat → Z_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 = false → x > y ∨ z > t.
Lemma add_signed_unsigned : ∀ x y,
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 < - y → y < x.
Lemma z_le_neg_ge x y : - x ≤ - y → y ≤ x.
Lemma zdiv_lt : ∀ x y z, z > 0 → x < 0 ≤ y → x / 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.
Open Scope error_monad_scope.
Definition get_opt {A} (a:option A) (msg:string) : res A :=
match a with
| None ⇒ Error (MSG msg::nil)
| Some a ⇒ OK a
end.
Lemma fold_left_cons_map_app {A B:Type} (f: A → B) :
∀ (l: list A) (k: list B),
fold_left (fun acc a ⇒ f a :: acc) l k = rev (map f l) ++ k.
Lemma flat_map_app {A B: Type} (f: A → list B) :
∀ l m,
flat_map f (l ++ m) = flat_map f l ++ flat_map f m.
Lemma aux {A B C:Type} (f: A → B → C) :
∀ (l: list A) (m: list B) (k: list C),
fold_left (fun acc a ⇒ rev (map (f a) m) ++ acc) l k =
rev (flat_map (fun a ⇒ map (f a) m) l) ++ k.
Lemma aux' {A B C D: Type} (f: A → B → C → D) :
∀ (l: list A) (m: list B) (n: list C) (k: list D),
fold_left (fun acc a ⇒ rev (flat_map (fun b ⇒ map (f a b) n) m) ++ acc) l k =
rev (flat_map (fun a ⇒ flat_map (fun b ⇒ map (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:Z→Type) x y,
(x≤y → P x) → (y≤x → P y )-> P (Zmin x y).
Lemma case_Zmax : ∀ (P:Z→Type) x y,
(y≤x → P x) → (x≤y → P 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 ≤ b → c < 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)).