✔ Recursive call failing on Acc · Coq users

Coq complains that my principal argument is "up / 256" instead of a subterm of "up", but that's the whole point of well founded induction, and I wonder what is wrong with my code below?

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)) :=
      match (N_le_gt_dec up 256) as upp return upp = _ -> _ with
      | left Hle => fun Hnp => _
      | right Hre => fun Hnp => _
      end eq_refl
    ) np (N.lt_wf 0 _ )).
    (* base case *)
    exact (List.cons (np_total up Hle) List.nil).

    (* Induction case: r := Nmod up 256 and t = N.div up 256 *)
    remember (N.modulo up 256) as r.
    remember (N.div up 256) as t.

    assert (Hacc: Acc (λ x y : N, 0 <= x < y) (t / 256)).
    eapply Acc_inv with (x := t). exact H.
    eapply N_eq_gt with (up := up); auto.
    (* total function *)
    pose proof (nmod_256 up) as Hup.
    assert (Hr : r < 256).
    rewrite <-Heqr in Hup.
    exact Hup.
    exact  (List.cons (np_total r Hr) (length_byte_list t Hacc)).
    Guarded.

  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_le_gt_dec : forall u v : N, {u < v} + {v <= u}.
  Proof.
  Admitted.

  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.

  (* 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)) :=
      match (N_le_gt_dec up 256) as upp return upp = _ -> _ with
      | left Hle => fun Hnp => _
      | right Hre => fun Hnp => _
      end eq_refl
    ) np (N.lt_wf 0 _ )).
    (* base case *)
    exact (List.cons (np_total up Hle) List.nil).

    (* Induction case: r := Nmod up 256 and t = N.div up 256 *)
    remember (N.modulo up 256) as r.
    remember (N.div up 256) as t.

    assert (Hacc: Acc (λ x y : N, 0 <= x < y) (t / 256)).
    eapply Acc_inv with (x := t). exact H.
    eapply N_eq_gt with (up := up); auto.
    (* total function *)
    pose proof (nmod_256 up) as Hup.
    assert (Hr : r < 256).
    rewrite <-Heqr in Hup.
    exact Hup.
    exact  (List.cons (np_total r Hr) (length_byte_list t Hacc)).
    Guarded.

Paolo Giarrusso (Oct 08 2021 at 06:01):

First, you'll want an explicit struct annotation, to mark your fixpoint as structurally recursive on H, and then you should get the guardedness checker happy for that recursive argument.

Paolo Giarrusso (Oct 08 2021 at 06:03):

Well-founded recursion is essentially just a design pattern for using structural recursion: it does it on Acc. So I wonder about Acc_inv; but if it is transparent with the right definition, this should work.

Paolo Giarrusso (Oct 08 2021 at 06:04):

Paolo Giarrusso (Oct 08 2021 at 06:09):

Style-wise, definitions are clearer in Gallina if they're transparent: you could move much more of your body into the refine, and Qed off the proofs using abstract (or Program and obligations, if Program does not mangle your code too much)

Mukesh Tiwari (Oct 08 2021 at 06:39):

Thanks @Paolo Giarrusso . Do you know a quick/clever way to turn r := up mod 256 into Hr : r = up mod 256? I generally do something like:

assert (r = up mod 256).
    subst r; reflexivity.

Mukesh Tiwari (Oct 08 2021 at 06:44):

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 (N_le_gt_dec up 256) as upp return upp = _ -> _ with
      | left Hle => fun Hnp => List.cons (np_total up Hle) List.nil
      | right Hre => 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 0 _ )).

    assert (Heqr: r = up mod 256).
    subst r. reflexivity.
    pose proof (nmod_256 up) as Hup.
    rewrite <-Heqr in Hup; exact Hup.


    assert (Hacc: Acc (λ x y : N, 0 <= x < y) (t / 256)).
    eapply Acc_inv with (x := t). exact H.
    eapply N_eq_gt with (up := up); auto.
    exact Hacc.
  Defined.

Paolo Giarrusso (Oct 08 2021 at 06:51):

proof bullets would help reading, but instead of introducing Heqr, could you just use unfold r; exact Hup? Or even exact Hup since that unfold is redundant (unfolds aren’t needed by eapply, they’re only needed to help rewrite)

Mukesh Tiwari (Oct 08 2021 at 07:04):

Mukesh Tiwari (Oct 08 2021 at 08:52):

@Paolo Giarrusso Do you know a way to turn Opaque definitions to Transparent? I am talking about N.lt_wf [1]. One way is to copy paste the definition and end it with Defined but I am wondering is there any other way?

About N.lt_wf.
N.lt_wf is not universe polymorphic
Arguments N.lt_wf _%N_scope
N.lt_wf is opaque
Expands to: Constant Coq.NArith.BinNat.N.lt_wf

Gaëtan Gilbert (Oct 08 2021 at 08:58):

Mukesh Tiwari (Oct 08 2021 at 09:46):

Thanks @Gaëtan Gilbert . I manage to prove it (a transparent definition) but I am curious what would break if someone changes the Qed in [1] to Defined in Coq code base?

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.

Gaëtan Gilbert (Oct 08 2021 at 09:54):

probably nothing would break
deciding what to make qed is pretty adhoc so there may not be any real reason for these lemmas to be opaque

Pierre-Marie Pédrot (Oct 08 2021 at 09:57):

Note that making wf proofs Defined is (arguably) discouraged by quite a few people.

Pierre-Marie Pédrot (Oct 08 2021 at 09:57):

Mukesh Tiwari (Oct 08 2021 at 11:08):

Pierre-Marie Pédrot (Oct 08 2021 at 11:28):

Yeah, it's true that I distinctly remember Thomas Braibant discussing about this technique some time when I was still at the ENS Lyon, so somewhere between 2009 and 2010... But as the message says, it was already considered folklore so the proper attribution might be lost to the mist of the dawn of ages...

Guillaume Melquiond (Oct 08 2021 at 11:46):

Karl Palmskog (Oct 08 2021 at 14:20):

ah, could someone please document this trick/idiom on the Discourse? Otherwise, I fear we will have to keep digging up these old Coq-Club threads...

Paolo Giarrusso (Oct 08 2021 at 22:32):

Others have answered the main question; I'll add that Qed and Opaque are different things, for non-obvious soundness reasons (!)

Mukesh Tiwari (Oct 08 2021 at 23:00):

Notification Bot (Oct 09 2021 at 00:14):

Mukesh Tiwari (Oct 09 2021 at 01:35):

Karl, I am happy to do that but in which section of Discourse should I post this trick?