The Coq mailing list

["Adam Koprowski" <adam.koprowski AT gmail.com>]

   Dear David,
 
  I was trying to use this nice new way of defining fixpoint
functions in Coq but I run into trouble. Following your example I tried
to use syntax:
  { measure <measure_fun_name> <argument_name> } 
  but then Coq complains "No argument named
<measure_fun_name>" just as if it was trying to interpret the
name of the measure functions as an argument name. If I swap the order
of the arguments I get a usual error "Recursive call to <...> has
principal argument equal to <...> instead of a subterm of
<...>" just as if Coq was ignoring the measure declaration. Any
ideas what am I doing wrong? Below you'll find a more complete scriplet
that is somehow closer to what I'm actually trying to achieve.
   Any help greatly appreciated!
   Best wishes,
    Adam

===================================
Set Implicit Arguments.

Require Import List.
Require Import Relations.
Require Export Recdef.

Section STLC.

  Parameter BaseType : Set.

  Inductive SimpleType : Set :=
  | BasicType(T: BaseType)
  | ArrowType(A B : SimpleType).
  Notation "x --> y" := (ArrowType x y) (at level 55, right associativity) : type_scope.
  Notation "# x " := (BasicType x) (at level 0) : type_scope.
  Implicit Types A B C : SimpleType.

  Definition Env := list (option SimpleType).
  Definition EmptyEnv : Env := nil.
  Implicit Type E : Env.

  Definition VarD  E x A := nth_error E x = Some (Some A).
  Definition VarUD E x := nth_error E x = None \/ 
                         
