Trying to follow the course material in the Mathematical Components book (see here, I tried to mimic the type of the nat. The code is the followoing:
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope alt_nat_scope.
Open Scope alt_nat_scope.
Inductive alt_nat : Set :=
| N0
| NS of alt_nat.
Fixpoint alt_nat_leq (m n : alt_nat) {struct m} :=
match m, n with
| N0, N0 => true
| N0, NS n0 => true
| NS m0, N0 => false
| NS m0, NS n0 => alt_nat_leq m0 n0
end.
Notation "m <= n" := (alt_nat_leq m n) : alt_nat_scope.
Notation "m < n" := (alt_nat_leq (NS m) n) : alt_nat_scope.
Notation "m >= n" := (alt_nat_leq n m) (only parsing) : alt_nat_scope.
Notation "m > n" := (alt_nat_leq (NS n) n) (only parsing) : alt_nat_scope.
Fixpoint alt_addn (a b : alt_nat) :=
match b with
| N0 => a
| NS b0 => NS (a + b0)
end
where " a + b " := (alt_addn a b) : alt_nat_scope.
Fixpoint alt_subn (a b : alt_nat) :=
match a, b with
| N0, _ => N0
| NS a0, N0 => a
| NS a0, NS b0 => (a0 - b0)
end
where "a - b" := (alt_subn a b) : alt_nat_scope.
Fixpoint alt_muln (a b : alt_nat) :=
match a with
| N0 => N0
| NS a0 => (a0 * b) + b
end
where "a * b" := (alt_muln a b) : alt_nat_scope.
Definition One := NS N0.
Fixpoint f2 (m d q : alt_nat) :=
if (m - (d - One)) is (NS m') then f2 m' d (NS q) else (q, m).
Definition f1 (m d : alt_nat) :=
if (N0 < d) then f2 m d N0 else (N0, m).
The code of the function f2 follows the semantic of Euclidean division
as described at §5.4 of the book (Page 110). Rocq complains with the
message "Cannot guess decreasing argument of fix" when evaluating f2.
However, everything goes smoothly when the type alt_nat is replaced by
the standard nat type (with the straight forward adjustments).
How to explain/fix this issue? Thanks
There is very important subtle difference between you alt_subn and Nat.sub: the line N0 => N0 is N0 => a which gives the same result but makes the termination checking work. I though this was explained in the book but I don't remember precisely.