Library Coq.omega.PreOmega


Require Import Arith Max Min BinInt BinNat Znat Nnat.

Local Open Scope Z_scope.

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

These tactic use the complete specification of Z.div and Z.modulo (Z.quot and Z.rem, respectively) to remove these functions from the goal without losing information. The Z.euclidean_division_equations_cleanup tactic removes needless hypotheses, which makes tactics like nia run faster. The tactic Z.to_euclidean_division_equations combines the handling of both variants of division/quotient and modulo/remainder.

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.


zify: the Z-ification tactic



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

Require Import ZifyClasses ZifyInst.
Require Zify.

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.