From Coq Require Import Arith Utf8 Psatz
  Peano.

Section Wf_div.

  Definition R := fun x y => x < y.

  Lemma R_acc : forall (a : nat), Acc R a.
  Proof.
    induction a as [|a IHa].
    +
      constructor.
      intros ? Ha.
      refine (match Ha with end).
    +
      constructor.
      intros y Ha.
      constructor.
      intros z Hc.
      pose proof (Acc_inv IHa) as Ih.
      eapply Ih.
      unfold R in Ha, Hc |- *.
      abstract nia.
  Qed.


  Lemma R_sub_acc : forall (a b : nat),
     Acc R (a - b).
  Proof.
    intros ? ?.
    eapply R_acc.
  Qed.



  Theorem nat_div : nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intros a b Ha.
    refine((
      fix nat_div u (acc : Acc R u) :=
      match (lt_eq_lt_dec a b) with
        | inleft Hb =>
          match Hb with
          | left Hc => (0, a)
          | right Hc => (1, 0)
          end
        | inright Hb =>
          match nat_div (a - b) _ with
          | (q, r) => (S q, r)
          end
        end) a (R_acc a)).
    eapply R_sub_acc;
    assumption.
    Guarded.

Theorem nat_div :  forall (b : nat),
    0 < b -> nat -> nat * nat.
  Proof.
    intros b Hb.
    refine(
      fix nat_div a (* (acc : Acc R a) {struct acc} *) := _).

Section Divisor.
Variable b : nat.
Hypothesis Hb : 0 < b.

Definition div : nat->  nat * nat.
  refine (well_founded_induction lt_wf (fun n => (nat * nat)%type) _ ).
  - intros x Recx; destruct (lt_eq_lt_dec x b).
    + destruct s.
      * exact (0, b).
      * exact (1, 0).
    + destruct (Recx (x-b)) as [q r].
     *  abstract lia.
     *  exact (S q, r)
Defined.

End Divisor.

  Theorem nat_div :  nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.
    cut (Acc R a); revert a.
    +
      refine(fix nat_div a (acc : Acc R a) {struct acc} :=
        match acc with
        | Acc_intro _ f => fun b Ha =>
          match (lt_eq_lt_dec a b) with
          | inleft Hb =>
            match Hb with
            | left Hc => (0, a)
            | right Hc => (1, 0)
            end
          | inright Hb =>
            match nat_div (a - b) _ b Ha with
            | (q, r) => (S q, r)
            end
          end
        end).
      assert (Hc : R (a - b) a).
      unfold R. abstract nia.
      exact (f (a - b) Hc).
    +
      intros a.
      eapply R_acc.
  Defined.

FixWf :
  forall (A : Type) (R : relation A),
       WellFounded R ->
       forall P : A -> Type, (forall x : A, (forall y : A, R y x -> P y) -> P x) -> forall x : A, P x

let rec nat_div a b =
  match lt_eq_lt_dec a b with
  | Inleft hb ->
    (match hb with
     | Left -> Pair (O, a)
     | Right -> Pair ((S O), O))
  | Inright -> let Pair (q, r) = nat_div (sub a b) b in Pair ((S q), r)

Require Import Arith.
From Equations Require Import Equations.
Set Equations Transparent.



Definition pf {A} (a : A) : {b | a = b} :=
  exist _ a eq_refl.

Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).


Equations division (a b : nat) (p : 0 < b) : nat * nat by wf a lt :=
  division a b p with pf (a <? b) =>
      | true eqn: _ =>  (0, a)
      | false eqn: Ha =>
        match division (a - b) b p with
        | (q, r) => (S q, r)
        end.
  Next Obligation.
    eapply Nat.sub_lt.
    eapply Nat.ltb_ge in Ha;
    exact Ha.
    exact p.
  Defined.

Extraction division.

let division a a0 =
  let rec fix_F x =
    let a1 = let pr1,_ = x in pr1 in
    let b = let pr1,_ = let _,pr2 = x in pr2 in pr1 in
    (match pf (Nat.ltb a1 b) with
     | True -> Pair (O, a1)
     | False ->
       let Pair (q, r) = let y = (sub a1 b),(b,__) in fix_F y in
       Pair ((S q), r))
  in fix_F (a,(a0,__))

