Library Coq.omega.PreOmega
Z.div_mod_to_equations, Z.quot_rem_to_equations, Z.to_euclidean_division_equations: the tactics for preprocessing Z.div and Z.modulo, Z.quot and Z.rem
Module Z.
Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
Lemma div_0_r_ext x y : y = 0 -> x / y = 0.
Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x.
Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0.
Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y.
Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y.
Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0.
Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0.
Ltac div_mod_to_equations_generalize x y :=
pose proof (Z.div_mod x y);
pose proof (Z.mod_pos_bound x y);
pose proof (Z.mod_neg_bound x y);
pose proof (div_0_r_ext x y);
pose proof (mod_0_r_ext x y);
let q := fresh "q" in
let r := fresh "r" in
set (q := x / y) in *;
set (r := x mod y) in *;
clearbody q r.
Ltac quot_rem_to_equations_generalize x y :=
pose proof (Z.quot_rem' x y);
pose proof (rem_bound_pos_pos x y);
pose proof (rem_bound_pos_neg x y);
pose proof (rem_bound_neg_pos x y);
pose proof (rem_bound_neg_neg x y);
pose proof (quot_0_r_ext x y);
pose proof (rem_0_r_ext x y);
let q := fresh "q" in
let r := fresh "r" in
set (q := Z.quot x y) in *;
set (r := Z.rem x y) in *;
clearbody q r.
Ltac div_mod_to_equations_step :=
match goal with
| [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y
| [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y
| [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y
| [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y
end.
Ltac quot_rem_to_equations_step :=
match goal with
| [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y
| [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y
| [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
| [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
end.
Ltac div_mod_to_equations' := repeat div_mod_to_equations_step.
Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step.
Ltac euclidean_division_equations_cleanup :=
repeat match goal with
| [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
| [ H : ?x <> ?x -> _ |- _ ] => clear H
| [ H : ?x < ?x -> _ |- _ ] => clear H
| [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
| [ H : ?T -> _, H' : ~?T |- _ ] => clear H
| [ H : ~?T -> _, H' : ?T |- _ ] => clear H
| [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl)
| [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H
| [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H
| [ H : ?A -> ?B -> _, H' : ?B |- _ ] => specialize (fun a => H a H')
| [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H
| [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H
| [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
| [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
| [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
| [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
| [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
| [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
| [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
| [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
| [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
| [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
| [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
| [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
| [ H : 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf)))
| [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf)))
| [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf))
| [ H : ?A -> ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf))
| [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
| [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
| [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
| [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
| [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
| [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
| [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
| [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
end.
Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup.
Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup.
Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup.
End Z.
I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations
Ltac zify_op := repeat zify_op_1.
II) Conversion from nat to Z
Definition Z_of_nat' := Z.of_nat.
Ltac hide_Z_of_nat t :=
let z := fresh "z" in set (z:=Z.of_nat t) in *;
change Z.of_nat with Z_of_nat' in z;
unfold z in *; clear z.
Ltac zify_nat_op :=
match goal with
| H : context [ Z.of_nat (Pos.to_nat ?a) ] |- _ => rewrite (positive_nat_Z a) in H
| |- context [ Z.of_nat (Pos.to_nat ?a) ] => rewrite (positive_nat_Z a)
| H : context [ Z.of_nat (N.to_nat ?a) ] |- _ => rewrite (N_nat_Z a) in H
| |- context [ Z.of_nat (N.to_nat ?a) ] => rewrite (N_nat_Z a)
| H : context [ Z.of_nat (Z.abs_nat ?a) ] |- _ => rewrite (Zabs2Nat.id_abs a) in H
| |- context [ Z.of_nat (Z.abs_nat ?a) ] => rewrite (Zabs2Nat.id_abs a)
| H : context [ Z.of_nat (plus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_add a b) in H
| |- context [ Z.of_nat (plus ?a ?b) ] => rewrite (Nat2Z.inj_add a b)
| H : context [ Z.of_nat (min ?a ?b) ] |- _ => rewrite (Nat2Z.inj_min a b) in H
| |- context [ Z.of_nat (min ?a ?b) ] => rewrite (Nat2Z.inj_min a b)
| H : context [ Z.of_nat (max ?a ?b) ] |- _ => rewrite (Nat2Z.inj_max a b) in H
| |- context [ Z.of_nat (max ?a ?b) ] => rewrite (Nat2Z.inj_max a b)
| H : context [ Z.of_nat (minus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_sub_max a b) in H
| |- context [ Z.of_nat (minus ?a ?b) ] => rewrite (Nat2Z.inj_sub_max a b)
| H : context [ Z.of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H
| |- context [ Z.of_nat (pred ?a) ] => rewrite (pred_of_minus a)
| H : context [ Z.of_nat (mult ?a ?b) ] |- _ =>
pose proof (Nat2Z.is_nonneg (mult a b));
rewrite (Nat2Z.inj_mul a b) in *
| |- context [ Z.of_nat (mult ?a ?b) ] =>
pose proof (Nat2Z.is_nonneg (mult a b));
rewrite (Nat2Z.inj_mul a b) in *
| H : context [ Z.of_nat O ] |- _ => change (Z.of_nat O) with Z0 in H
| |- context [ Z.of_nat O ] => change (Z.of_nat O) with Z0
| H : context [ Z.of_nat (S ?a) ] |- _ =>
let isnat := isnatcst a in
match isnat with
| true =>
let t := eval compute in (Z.of_nat (S a)) in
change (Z.of_nat (S a)) with t in H
| _ => rewrite (Nat2Z.inj_succ a) in H
| _ =>
change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
end
| |- context [ Z.of_nat (S ?a) ] =>
let isnat := isnatcst a in
match isnat with
| true =>
let t := eval compute in (Z.of_nat (S a)) in
change (Z.of_nat (S a)) with t
| _ => rewrite (Nat2Z.inj_succ a)
| _ =>
change (Z.of_nat (S a)) with (Z_of_nat' (S a))
end
| _ : 0 <= Z.of_nat ?a |- _ => hide_Z_of_nat a
| _ : context [ Z.of_nat ?a ] |- _ =>
pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a
| |- context [ Z.of_nat ?a ] =>
pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a
end.
Definition Zpos' := Zpos.
Definition Zneg' := Zneg.
Ltac hide_Zpos t :=
let z := fresh "z" in set (z:=Zpos t) in *;
change Zpos with Zpos' in z;
unfold z in *; clear z.
Definition Z_of_N' := Z.of_N.
Ltac hide_Z_of_N t :=
let z := fresh "z" in set (z:=Z.of_N t) in *;
change Z.of_N with Z_of_N' in z;
unfold z in *; clear z.
The complete Z-ification tactic
is_inj T returns true iff the type T has an injection
Ltac is_inj T :=
match T with
| _ => let x := constr:(_ : InjTyp T _ ) in true
| _ => false
end.
Ltac elim_let :=
repeat
match goal with
| x := ?t : ?ty |- _ =>
let b := is_inj ty in
match b with
| true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
end
end.
Ltac zify :=
intros ; elim_let ;
Zify.zify ; ZifyInst.saturate.
match T with
| _ => let x := constr:(_ : InjTyp T _ ) in true
| _ => false
end.
Ltac elim_let :=
repeat
match goal with
| x := ?t : ?ty |- _ =>
let b := is_inj ty in
match b with
| true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
end
end.
Ltac zify :=
intros ; elim_let ;
Zify.zify ; ZifyInst.saturate.