The Coq mailing list

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

Hi,

Thanks for your tips.

> There is different ways in Coq for defining such a function. One is to
> use the 'Function' definition:
>
> Function SumFilterZRec (z: Z) (filter: Z -> bool) (hi: Z) {wf Zgt z} :
> [...]

This seems to be a pretty cool concept. Finally I got it through with  
a different WF relation (using Zwf).



Require Import ZArith.
Require Import Recdef.
Require Import Zwf.
Open Scope Z_scope.

Parameter hi : Z.
Parameter lo : Z.
Parameter filter : Z -> bool.

Definition ZltWf : Z -> Z -> Prop :=
  fun x y : Z => Zwf lo x y.

Function SumFilterZRec (z: Z) {wf ZltWf z} :
Z :=
  match Zcompare lo z with
  | Lt => if filter z then
            z + SumFilterZRec (z-1)
          else
            SumFilterZRec (z-1)
  | _ => 0
  end.
  Proof.
  intros; split;
    [cut (lo < z);
      [omega
      |red;assumption]
    |omega].
  intros; split;
    [cut (lo < z);
      [omega
      |red;assumption]
    |omega].
  apply (Zwf_well_founded lo).
  Qed.

Definition SumFilterZ : Z :=
  match Zcompare lo hi with
  | Lt => SumFilterZRec hi
  | _ => 0
  end.





Best regards
  Hermann ^[:wq

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