WIP on wf for int63 ltb

acc_int63.v

Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.Numbers.Cyclic.Int63.Int63.
Require Import Coq.Numbers.Cyclic.Int63.Ring63.
Require Import Coq.Init.Wf Wf_nat.

Local Open Scope Z_scope.
Local Open Scope int63_scope.
Local Coercion is_true : bool >-> Sortclass.

Definition Acc_ltb_0 : Acc Int63.ltb 0.
Proof.
  constructor.
  intros y H; exfalso.
  abstract (apply ltb_spec in H; pose proof (to_Z_bounded y) as H';
            rewrite to_Z_0 in H; lia).
Defined.

Definition Acc_eq {A R x y} : x = y :> A -> Acc R x -> Acc R y.
Proof.
  intros H [a]; constructor; intros z Hz; apply a; clear -H Hz;
    abstract (subst; assumption).
Defined.

Definition Acc_ltb_succ {x} : Acc Int63.ltb x -> Acc Int63.ltb (succ x).
Proof.
  intro a; constructor; intros y Hy; constructor; intros y' Hy'.
  destruct a as [a]; apply (a y'); clear a.
  abstract (
      apply ltb_spec in Hy; apply ltb_spec in Hy'; apply ltb_spec;
      rewrite succ_spec in Hy; pose proof wB_pos; pose proof wB_diff_0;
      pose proof (to_Z_bounded y); pose proof (to_Z_bounded y');
      pose proof (to_Z_bounded x);
      cut ((to_Z x + 1) / wB = 0 \/ (to_Z x + 1) / wB = 1)%Z;
      Z.div_mod_to_equations; nia
    ).
Defined.

Definition Acc_ltb_max_succ {x} : Acc Int63.ltb x -> Acc Int63.ltb (if Int63.ltb (succ x) x then x else succ x).
Proof.
  intro a; constructor; intros y Hy; constructor; intros y' Hy'.
  destruct a as [a]; apply (a y'); clear a.
  destruct a as [a]; apply (a y'); clear a.
  abstract (
      (destruct (succ x < x) eqn:?);
      apply ltb_spec in Hy; apply ltb_spec in Hy'; apply ltb_spec;
      try lia;
      rewrite succ_spec in Hy; pose proof wB_pos; pose proof wB_diff_0;
      pose proof (to_Z_bounded y); pose proof (to_Z_bounded y');
      pose proof (to_Z_bounded x);
      cut ((to_Z x + 1) / wB = 0 \/ (to_Z x + 1) / wB = 1)%Z;
      Z.div_mod_to_equations; nia
    ).
Defined.

Polymorphic Fixpoint fun_pow {A} (f : A -> A) (n : nat) : A -> A
  := match n with
     | O => fun a => a
     | S n => fun a => f (fun_pow f n a)
     end.

Definition Acc_ltb_fun_pow {n f} : (forall x, Acc Int63.ltb x -> Acc Int63.ltb (f x)) -> forall x, Acc Int63.ltb x -> Acc Int63.ltb (fun_pow f n x).
Proof.
  intros H x a.
  induction n as [ | n IHn ]; cbn [fun_pow]; [ exact a | ].
  apply H, IHn.
Defined.

Polymorphic Definition fun_pow2 {A} (f : A -> A) : A -> A
  := fun_pow f 2.

Polymorphic Definition fun_pow_pow {A} (f : A -> A) (n : nat) : A -> A
  := fun_pow fun_pow2 n f.

Definition Acc_ltb_fun_pow_pow {n f} : (forall x, Acc Int63.ltb x -> Acc Int63.ltb (f x)) -> forall x, Acc Int63.ltb x -> Acc Int63.ltb (fun_pow_pow f n x).
Proof.
  cbv [fun_pow_pow]; cbn [fun_pow].
  revert f; induction n as [ | n IHn ]; intros f H x a;
    [ apply H, a | ]; cbn [fun_pow] in *.
  eauto using @Acc_ltb_fun_pow with nocore.
Defined.
(*
  


Compute (2^Z.log2 wB)%Z.
Definition Acc_ltb_fun_pow {n f} : (forall x, Acc Int63.ltb x -> Acc Int63.ltb (f x)) -> forall x, Acc Int63.ltb x -> Acc Int63.ltb (fun_pow f n x).
Proof.
  intros H x a.
  induction n as [ | n IHn ]; cbn [fun_pow]; [ exact a | ].
  apply H, IHn.
Defined.

  := fun a =>


Definition Acc_ltb_add_nat {x n} : Acc Int63.ltb x -> Acc Int63.ltb (x + of_Z (Z.of_nat n)).
Proof.
  intro a; induction n as [ | n IHn ]; [ vm_compute of_Z | ].
  { eapply Acc_eq; [ | eassumption ]; clear; abstract ring. }
  { constructor; intros y Hy; constructor; intros y' Hy'.
    destruct IHn as [IHn]; apply (IHn y'); clear IHn a.
    apply ltb_spec in Hy; apply ltb_spec in Hy'; apply ltb_spec;
      rewrite ?add_spec, ?of_Z_spec, ?Nat2Z.inj_succ in *.
    Search (Z.of_nat (S _)).
      rewrite succ_spec in Hy; pose proof wB_pos; pose proof wB_diff_0;
      pose proof (to_Z_bounded y); pose proof (to_Z_bounded y');
      pose proof (to_Z_bounded x);
      cut ((to_Z x + 1) / wB = 0 \/ (to_Z x + 1) / wB = 1)%Z;
      Z.div_mod_to_equations; nia
    ).

    apply Acc_eq with (x := (x + of_Z (Z.of_nat n))
    ring.
    Search (φ (_ + _)).
    rewrite to_Z_p
    Search (_ = _ :> int).
  vm_compute.
  vm_compute of_Z.
  intro a; constructor; intros y Hy; constructor; intros y' Hy'.
  destruct a as [a]; apply (a y'); clear a.
  abstract (
  assert ((q = 0 \/ q = 1)%Z) by nia.
  destruct H6; try nia.
  Search (φ (succ _)).
  Print Acc.

  Search succ.
  constructor.
  intros y H; exfalso.
  abstract (apply ltb_spec in H; pose proof (to_Z_bounded y) as H';
            rewrite to_Z_0 in H; lia).
Defined.


  Search φ 0.
  of_Z_spec

       Search Int63.ltb.

Check Int63.ltb.
Print well_founded.
Check Acc.
Locate Acc.
Print



    *)