The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Sun, Jul 29, 2007 at 09:10:05PM -0700, Cristian Petrescu-Prahova wrote:
> Hello all,
> 
> I'm trying to understand how general recursion with ad-hoc predicate
> works. The idea to use ad-hoc predicates comes from Coq'Art, section
> 15.4. I am defining a factorial function over the Z domain. This works
> just fine if I am using the ZArith module, but fails in a way that I
> cannot comprehend if I try to use the axiomatized ZArith.Int module.
> The latter definition would help me understand how to use general
> recursion over axiomatized modules, and potentially help for faster
> extracted code.
> 
> The ZArith and ZArith developments are identical, except for the
> replacement of 'Z' with 'int',  the _int suffix added to all names.
> Here is what I am trying to do. Sorry for the relative length, I can't
> think of a simpler example to illustrate the problem.
> 

Hi Christian

Here comes a version that seems to work (both with Coq 8.1 and current
development version). In fact, I've just followed your approach:
lacking your exact "int" version (copy-paste error in your mail ?), 
I tried to reconstitute it as you said: replacement of Z to int.  
Most important point: I've kept the proofs as close as possible, just
placing some Zcompare_refl for what was directly computable in Z.

Without your exact fact_domain_inv_int proof it's hard to guess why 
yours is not considered as a subterm by Coq. Are you using "Defined" ? 
Have you started your proof by a "case H" as in the proof for Z ?

Best regards, 
Pierre Letouzey

PS: By the way, a better and more complete axiomatization for numbers
is currently being built par E. Makarov, you can have a look at
directory theories/Numbers of coq's development svn trunk (see
coq.gforge.inria.fr). The module Int is rather a quick hack I've
written to abstract finite set trees from Z (see FSets/FSetAVL.v).




Require Import Int.
Open Local Scope Int_scope.

Module Make_int (I:Int).
Import I.
Open Local Scope Int_scope.

Inductive fact_domain : int -> Prop :=
| fact_domain_zero :
  fact_domain 0
| fact_domain_pos :
  forall z : int, z >= 0 -> fact_domain (minus z 1) -> fact_domain z.

Theorem fact_domain_pos_true : forall z : int, fact_domain z -> z >= 0.
intros x H.
case H.
red.
rewrite Zcompare.Zcompare_refl.
discriminate.
intros.
assumption.
Defined.

Theorem fact_domain_inv :
  forall z : int, fact_domain z -> z > 0 -> fact_domain (minus z 1).
intros z H.
case H.
intros.
red in H0.
rewrite Zcompare.Zcompare_refl in H0.
discriminate.
intros.
assumption.
Defined.

Fixpoint fact (z : int) (h : fact_domain z) {struct h} : int :=
match gt_le_dec z 0 with
  | right hle =>
    match ge_lt_dec z 0 with
      | right hlt => False_rec int (fact_domain_pos_true z h hlt)
      | left _ => 1
    end
  | left hgt =>
    z * (fact (minus z 1) (fact_domain_inv z h hgt))
end.

End Make_int.