The Coq mailing list

[Pablo Argon <Pablo.Argon AT ircyn.ec-nantes.fr>]

Hello,

I'm trying to re-play  (using Coq 6.2.4 on linux) Eduardo Gimenez's
proof
of well-founded recursion given in the tutorial on recursive types
(http://pauillac.inria.fr/coq/ps/RecTutorial.v.ps) page 34,
with the div function.

The proof of div (p.36) doesn't save:

Theorem div: (x:nat)(y:nat)(Acc nat Lth x)->nat.
Proof.
 Fix 3;Intros x y H.
 Refine
   If (iseq x O) then O
    else If (iseq y O) then x
          else (S (div (minus x y) y ?)).
Apply (decrease x y); Assumption.
Guarded.

(*Coq says*)
 Condition violated : Recursive call applied to an illegal term
The recursive definition
[x,y:nat; H:(Acc nat Lth x)]
 Cases (iseq x O) of
   (left _) => O
 | (right a) =>
    Cases (iseq y O) of
      (left _) => x
    | (right a0) => (S (div (minus x y) y (decrease x y H a a0)))
    end
 end
is not well-formed

May someone explain me why?
Thank you all by advance,
                Pablo Argon

NB: follows the whole script I used.

====================================================================
        PABLO ARGON
        IRCyN (UMR 6597)
        École Centrale Nantes, 
        1 rue la Noë, BP 92101
        44321 Nantes cedex 3, 
        FRANCE 

        Tél: 02 40 37 69 23
        Fax: 02 40 37 69 30
====================================================================

(* Exemple du INRIA-Report 0221 (E.Gimenez) p33-ss *)

Require Minus.
Require Refine.
Require EqDecide.

Section Principle_of_double_induction.
Variable P: nat ->  nat -> Prop.
Hypothesis base_case1 : (x:nat)(P O x).
Hypothesis base_case2 : (x:nat)(P x O).
Hypothesis inductive_hyp : (n,m:nat)(P n m)->(P (S n) (S m)).

Fixpoint nat_double_ind [n:nat] : (m:nat)(P n m) :=
 [m:nat]<P>Cases n m of
    O     x   => (base_case1 x)
  | x     O   => (base_case2 x)
  | (S x) (S y)=>(inductive_hyp x y (nat_double_ind x y))
end.
End Principle_of_double_induction.


Inductive Lth [n:nat] : nat->Prop :=
  Lth_intro1: (Lth n (S n))
| Lth_intro2:  (m:nat)(Lth n m)->(Lth n (S m)).


Lemma minus_O : (n:nat)(minus n O)=n.
Proof.
 Destruct n;Auto.
Qed.

Lemma smaller: (x,y:nat)(Lth (minus x y) (S x)).
Proof.
(Intros x y; Pattern y x; Elim x using nat_double_ind; Intro n).
Cut (n:nat)(minus n O)=n.
Intro H.
Rewrite H.
Constructor 1.

Auto with v62.

Simpl.
Constructor.

Intros.
Simpl.
(Constructor 2; Assumption).
Qed.

Lemma smallerSS: (x,y:nat)~x=O->~y=O->(Lth (minus x y) x).
Proof.
(Destruct x; Destruct y;
 ((Simpl; Intros; Apply smaller; Assumption)) Orelse
  ((Intros; Absurd O=O; Auto with v62))).
Qed.

Theorem decrease:
 (x,y:nat)(Acc nat Lth x)->
   ~x=O->~y=O->(Acc nat Lth (minus x y)).
Proof.
Intros x m H.
Case H.
Intros n h xno yno.
Apply h.
(Apply smallerSS; Assumption).
Qed.

Theorem iseq: (x:nat)(y:nat){x=y}+{~x=y}.
Proof.
 Decide Equality.
Qed.


Grammar command command1 :=
ruleIf ["If"    command($c1)
        "then"  command($c2)
        "else"  command($c3)] ->
          [<<Cases $c1 of
               (left  _) => $c2 
              |(right _) => $c3 
             end>>].

(* ------------ fonction div ------------*)
Theorem div: (x:nat)(y:nat)(Acc nat Lth x)->nat.
Proof.
 Fix 3;Intros x y H.
 Refine
   If (iseq x O) then O
    else If (iseq y O) then x
          else (S (div (minus x y) y ?)).
Apply (decrease x y); Assumption.
Guarded.