Library Diqt.Int_utils

From Coq Require Import ZArith Lia Uint63.

Open Scope uint63_scope.

Lemma eqbPF_to_Z:
  ∀ x y, x =? y = false ↔ to_Z x ≠ to_Z y.

Lemma eqbPT_to_Z:
  ∀ x y, x =? y = true ↔ to_Z x = to_Z y.

Lemma add_neutral:
  ∀ (u: int), u + 0 = u.

Lemma fold_int_aux:
  ∀ (i e: int), i <? e = true→ i <? i + 1 = true.

Definition R x y := (y <? x) = true.

Definition fold_int' (T : Type) (f : int → T → T) (s e : int) (acc : T)
  (H : Acc R s) :=
(fix cont (i : int) (acc : T) (H : Acc R i) {struct H} : T :=
   let b := i <? e in
   (if b return ((i <? e) = b → T)
    then
     fun Hb ⇒
     cont (i + 1) (f i acc)
       match H with
       | Acc_intro _ H ⇒ H (i + 1) (fold_int_aux i e Hb)
       end
    else fun _ ⇒ acc) (eq_refl b)) s acc H.

Lemma acc_int:
  ∀ x, Acc (fun x y ⇒ y <? x = true) x.

Definition fold_int {T: Type} (f : int → T → T) (e: int) (acc: T) :=
  fold_int' T f 0 e acc (Acc_intro_generator 22 acc_int 0).

Lemma suc_sub:
  ∀ n m,
  m < n →
  (S (n - S m) = n - m)%nat.

Lemma nat_rect_one:
  ∀ T f n x acc,
  to_Z x = Z.of_nat n →
  nat_rect (fun _ : nat ⇒ T) (f x acc)
    (fun (n0 : nat) (acc0 : T) ⇒ f (of_pos (Pos.of_succ_nat (n + n0))) acc0) 0 =
  f (of_Z (Z.of_nat (n + 0)))
    (nat_rect (fun _ : nat ⇒ T) acc
      (fun (n0 : nat) (acc0 : T) ⇒ f (of_Z (Z.of_nat (n + n0))) acc0) 0).

Lemma fold_int_spec :
  ∀ T (f : int → T → T) e acc,
  fold_int f e acc =
  nat_rect (fun _ ⇒ T) acc
           (fun n acc ⇒ f (of_Z (Z.of_nat n)) acc)
           (Z.to_nat (to_Z e)).