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: Oct 13 2024 at 01:02 UTC