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 _ _)`

,

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.
```

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.

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: Jun 16 2024 at 03:41 UTC