I had been trying to convert a nat value into its constituent digits.
nat2nats 1234 giving
[1; 2; 3; 4].
So I did:
Require Import List. Import ListNotations. Fixpoint nat2nats (n : nat) : list nat := match n with | O =>  | _ => ((Nat.modulo n 10) :: nat2nats (Nat.div n 10) ) end.
but couldn't figure out a way to show that
n is decreasing on recursive calls and got error like:
Recursive definition of nat2nats is ill-formed. In environment nat2nats : nat -> list nat n : nat n0 : nat Recursive call to nat2nats has principal argument equal to "Nat.div n 10" instead of "n0". Recursive definition is: "fun n : nat => match n with | 0 =>  | S _ => Nat.modulo n 10 :: nat2nats (Nat.div n 10) end".
How can we get around this?
Nat.div n 10 is not a syntactic subterm of
n, this requires well-founded induction.
Two standard approaches are
Fixpoint nat2nats_fuel (fuel : nat) (n : nat) : list nat := match fuel with | O =>  | S fuel => ... nat2nats_fuel fuel (n / 10) ... end.
For naturals, aren't there also specialized functions for well-founded induction on smaller numbers?
Not sure they're worth learning (indeed I didn't, else I'd have linked them)
Yeah there is a strong induction principle, but it doesn't spare you from the hard part of thinking about dependent types.
To expand on Li-yao's first point, here is an example with well-founded induction using Equations (v1.3) :
Require Import List. Import ListNotations. Require Import Lia. From Equations Require Import Equations. (* The obligation system is slightly getting in our way so we deactivate it *) Obligation Tactic := idtac. Equations? nat2nats (n : nat) : list nat by wf n lt := | O =>  | _ => ((Nat.modulo n 10) :: nat2nats (Nat.div n 10) ). Proof. (* Goal corresponding to the well-founded recursive call : Nat.div n 10 < S n *) apply PeanoNat.Nat.div_lt_upper_bound; lia. Qed.
Last updated: Oct 03 2023 at 02:34 UTC