The Coq mailing list

[Guillaume Allais <sbleune AT gmail.com>]

Hi Flavio,

I think that your definitions are a bit too complicated for what you want to do. I took the second one and let Coq infer the measure (when the measure is simple, it works well).

Here is the code :

__________________________________

Fixpoint quotient (a b: nat) : 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.

__________________________________

The term created is way smaller than the one obtained with your first try (if you don't see what I mean, just try "Print quotient_terminate").
The proof is quite easy with this definition :
__________________________________

Theorem triv1 : forall a:nat, quotient (S a) (S a) = 1.
Proof.
 induction a.
 trivial.
 unfold quotient.
 rewrite minus_diag.
 case (le_gt_dec (S a) (S a)) ; intro H.
 reflexivity.
 elim (gt_irrefl _ H).
Qed.

__________________________________

Cheers,

--
guillaume

On 28 January 2010 20:24, Flavio L. C. de Moura <flaviomoura AT unb.br> wrote:

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