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

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.
by move: w; rewrite mem_iota add0n; 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: May 28 2023 at 20:30 UTC