Ad-hoc totality proof

[ypytomets]

There's cases, when build-in checker is not able to verify totality.
There's some workarounds, like add extra index to data type to proof structural recursion, or create a data wrapper as a single recursion step for the mutual recursion case, or split proof on several explicit cases over simpler data types. But that requires additional term-level boilerplate, and can lead to reducing computational complexity, extra runtime overhead, worse overall concept splitting and codebase readability.

That would be handy instead of constraining hacky workaround for each such case for developers just to allow to write custom ad-hoc proof strategies (on meta/reflection level, which wouldn't affect actual runtime), instead of just believe_me: that can improve the actual correct code development speed without wasting time on workarounds and/or extra compiler proposals (and can be a convenient local sandbox for such potential proposals eventually).

[buzden]

I would definitely agree with that need. I also thought about it in the past, and I called my idea a first-class totality proofs.

This is not a well-thought thing, rather a bunch of ideas. To prove totality of some (potentially mutually) recursive call, we need to assure that on every path some well-founded metric strictly decreases. This proof may consist of stages where this metric decreases strictly and non-strictly (i.e. when m' < m and m' <= m respectively). First, we need to set up some metric, and then we can define a data type that proves that this metric holds in one of these two forms for a pair of expressions. Roughtly,

data Less : Metric mt => mt -> a -> b -> Type
data LessEq : Metric mt => mt -> a -> b -> Type

We could have some standard metric of structural decreasing:

data Structural : Type
implementation Metric Structural where ...

Then, we definitely know (and compiler can safely assume) that for every constructor C and every its argument x we have

%hint
C_x : Less Structural x (C ... x ...)

Also, we definitely have

%hint
relax : Less m a b => LessEq m a b

and

%hint
transR : Less m a b => LessEq m b c => Less m a c
%hint
transL : LessEq m a b => Less m b c => Less m a c

Then, we could change the totality checker to assume totaliy if every argument on every path has its appropriate Less implementation in the current context.

Having that we can, e.g., prove, say, that

map_preserves_tot : (f : a -> b) -> (xs : List a) -> LessEq Structural xs (map f xs)
tail_strictly_less : (xs : List a) -> NonEmpty xs -> Less Structural (tail xs) xs

and similar things. Sometimes we can use believe_me for that, or at least, postpone proofs with typed holes. Anyway, use of such unsafe hacks is very limited, and I think they are strictly better and safer than status quo.