The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

Hi,

I got "Warning: Cannot define principle(s) for div2"
when generating functional inductive scheme:

Require Import Omega.
Definition test (n:nat) := n + 1.
Function div2 (n:nat) {measure (fun n'=>n')} : nat :=
 match n with
 | O => 0
 | S O => 0
 | S (S n') => S (div2 (test n'))
 end.
intros. subst. unfold test. omega. Qed.

Functional Scheme div2_ind := Induction for div2 Sort Prop.

>> Warning: Cannot define principle(s) for div2

But I can still use div2_ind for induction proofs.

Lemma div2_le' : forall n:nat, div2 n <= n.
intro n.
functional induction (div2 n).
auto. auto. unfold test in *. omega.
Qed.

If I defined 'div2' by recursion on {struct...}, it doesn't
report this warning. Does this warning affect anything
for a well-found measure Function?

"Program Fixpoint" is another feature for programming in Coq.
I found it is more convenient if the definition replies on
equalities from pattern-matching. Does "Program Fixpoint"
also support "inductive scheme"? Do we have any applications
which proved inductive properties for "Program Fixpoint"?

Thanks
-- 
Jianzhou