The Coq mailing list

["Flavio L. C. de Moura" <flaviomoura AT unb.br>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi there,

  I defined a simple (but not structurally) recursive function, but I am
not able to play with it, and I would like to understand why...  The
function is

Require Import Recdef.

Function quotient (a b: nat) {measure (fun x => x) a} : nat :=
  match a,b with
    | _,0 => 0
    | 0,_ => 0
    | _,_ => match (nat_compare a b) with
               | Gt => S(quotient (a - b) b)
               | Lt => 0
               | Eq => 1
                 end
  end.
intros a b n H n0 H1 H2.
assert (S n > S n0).
generalize H2; clear H2.
apply <- nat_compare_gt.
apply lt_minus.
auto with arith.
auto with arith.
Defined.

And I would like to proof the following:

Theorem triv1 : forall a:nat, quotient (S a) (S a) = 1.
Proof.
  induction a.

I didn't manage to go further from now on:  quotient 1 1 = 1.

Why simpl doesn't apply the definition of quotient? I also tried to
defined other variations of this function but I get stuck at the very
same point... For instance, I also tried the following:

Program Fixpoint quotient (a b: nat) {measure (fun x => x) a} : nat :=
  match a with
    | 0 => 0
    | S n => match b with
               | 0 => 0
               | S m => if (le_gt_dec m n) then S (quotient (n - m) (S m))
                     else 0
             end
  end.
Obligation 1.
  omega.
Defined.


In addition, from the Coq documentation, I couldn't find a difference
between the constructions "Function" and "Program Fixpoint". Is there
any conceptual difference between them?

Thank you very much in advance!

Cheers.


-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkth5GwACgkQJ9M3XSenoWidngCfZOM6mgvOl4ezlVHeLpTldaG3
MosAoI4AGjKlFTHJwSWwbyYSo0OmroBq
=53qP
-----END PGP SIGNATURE-----