## Stream: Equations devs & users

### Topic: Termination with higher-order functions

#### Alexander Gryzlov (May 23 2022 at 19:58):

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.

#### Kenji Maillard (May 23 2022 at 20:35):

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

#### Alexander Gryzlov (May 23 2022 at 22:20):

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.
move: w; rewrite -/(iota 0 (S k)) mem_iota.
by case/andP.
Defined.
``````

For some reason `l` becomes an implicit, so I revert it with `Arguments`.

#### Alexander Gryzlov (May 23 2022 at 22:20):

The problem however, is reasoning about this definition, it seems that `noeqns` prevents any eliminators from being generated...

#### Alexander Gryzlov (May 23 2022 at 22:29):

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.

#### Kenji Maillard (May 24 2022 at 08:56):

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

#### Matthieu Sozeau (May 24 2022 at 09:18):

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

#### Matthieu Sozeau (May 24 2022 at 09:20):

@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: Jan 29 2023 at 14:02 UTC