The Coq mailing list

["Cristian Petrescu-Prahova" <cristipp AT gmail.com>]

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.

The ZArith development is:

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.

The The ZArith.Int development is:

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 Make_Int.

Alas, the fact_int definition fails with the following error message:

Error:
Recursive definition of fact_int is ill-formed.
In environment
fact_int : forall z : int, fact_domain_int z -> int
z : int
h : fact_domain_int z
hgt : z > 0
Recursive call to fact_int has principal argument equal to
"fact_domain_inv_int z h hgt"
instead of a subterm of h

Why is 'fact_domain_inv z h hgt' a subtem of h in fact definition, but
'fact_domain_inv_int z h hgt'  is not a subterm of h in fact_int
definition?

Any help and comments would be greatly appreciated.

Thank you,
Cristian