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.
```

Complete source code:

```
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.
```

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.

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.

Oh yeah: https://github.com/coq/coq/blob/cf408497eef21ee76fb253d95dce20902bd5cb37/theories/Init/Wf.v

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)

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.
```

But I think there must be some better way to do this.

Also, what is your feedback on this one?

```
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.
```

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`

)

Awesome!

@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
```

qed cannot be undone

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.
```

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

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

They recommend instead Qed wf proofs + what is known (?) as Krebbers' trick

@Pierre-Marie Pédrot That trick [1] goes at least 12 years back :).

[1} https://coq-club.inria.narkive.com/gO2dnKc4/well-founded-recursion-stuck-on-opaque-proofs

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...

This trick certainly predates Krebber. For instance, Gonthier was already explaining it in 2007: https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html

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...

It's also a good fit for a self-answered question on StackOverflow.

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?

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

Paolo Giarrusso said:

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

Sounds interesting and premise for a new question @Paolo Giarrusso .

Mukesh Tiwari has marked this topic as resolved.

Karl Palmskog said:

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...

It's also a good fit for a self-answered question on StackOverflow.

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

I think "Using Coq" fits well (https://coq.discourse.group/c/using-coq/5)

Last updated: Sep 30 2023 at 07:01 UTC