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