## Stream: Coq users

### Topic: ✔ Recursive call failing on Acc

#### Mukesh Tiwari (Oct 08 2021 at 05:04):

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.

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

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

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

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

#### 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`)

Awesome!

#### 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 . 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):

qed cannot be undone

#### 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  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):

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

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

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

#### 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):

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

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

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

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

Paolo Giarrusso Do you know a way to turn Opaque definitions to Transparent? I am talking about N.lt_wf . 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 (!)

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

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 .

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

Mukesh Tiwari has marked this topic as resolved.

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

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?

#### Karl Palmskog (Oct 09 2021 at 09:44):

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

Last updated: Jan 31 2023 at 14:03 UTC