Hi everyone, how can I convince Coq to accept my definition of `nat_div`

. (I understand that I am relying on accessibility predicate for termination but my decreasing argument is `u`

)

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

my decreasing argument is u

but the recursive call is unrelated to `u`

@Gaëtan Gilbert Yeah, you are right. Maybe I see your point but I don't how to resolve it. I guess something like this?

```
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} *) := _).
```

But the challenge is this does not give me a nice induction principle. When I uncomment `(acc : Acc R a)`

, the type checker is not happy.

(deleted)

What about :

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

Indeed, the structural argument about accessibility can be observed in `Acc_rect`

, used in `well_founded_induction_type`

.

Thanks @Pierre Castéran ! I already have a solution using well_founded_induction but I am trying to simulated the `Equations`

solution posted on Coq mailing, but I am not able to see how to convince Coq about termination.

I managed to get one but it's certainly not as clean as the Equations solution.

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

Yes. What is the main difference between using `Equations`

and `well_founded_induction`

?

I already used `Equations`

to define a complex well_founded recursive function.

The resulting function was also an application of

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

Your solution looks OK, the main difference is that your `fix ... match acc ...`

part is in your definition instead of the standard library :grinning:

`Equations`

really feels like magic, a really pleasant system to work for dependent types. I don't know how it internally work so I have no idea about the difference between `Equations`

and `well_founded_induction`

.

I guess the two versions don't behave the same when it comes to reduction and/or extraction? Nothing fundamental but significant though.

Surprisingly, the extraction gives a OCaml code that is very similar to the one that Coq type checker rejects :)

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

Compare it to the one you get with `well_founded_induction`

, and the one with `Equations`

.

Equations extraction is very different, at least by just looking at the syntax, from the well_founded_one. Vanilla Coq extraction very idiomatic, at least for my taste.

Equations extraction.

```
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,__))
```

Well _founded_induction extraction

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

Mukesh Tiwari has marked this topic as resolved.

FWIW, all uses of lia/nia in Defined blocks should usually be wrapped by abstract; and if you're interested in extraction you probably want N not nat...

@Paolo Giarrusso Do you know where can I find this theorem, ```
Theorem N_lt_eq_lt_dec : forall (x y : N),
{x < y} + {x = y} + {y < x}.
```

in Coq library?

@Mukesh Tiwari https://gitlab.mpi-sws.org/iris/stdpp/-/blob/e04271e24ab89bc735321375fb85ed7e1f9f80e7/stdpp/lexico.v#L99-107

Dominique Larchey-Wendling has marked this topic as unresolved.

Hi @Mukesh Tiwari

Nowadays I usually use the following `induction on _ _ as _ with measure _`

tactic notation to do all the `Acc`

fixpoint encoding for me in a uniform way. Best regards,

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

As a side question: don't you have difficulties to compute with your `nat_div`

in Coq. Sometimes, the `Qed`

from the lemmas of the `Arith`

lib block the evaluation of such functions.

Don't you need Rwf and measure2_rect to be Defined to compute with nat_div, @Dominique Larchey-Wendling ?

Alternatively, the well-foundedness proofs can sometimes be kept opaque, if you use Acc_intro_generator; I've learned about this from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/well_founded.v#L11

I have not tested this particular one but I now prefer to write fully specified functions and get the fixpoint equations out of the spec, if ever needed. However, when properly specified, the equations may not be needed at all. But I did experiment such problems with evaluating well-founded fixpoints in the past.

Moreover I remember being told about this remark of generating `Acc`

based fuel (by @Matthieu Sozeau on coq-club if my memory is correct), to be able to evaluate such `Acc`

based fixpoints but thanks for the link that formalizes that cleanly.

Ah, you've just reminded me: none of above versions come with unfolding lemmas — except the one from Equations, and I guess your point is to make unfolding unnecessary via the spec

Dominique Larchey-Wendling said:

As a side question: don't you have difficulties to compute with your

`nat_div`

in Coq. Sometimes, the`Qed`

from the lemmas of the`Arith`

lib block the evaluation of such functions.

Yeah, I had but when I changed `R_acc`

(see the very top post) closed with Qed to Defined, it worked. Also, I found out that `lt_wf`

has been closed with Defined so I used it (https://github.com/coq/coq/blob/master/theories/Arith/Wf_nat.v). But I see your point because in the past, I have had hard time evaluating the functions defined using `well_founded_ind`

. I think something has changed in evaluation mechanism of Coq but I can only speculate.

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

Paolo Giarrusso said:

Alternatively, the well-foundedness proofs can sometimes be kept opaque, if you use Acc_intro_generator; I've learned about this from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/well_founded.v#L11

This is something we should highlight to the community better. Maybe one good way is as a Proof Assistant Stack Exchange question? Apparently the original source is https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html

@Karl Palmskog It would also be a good idea to maintain a tutorial/wiki, possibly within the Coq GitHub repo, for this kind of Coq tricks.

I suggest making PR to something like: https://github.com/tchajed/coq-tricks

I list some of the tutorial/tricks resources at https://github.com/coq-community/awesome-coq#tutorials-and-hints

the main reason for getting something into Proof Assistant SE is that search engines adore them

Interestingly, I already have two examples [1, 2] of computing with Opaque Acc proofs. I just need to write some explanation about it and push them to https://github.com/tchajed/coq-tricks.

[1] https://github.com/mukeshtiwari/Coq-automation/blob/master/Opaque.v#L62

[2] https://github.com/mukeshtiwari/Coq-automation/blob/master/Gcd_guarded.v#L64

Just an observation: it seems that using this method (unfolding `Acc`

once and use `f`

to construct less than `lt`

proof), we can compute with well founded functions without any guard (Edit: Acc_intro_generator). I tried to write my byte list following the same pattern and it works.

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

As long as the Acc argument reduces enough times the computation will go through; using guard + opaque well-foundedness is a bit hacky, but it can perform better if the well-foundedness proof is slow

It's a bit incorrect to say "without guarded recursion", the definition is still guarded on the Acc proof. As `lt_wf`

is transparent though, you can compute with it fine.

I think "without guard" stood for "without Gonthier's hack for opaque well-foundedness proofs", since the actual listings kind-of rename stdlib's `Acc_intro_generator`

to `guard`

; I agree the description is confusing and stdlib's name is better.

Last updated: Jun 24 2024 at 14:01 UTC