The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

I'm shamed, the paper is wrong, the implemented rule FixSpec is stronger ! 

it is 

Γ⊢f v ▶ b

Γ,g ▶ <,d ▶ ⊥,x ▶ b ⊢f u ▶ a

--------------------------------------------------------

Γ⊢f fixT′ g d x−→u t v ▶ a

which means in your example that's you've got ..., minus ▶ <, n0 ▶ <, m ▶ ⊥

There is an implicit recursion here. The rule says: suppose that the fixpoint is strictly smaller, compute the subterm value of its body.

I'm really really sorry for the mistake and I must put a corrected version somewhere … Thanks a lot for noticing !

Pierre B.

Le 10 janv. 2013 à 11:34, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> a écrit :

Hello Pierre,

thanks for the reference.

I was aware that the current Coq guardedness condition first reduces the body. However, still, the fully reduced version of my example

 fix foo (n : nat) : nat :=
   match n with
   | 0 => 0
   | S x => S (foo
      ((fix minus (n0 m : nat) {struct n0} : nat :=
        match n0 with
        | 0 => n0
        | S k =>
          match m with
          | 0 => n0
          | S l => minus k l
          end
        end) x 2))
   end

is not accepted by Giménez' guardedness condition (there the recursive argument of the recursive call to "foo" should be of the shape "z Q1 ... Qn" with "z" in the set of allowed variables). Here it is a "fix" construct.

I do not directly see whether it it covered by yours. Having a "fix" construct as the recursive argument of the recursive call to "foo" seems to be fine. While checking the body of the inner fix (after using the FixSpec rule) we have

 ..., minus ▶ ⊥, n0 ▶ <, m ▶ ⊥

After that, to check the body of the "S l" case in the second match, it seems to fail on

 minus k l

Am I missing something maybe?

Best,

Robbert

On 01/09/2013 12:17 PM, Pierre Boutillier wrote:

Hi,

The formal description of the current guardedness condition :
http://hal.inria.fr/hal-00651780

Very approximately (and the devil is in the details), it is Giménez
guardedness condition but on the weak head normal form of the body of
the fixpoint

(
    match n with
    | 0 =>  0
    | S x =>  S (foo (x - 2))
    end.
in your second example)

All the best,
Pierre B

On 09/01/2013 12:09, Robbert Krebbers wrote:

Hello,

today I noticed that the gcd function on nat is defined as follows

  Fixpoint gcd a b :=
    match a with
    | O =>  b
    | S a' =>  gcd (b mod (S a')) (S a')
    end.

I was quite surprised that this is accepted by Coq's guardedness
checker. After all, it is not obvious that (b mod (S a')) is indeed
structurally smaller than (S a').

Also an example like

  Fixpoint foo (n : nat) :=
    match n with
    | 0 =>  0
    | S x =>  S (foo (S x - 3))
    end.

is happily accepted.

This does not seem to be covered by, nor to be an obvious extension
of, the guardedness condition as defined in Giménez' 1994 "Codifying
guarded definitions with recursive schemes" to which (Chapter 4 of)
the reference manual refers.

Is there a formal description of the current guardedness condition
that captures the above cases? Or an intuitive explanation on what it
is doing to check these.

Robbert