The Coq mailing list

[Hermann Lehner <hermann.lehner AT inf.ethz.ch>]

Hi,

I'm trying to define a function 'SumFilterZ' in Coq that corresponds to 
the addition of all integers between 'lo' and 'hi' if 'filter' is true.

The straight-forward idea that I appended below does not work as Coq can 
not check (syntactically) that it's well founded... I guess :)

Can anyone give me the "right and proper" way to define 'SumFilterZ'?

Thanks a lot for some help!

Best Regards
  Hermann Lehner


Require Import ZArith.
Open Scope Z_scope.

Fixpoint SumFilterZRec (z: Z) (filter: Z -> bool) (hi: Z) {struct z} : Z :=
  match Zcompare z hi with
  | Lt => if filter z then
            z + SumFilterZRec (Zsucc z) filter hi
          else
            SumFilterZRec (Zsucc z) filter hi
  | _ => 0
  end.

Definition SumFilterZ (filter : Z -> bool) (lo : Z) (hi : Z) : Z :=
  match Zcompare lo hi with
  | Lt => SumFilterZRec lo filter hi
  | _ => 0
  end.


--
http://www.hermann-lehner.com