Section Wf_div.



  Lemma R_wf :
    well_founded lt.
  Proof.
    intro a.
    apply lt_wf.
  Qed.



  Theorem nat_div_wf : forall (a b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.
    induction (R_wf a) as [a Ha IHa];
    intros b Hb.
    destruct (lt_eq_lt_dec a b) as [[Hc | Hc] | Hc].
    +
      exact (0, a).
    +
      exact (1, 0).
    +
      assert (Hrel : (a - b) < a) by nia.
      destruct (IHa (a - b) Hrel b Hb) as (q, r).
      exact (S q, r).
  Defined.

End Wf_div.

Extraction nat_div_wf.

let rec nat_div_wf x b =
  let s = lt_eq_lt_dec x b in
  (match s with
   | Inleft a -> (match a with
                  | Left -> Pair (O, x)
                  | Right -> Pair ((S O), O))
   | Inright ->
     let p = let y = sub x b in nat_div_wf y b in
     let Pair (a, b0) = p in Pair ((S a), b0))

Require Import Arith Extraction Wellfounded Lia Utf8.

Section measure2_rect.

  Variable (X Y : Type) (m : X → Y → nat) (P : X → Y → Type)
           (HP : ∀x y, (∀ x' y', m x' y' < m x y → P x' y') → P x y).

  Let m' '(x,y) := m x y.
  Let Rwf : well_founded (λ p q, m' p < m' q).
  Proof. apply wf_inverse_image, lt_wf. Qed.

  Definition measure2_rect x y : P x y.
  Proof.
    generalize (Rwf (x,y)); revert x y.
    refine (fix loop x y a {struct a} :=
      HP x y (λ x' y' _, loop x' y' _)).
    now apply Acc_inv with (1 := a).
  Qed.

End measure2_rect.

Extraction Inline measure2_rect.

Tactic Notation "induction" "on" hyp(x) hyp(y) "as" ident(IH) "with" "measure" uconstr(f) :=
  pattern x, y; revert x y; apply measure2_rect with (m := λ x y, f); intros x y IH.

Definition nat_div_specif n b '(q,r) := (n = q*b+r) /\ r < b.

Definition nat_div_pwc (n b : nat) : 0 < b → { c | nat_div_specif n b c }.
Proof.
  induction on n b as loop with measure (n-b); intros Hb.
  refine (match (lt_eq_lt_dec n b) with
    | inleft Hnb =>
      match Hnb with
      | left Hnb  => exist _ (0,n) _
      | right Hnb => exist _ (1,0) _
      end
    | inright Hnb =>
      let (c,Hc) := loop (n-b) b _ _ in
      match c as c' return nat_div_specif _ _ c' -> _ with
      | (q,r) => fun Hc =>  exist _ (S q,r) _
      end Hc
    end); red; try destruct Hc; try lia.
Defined.

Definition nat_div n b Hb := proj1_sig (nat_div_pwc n b Hb).

Fact nat_div_spec n b Hb :
  let (q,r) := nat_div n b Hb
  in  n = q * b + r /\ r < b.
Proof.
  unfold nat_div.
  destruct (nat_div_pwc n b Hb) as ([] & []); simpl; lia.
Qed.

Extraction Inline nat_div_pwc.
Recursive Extraction nat_div.

Section Wf_div.


  Theorem nat_div :  nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.
    cut (Acc lt a);
    [revert a |].
    +
      refine(fix nat_div a (acc : Acc lt a) {struct acc} :
        forall b : nat, 0 < b -> nat * nat :=
        match acc with
        | Acc_intro _ f => fun b Ha =>
          match (lt_eq_lt_dec a b) with
          | inleft Hb =>
            match Hb with
            | left Hc => (0, a)
            | right Hc => (1, 0)
            end
          | inright Hb =>
            match nat_div (a - b) _ b Ha with
            | (q, r) => (S q, r)
            end
          end
        end).
      assert (Hc : (a - b) < a).
      abstract nia.
      exact (f (a - b) Hc).
    +
      eapply lt_wf.
  Defined.

End Wf_div.

Lemma pf : 0 < 2.
Proof.
  auto.
Defined.

Eval compute in nat_div 400 2 pf.

= (200, 0)
     : nat * nat

From Coq Require Import Arith Utf8 Psatz
  Peano NArith Strings.Byte NArith.

Definition np_total (np : N):  (np <? 256 = true) ->  byte.
  Proof.
    intros H.
    pose proof of_N_None_iff np as Hn.
    destruct (of_N np) as [b | ].
    + exact b.
    + exfalso; abstract (apply N.ltb_lt in H;
        intuition nia).
  Defined.

  Lemma nmod_256 : forall np, np mod 256 < 256.
  Proof.
    intros; eapply N.mod_lt; intro H;
    inversion H.
  Qed.

Definition length_byte_list_without_guard : N -> list byte.
  Proof.
    intro np.
    cut (Acc lt (N.to_nat np));
    [revert np |].
    +
      refine(fix length_byte_list_without_guard np (acc : Acc lt (N.to_nat np))
        {struct acc} :=
      match acc with
      | Acc_intro _ f =>
        match (np <? 256) as npp
          return _ = npp -> _
        with
        | true => fun Ha => List.cons (np_total np Ha) List.nil
        | false => fun Ha =>
            let r := N.modulo np 256 in
            let t := N.div np 256 in
            List.cons (np_total r _) (length_byte_list_without_guard t _)
        end eq_refl
      end).
      ++
        apply N.ltb_lt, (nmod_256 np).
      ++
        apply N.ltb_ge in Ha.
        assert (Hc : (N.to_nat t < N.to_nat np)%nat).
        unfold t. rewrite N2Nat.inj_div.
        eapply Nat.div_lt; try abstract nia.
        exact (f (N.to_nat t) Hc).
    +
      apply lt_wf.
  Defined.


Eval compute in length_byte_list_without_guard 3723.
= ("139"%byte :: "014"%byte :: nil)%list
     : list byte