Stream: Coq users

Topic: correct lemma statement

view this post on Zulip zohaze (Mar 04 2024 at 17:11):

Definition mod_fun (first a: nat)(l: list nat) : nat:=
if beq_nat first 0  then a mod (length l) else (a+1) mod (length l).

I am using mod_fun in main function f' recusively, whose output is list nat. In main function simply
increase the value of a.(always start first=0 , a=0 , increase a till it becomes equal to length l and only first time
first is zero). Output list nat always contains more zeros than any other natural number.(Because f' always start with zero and get zero when a becomes equal to length l). I want to prove this statement,how to do it?

Last updated: Jun 23 2024 at 04:03 UTC