I was playing with some function and wf recursion, and I noticed that if I used the inductive representation of order for nat and another representation using fixpoint, then the first definition computes (cbn, compute, etc) and the second doesn't.

I was curious why that could that be? Do you need to add some hint or something like that?

The function is simply quicksort with wf over the length of the list.

```
Equations? qsort (l : list nat) : list nat by wf (length l) lt :=
qsort nil := nil;
qsort (hd :: tl) :=
let lt_list := filter (fun x => x <? hd) tl in
let sorted_lt := qsort lt_list in
let gt_list := filter (fun x => hd <=? x) tl in
let sorted_gt := qsort gt_list in
sorted_lt ++ hd :: sorted_gt.
Proof.
(* omitted *)
Defined.
Eval compute in qsort [3 ; 1 ; 1 ; 2].
(* = [1; 1; 2; 3] *)
```

If I change `lt`

to the following definition, then running `Eval`

on it doesn't compute.

```
Fixpoint leq (n m : nat) : Prop :=
match n,m with
| 0 , _ => True
| S _ , 0 => False
| S n , S m => leq n m
end.
Definition lt n m := leq (S n) m.
#[local] Instance wf_nat : WellFounded lt := lt_wf. (* omitting proofs for brevity but they exist *)
Equations? qsort (l : list nat) : list nat by wf (length l) lt := (* same definition, proof changes a little *)
Eval compute in qsort [3 ; 1 ; 1 ; 2].
(*
(fix Fix_F
(x : list nat)
(a : Acc
(fun x0 y : list nat =>
..... big chunk ..... ))) [3; 1; 1; 2]
((fix F
(x : nat)
(a : Acc
(fun n m : nat =>
..... big chunk ..... ) 4 (lt_wf 4) [3; 1; 1; 2] eq_refl)
*)
```

Your ˋlt_wfˋ did not unfold. Is it `Defined`

or ˋQed`ed?

`Defined`

Ahhh, my bad! `lt_wf`

was with `Qed`

, changed it to `Defined`

and everything worked. I thought you were talking about the proof in the quicksort functino itself. Thanks!

I imagined I had to make something transparent or add a hint or something, but I wasn't expecting that the proof of well foundedness was the one to be made transparent :ok:

Another technique that might be useful in this kind of situation is to use `Acc_intro_generator`

, as defined here. This lets you artificially add some constructors on top of a (possibly opaque) proof of accessibility, so as to compute properly with it.

Last updated: Oct 13 2024 at 01:02 UTC