nth_error E x = Some None.
  Notation "E |= x := A" := (VarD E x A) (at level 60).
  Notation "E |= x :!" := (VarUD E x) (at level 60).

  Definition decl A E := Some A::E.
  Infix "[#]" := decl (at level 20, right associativity).  

  Inductive Preterm : Set :=
  | Var(x: nat)
  | Abs(A: SimpleType)(M: Preterm)
  | App(M N: Preterm).

   (* Some notation for preterms *)
  Implicit Type Pt : Preterm.
  Notation "% x" := (Var x) (at level 20).
  Infix "@@" := App (at level 25, left associativity).
  Notation "s [ x ]" := (s @@ x) (at level 30).
  Notation "\ A => M" := (Abs A M) (at level 35).

  Reserved Notation "E |- Pt := A" (at level 60).
  Inductive Typing : Env -> Preterm -> SimpleType -> Set :=
  | TVar: forall E x A, 
            E |= x := A -> 
            E |- %x := A
  | TAbs: forall E A B Pt, 
            A [#] E |- Pt := B -> 
            E |- \A => Pt := A --> B
  | TApp: forall E A B PtL PtR, 
            E |- PtL := A --> B -> 
            E |- PtR := A -> 
            E |- PtL @@ PtR := B
  where "E |- Pt := A" := (Typing E Pt A).

  Record Term : Set := buildT { 
    env: Env;
    term: Preterm;
    type: SimpleType; 
    typing: Typing env term type
  }.
  Implicit Types M N T : Term.

  Fixpoint type_measure (A: SimpleType) : nat :=
  match A with
  | #B => 0
  | A --> B => S (type_measure B)
  end.

  Definition term_type_measure (T: Term) : nat := type_measure (type T).

  Definition isApp M : Prop :=
  let (_, _, _, typ) := M in
  match typ with
  | TApp _ _ _ _ _ _ _ => True
  | _ => False
  end.

  Definition appBodyL M : isApp M -> Term :=
  match M return (isApp M -> Term) with
  | buildT _ _ _ typ =>
      match typ return (isApp (buildT typ) -> Term) with
      | TApp _ _ _ _ _ L R => fun _ : True => buildT L
      | _ => fun notApp: False => False_rec Term notApp
      end
  end.
  Implicit Arguments appBodyL [M].

  Definition appBodyR M : isApp M -> Term :=
  match M return (isApp M -> Term) with
  | buildT _ _ _ typ =>
      match typ return (isApp (buildT typ) -> Term) with
      | TApp _ _ _ _ _ L R => fun _ : True => buildT R
      | _ => fun notApp: False => False_rec Term notApp
      end
  end.
  Implicit Arguments appBodyR [M].

  Variable R : Term -> Term -> Prop.
  Definition AccR := Acc (transp Term R).

  Fixpoint Computable (M: Term) {measure M term_type_measure} : Prop :=
  match (type M) with
  | #T => AccR M
  | TL --> TR =>
      forall P (Papp: isApp P) (PL: appBodyL Papp = M) (typeL: type P = TR),
    Computable (appBodyR Papp) ->
    Computable P
  end.
  
End STLC.

On 7/23/06, David Pichardie <david.pichardie AT irisa.fr> wrote:

Dear Adam,

You offer me a good occasion to make some advertisement about the new
Coq feature named Function.
In Coq8.1beta, you have now an easy way to define such functions.

You example is particularly easy to define using a measure function.
See the coq script below.
Function helps you to make proof too (which is often as hard as
programming...).
I you have something to prove on such a function I would be happy to
show you how
'function induction' can help you.

Function syntax is given here :
http://coq.inria.fr/V8.1beta/refman/Reference-Manual003.html#@command15

Coq script (using Coq 8.1beta http://coq.inria.fr/V8.1beta):

Require Export Omega.
Require Export Recdef.

Variable A : Set.

Inductive T : Set :=
| Ts: A -> T
| Tc: T -> T -> T.

Inductive V : Set :=
| Vc: T -> V.

(* Measure function to prove termination of Vfun *)
Fixpoint mesT (t:T) : nat :=
   match t with
    Ts a => 0
  | Tc t1 t2 => S (mesT t1 + mesT t2)
  end.

Definition mes (v:V) : nat :=
   let (t) := v in mesT t.

Lemma decrease_Vfun : forall t1 t2,
   mes (Vc t1) < mes (Vc (Tc t1 t2)).
Proof.
   intros; simpl; omega.
Qed.

(* Definition of Vfun *)
Function Vfun (v: V) {measure mes v} : A :=
match v with
| Vc (Ts a) => a
| Vc (Tc t1 t2) => Vfun (Vc t1)
end.
Proof.
   intros; subst; apply decrease_Vfun.
Qed.

(* Two usefull proofs have so been generated *)
Check Vfun_equation.
Check Vfun_ind.




Le 22 juil. 06, à 16:06, Adam Koprowski a écrit :

>
> Dear all,
> I wonder how one can persuade Coq that the Fixpoint definition is
> well-formed if the decrease of the argument is not completely obvious.
> For instance how to modify the definition of Vfun in the simple
> scriplet below to make it acceptable by Coq?
> Thanks in advance for any help,
> Adam
>
>
> Variable A : Set.
>
> Inductive T : Set :=
> | Ts: A -> T
> | Tc: T -> T -> T.
>
> Inductive V : Set :=
> | Vc: T -> V.
>
> Fixpoint Vfun (v: V) : A :=
> match v with
> | Vc (Ts a) => a
> | Vc (Tc t1 t2) => Vfun (Vc t1)
> end.
>
> --
> =====================================================
> Adam.Koprowski AT gmail.com , ICQ: 3204612
> http://www.win.tue.nl/~akoprows
> The difference between impossible and possible
> lies in determination (Tommy Lasorda)
> =====================================================
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-
David Pichardie
http://www-sop.inria.fr/everest/personnel/David.Pichardie/
post-doc in the EVEREST team
INRIA Sophia-Antipolis
2004 Route des Lucioles
BP 93, 06902 Sophia Antipolis Cedex
France
Phone: (+33) 4 92 38 71 97
Fax: (+33) 4 92 38 50 29

-- 

=====================================================
Adam.Koprowski AT gmail.com, ICQ: 3204612
http://www.win.tue.nl/~akoprows
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================