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: Sep 25 2023 at 14:01 UTC