The Coq mailing list

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

In the manual of Coq 8.1, section 4.5.5 Fixpoint definitions,
I found the definition of "structurally smaller" as

//////////////////////////////////////////
The main rules for being structurally smaller are the following:
Given a variable y of type an inductive definition in a declaration 
Ind(\Gamma)[r](\Gamma_I := \Gamma_C ) where \Gamma_I is
[I1:A1;...;Ik:Ak], and \Gamma_C is [c1:C1;...;cn:Cn]. 

The terms structurally smaller than y are:
1) (t u),\x:u,t when t is structurally smaller than y .
2) case(c,P,f1 ... fn) when each fi is structurally smaller than y.
If c is y or is structurally smaller than y, its type is an inductive 
definition 
Ip part of the inductive declaration corresponding to y. Each fi corresponds 
to a type of constructor Cq = \p1:P1,...,\pr:Pr, \y1:B1,...,\yk:Bk; (I 
a1...ak) 
and can consequently be written \y1:B1',...,\yk:Bk',gi. 
(Bi' is obtained from Bi by substituting parameters variables) the variables
yj occurring in gi corresponding to recursive arguments Bi 
(the ones in which one of the Il occurs) are structurally smaller than y.
//////////////////////////////////////////

But, is the above definition completed? It does not give the basic element
that is smaller than y. Both Rule 1 and 2 base on the assumption that 
some smaller terms of y are already defined. Did I miss anything?

Jianzhou
----- Original Message ----- 
> From: "Jianzhou Zhao" 
> <jianzhou AT seas.upenn.edu>
> To: 
> <coq-club AT pauillac.inria.fr>
> Date: Fri, 11 Jan 2008 23:19:54 -0500
> Subject: [Coq-Club] Structural descrease for ad hoc recursion
> 
> Hey All,
> 
> I am the newbie of Coq and doing some experiments of adhoc recursion.
> One example from the online exercises of Coq'Art --
> /////////Start Coq///
> Require Import ZArith.
> Open Local Scope Z_scope.
> 
> Inductive fact_domain : Z -> Prop :=
> | fact_domain_zero :
>  fact_domain 0
> | fact_domain_pos :
>  forall z : Z, z >= 0 -> fact_domain (Zminus z 1) -> fact_domain z.
> 
> Theorem fact_domain_pos_true : forall z : Z, fact_domain z -> z >= 0.
> intros x H.
> case H.
> unfold Zge.
> discriminate.
> intros.
> assumption.
> Defined.
> 
> Theorem fact_domain_inv :
>  forall z : Z, fact_domain z -> z > 0 -> fact_domain (Zminus z 1).
> intros z H.
> case H.
> intros.
> discriminate.
> intros.
> assumption.
> Defined.
> 
> Fixpoint fact (z : Z) (h : fact_domain z) {struct h} : Z :=
> match Z_gt_le_dec z 0 with
>  | right hle =>
>    match Z_ge_lt_dec z 0 with
>      | right hlt => False_rec Z (fact_domain_pos_true z h hlt)
>      | left _ => 1
>    end
>  | left hgt =>
>    z * (fact (Zminus z 1) (fact_domain_inv z h hgt))
> end.
> /////////End Coq///
> 
> In this case, ad hoc recursion is defined based on the 'struct'
> fixpoint, too. But the decreased structure is h with the type 
> 'fact_domain z'. Now how does Coq figure out whether the recursive
> call of fact has the subterm of h? In the other word, how to define
> the subterm of h with the type 'fact_domain z'?
> 
> Thank you very much for advanced input.
> 
> Jianzhou
> 
> 
> 
> --__--__--
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> End of Coq-club Digest
>