Julin Shaji (Feb 01 2022 at 17:32): Julin Shaji (Feb 01 2022 at 17:32):I had been trying to convert a nat value into its constituent digits.
Like 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?
Paolo Giarrusso (Feb 01 2022 at 17:39):Since Nat.div n 10 is not a syntactic subterm of n, this requires well-founded induction.
Li-yao (Feb 01 2022 at 17:39):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?
Paolo Giarrusso (Feb 01 2022 at 17:41):Not sure they're worth learning (indeed I didn't, else I'd have linked them)
Li-yao (Feb 01 2022 at 17:51):Yeah there is a strong induction principle, but it doesn't spare you from the hard part of thinking about dependent types.
Kenji Maillard (Feb 01 2022 at 19:55):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