Stream: math-comp users

Topic: why guard does not complain?


view this post on Zulip Andrey Klaus (Apr 27 2023 at 00:46):

Hello!

In mathcomp book we have such a definition

Definition edivn_rec d :=
  fix loop m q := if m - d is m'.+1 then loop m' q.+1 else (q, m).

It looks to me like m' is not a direct subterm of m (at least it is not obvious (isn't it??)).
Why then the guard does not complain here?

view this post on Zulip Andrey Klaus (Apr 27 2023 at 01:04):

I was able to find this one https://proofassistants.stackexchange.com/questions/1428/formal-description-of-coq-s-termination-checker
if somebody can give a link to simpler description, would be great still.

view this post on Zulip Pierre Roux (Apr 27 2023 at 06:21):

The positivity checker is able to find that Nat.sub m d is a subterm of m thanks to the way Nat.sub is written.


Last updated: Jul 15 2024 at 19:01 UTC