## Stream: Coq users

### Topic: How to apply `Wf_Z.natlike_ind`?

#### Daniel Hilst Selli (Jan 19 2022 at 22:48):

I have this small example

``````Import Coq.Init.Datatypes.
Require Import BinInt.
Require Import Coq.ZArith.Wf_Z.
Open Scope Z_scope.

#[bypass_check(guard=yes)]
Fixpoint sum (i : Z) :=
if i =? 0 then
0
else
i + sum (i - 1).

Fixpoint sum' (i : nat) : nat :=
match i with
| O => 0
| S i' => (i + sum' i')%nat
end.

Lemma sums_eq : forall (z : Z),
sum z = Z.of_nat (sum' (Z.to_nat z)).
intros.
induction z using Wf_Z.natlike_ind.
``````

A t this point I got this error `Not the right number of induction arguments (expected 2 arguments).` I have no idea how to apply this induction principle, I tried multiple `with ...` combinations `refine (Wf_Z.natlike_ind _ _)`,

#### Ana de Almeida Borges (Jan 19 2022 at 23:53):

I also don't know how to do it with `induction`. You can manage with `apply` if the goal is of the right form. Here it isn't, since `Wf_Z.natlike_ind` is a statement about non-negative integers, so if you add that assumption you can use `apply` directly:

``````Lemma sums_eq : forall (z : Z),
0 <= z -> sum z = Z.of_nat (sum' (Z.to_nat z)).
Proof.
apply Wf_Z.natlike_ind.
``````

#### Ana de Almeida Borges (Jan 20 2022 at 00:01):

Off topic, but your `sum` function doesn't terminate when the input is negative. I guess you know this, since you disabled the guard checker. It's kind of a weird function to define, I would at least change it so that it sends all negative numbers to 0 or something. Then you can actually prove your original `sums_eq` statement.

#### Daniel Hilst Selli (Jan 20 2022 at 12:44):

Thank you Ana! It was easier than I thought. About the sum function, in my real problem I have a function with this kind of base case `if something <= 0 then return blablabla` and I need to verify it, so I can't redefine. I just adapted the code to create an minimal example for the question

Last updated: Sep 23 2023 at 15:01 UTC