Rewrite.v

Require Import Lia 
  Coq.Unicode.Utf8
  Coq.Bool.Bool 
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith.
Import VectorNotations.
Local Open Scope vector_scope.
Local Open Scope N_scope.


Section Wf_proof.

  Let f (a : N) := N.to_nat a.

  Definition zwf (x y : N) := (f x < f y)%nat.

  Lemma zwf_well_founded : well_founded zwf.
  Proof.
    exact (well_founded_ltof _ f).
  Defined.

  Lemma N_acc (x : N) : forall a, a < x -> Acc N.lt a.
  Proof.
    induction (zwf_well_founded x) as [z Hz IHz].
    intros ? Hxa.
    constructor; intros y Hy.
    eapply IHz with (y := a).
    unfold zwf. unfold f.
    nia. nia.
  Defined.
    
  Lemma N_lt_wf : well_founded N.lt.
  Proof.
    red; intros ?.
    constructor; intros y Hy.
    eapply N_acc with (x := a).
    exact Hy.
  Defined. 


  Lemma N_Lt_wf : forall up, Acc (fun x y => x < y) up.
  Proof.
    intros up.
    pose proof (N_lt_wf up).
    exact H.
  Defined.

End Wf_proof.


Section Util.

  Definition np_total (np : N) (H : np < 256) : byte.
  Proof.
    refine (match (np <? 256) as npp return _ = npp -> _ with 
    | true => fun H => match (of_N np) as npw return _ = npw -> _  with 
      | Some x => fun He => x 
      | None => fun He => _  (* impossible *)
      end eq_refl
    | false => fun H => _ 
    end eq_refl).
    apply of_N_None_iff in He.
    abstract nia. (* abstract or transparent? *)
    apply N.ltb_ge in H.
    abstract nia.
  Defined.

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

  Lemma N_eq_gt : forall up t : N, 256 <= up -> t = up / 256 -> 0 <= t / 256 < t.
  Proof.
    intros up t Hup Ht.
    split. 
    apply N.le_0_l.
    apply N.div_lt_upper_bound. 
    nia.
    (* I know that 1 <= t *)
    assert (Hot: 1 <= t).
    rewrite Ht.
    apply N.div_le_lower_bound. nia.
    simpl. exact Hup. nia.
  Qed.

  Fixpoint guard A (R : A -> A -> Prop) (n : nat) (wfR : well_founded R) : well_founded R :=
    match n with
    | 0%nat => wfR
    | S n => fun x => Acc_intro x (fun y _ => guard A R n (guard A R n wfR) y)
    end.


  (* Let's go with List :) *)
  Definition length_byte_list (np : N) : list byte.
  Proof.
    refine ((fix length_byte_list up (H: Acc (fun x y => (* 0 <= *) x < y) (N.div up 256)) {struct H} := 
      match (up <? 256) as upp return _ = upp -> _ with
      | true => fun Hnp => List.cons (np_total up _) List.nil
      | false => fun Hnp => 
        let r := N.modulo up 256 in 
        let t := N.div up 256 in 
        List.cons (np_total r _) (length_byte_list t _)
      end eq_refl
    ) np (N_Lt_wf _ ) (*(guard _ (fun x y => 0 <= x < y) 100 (N.lt_wf 0)) (N.div np 256))*)).
    + apply N.ltb_lt in Hnp; exact Hnp.
    + apply (nmod_256 up).
    + eapply Acc_inv with (x := t). exact H.
      apply N.ltb_ge in Hnp.
      eapply N_eq_gt with (up := up); auto. 
  Defined.

  Theorem length_correctness : forall np : N, List.length (length_byte_list np) = N.to_nat (N.div np 256 + 1).
  Proof.
    intro np.
    induction (N.lt_wf 0 np) as [up Hacc IHup].
    refine(match (up <? 256) as upp return _ = upp -> _ with
    | true => fun Hnp => _  
    | false =>  fun Hnp => _
    end eq_refl).
    + apply N.ltb_lt in Hnp.
      assert (Hup : up/256 = 0).
      rewrite N.div_small;
      [reflexivity | exact Hnp].
      rewrite Hup.
      unfold length_byte_list.
      simpl. apply N.ltb_lt in Hnp. 
      (* rewrite Hnp is not working
         which is ill-typed.
        Reason is: Incorrect elimination of "N.ltb_lt up 256" in the inductive type
        "and": ill-formed elimination predicate. *)
      admit.
    +
      unfold length_byte_list. simpl. rewrite Hnp.


      apply N.ltb_ge in Hnp.
      (* divide the up by 256 for next call *)
      remember (N.div up 256) as t.
      remember (N.modulo up 256) as r.
      assert (Hup: up = 256 * t + r).
      subst. rewrite <-N.div_mod with (b := 256);
      [reflexivity | nia].
      assert (Hot: 1 <= t).
      rewrite Heqt.
      apply N.div_le_lower_bound. nia.
      simpl. exact Hnp.
      assert (Htup: up = 256 + 256 * (t - 1) + r).
      nia.
      (* now I am going to remember
         256 * (t - 1) + r as y, for subsequent recursive 
         calls *)
      remember (256 * (t - 1) + r) as y.
      assert (Hyp: 0 <= y < up). nia.
      specialize(IHup y Hyp).
      rewrite Htup. rewrite Heqy in IHup.
      assert (Hz : 0 <= t - 1). nia.
      assert (Hr : r < 256). rewrite Heqr.
      apply nmod_256.
      assert (Ht: (256 * (t - 1) + r) / 256 + 1 = t).
      rewrite N.mul_comm, N.div_add_l, N.div_small.
      nia. exact Hr. nia.
      rewrite Ht in IHup.

      (* at this point, I want 
        length (length_byte_list (256 + 256 * (t - 1) + r)) = 
        S (length (length_byte_list (256 * (t - 1) + r))). 
      
      Then I can infer 
      length (length_byte_list (256 * (t - 1) + r)) = 
      N.to_nat t. 

      Now from IHup, y/256 = t - 1 and therefore
      y/256 + 1 = t and we are home *)