Is there a straightforward way to use well-founded mechanisms of Equations to ensure termination when the function being defined is used an argument to a higher-order function? Suppose I have this definition of a Fibonacci sequence:

```
Equations fib_map (n : nat) : N :=
fib_map 0 => 0;
fib_map k => foldr N.add 0 (map fib_map (iota 0 k))
```

(where `iota`

from mathcomp generates a sequence `0..k-1`

). What wf relation can I use here to prove termination? In Agda/Idris such cases are typically worked around by mutually defining the function together with an inlined version of `map`

, but this looks like it needs a well-founded proof.

You can do a proof by well-founded induction on the order on nat, but it's a bit tedious because you need to thread in enough information to prove that the recursive call is indeed on a smaller nat:

```
From Equations Require Import Equations.
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.
(* map enriched with membership information for the arguments *)
Equations? map_in [A : eqType] [B] (l : seq A) (f : forall a, a \in l -> B) : list B :=
| [::], _ => [::]
| (a :: xs), f => f a _ :: map_in xs (fun x w => f x _).
Proof.
1: apply: mem_head.
by rewrite in_cons orbC w.
Qed.
(* Without the noeqns I get a universe inconsistency... *)
Equations(noeqns) fib_map (n : nat) : nat by wf n :=
fib_map 0 => 0;
fib_map k => foldr Nat.add 0 (map_in (iota 0 k) (fun n _ => fib_map n)).
Next Obligation.
move: i.
rewrite -/(iota 0 (S n0)) mem_iota.
move=> /andP [_] /ltP //.
Defined.
```

Thanks! I've rewritten the definition slighly (and fixed the algorithm):

```
Equations map_in {A : eqType} {B} (l : seq A) (f : forall a, a \in l -> B): seq B :=
| [::], _ => [::];
| a :: xs, f =>
f a (mem_head a xs) ::
map_in (l:=xs) (fun x w => f x ltac:(rewrite in_cons w orbT)).
Arguments map_in [A B] l f.
Open Scope N_scope.
Equations(noeqns) fib_map (n : nat) : N by wf n lt :=
fib_map 0 => 0;
fib_map k.+1 => 1 + foldr N.add 0 (map_in (iota 0 k) (fun n w => fib_map n)).
Next Obligation.
apply: ssrnat.ltP; rewrite ltnS; apply: ltnW.
by move: w; rewrite mem_iota add0n; case/andP.
Defined.
```

For some reason `l`

becomes an implicit, so I revert it with `Arguments`

.

The problem however, is reasoning about this definition, it seems that `noeqns`

prevents any eliminators from being generated...

Ah, if I relax the derivation options to `#[derive(eliminator=no)]Equations fib_map ..`

the universe problem doesn't come up, but I still get enough equalities to use `simp`

which hopefully should be enough.

@Matthieu Sozeau Do you have any idea how we could debug this universe inconsistency ?

The actual error I have is that without `noeqns/noind`

the last `Qed/Defined`

fails complaining that there is a missing constraint `Equality.type.u0 <= Set`

and there seem to be a constraint in the context `Set < Equality.type.u0`

.

Interesting universe issue :) It is probably equations that tries to put the graph of the function in Set, which is too low

@Alexander Gryzlov a common idiom in this case is to add a simplification lemma for `map_in`

of shape `map_in l (fun x _ => f x) = map f l`

to the `fib_map`

rewrite database so that you never see `map_in`

again when reasoning about `fib_map`

.

Last updated: Jun 14 2024 at 20:01 UTC