coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] An error of 'Function'

From: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] An error of 'Function'
Date: Tue, 20 Apr 2010 11:04:52 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=Q06bPnbWaonN/iwPlpBAarvnKo3viKYpEHKBSQAYIgXMvq2IwTkyz2nMz5Guu098Gd ONMr/j+6QijqgpcAlYMapmjjLBxVkQcgTFwe+/BcIOCZTLGb0T3ouJRnFxdSdp34uU4c JkYNzmZ+t/PKDd+Cpgw0nNxPaFOb/DG62sRAs=

Hi,

I am using 8.2pl1.

Require Import Recdef.
Function test (n:nat) {measure (fun n=>n)} : unit :=
  (match n as n' return (n=n' -> _) with
  n => fun H:_=>
    match n with
    | O => tt
    | S n' => test n'
    end
  end) (refl_equal n).

>> Error: No such section variable or assumption: test.

It works if I removed either {measure} or pattern equalities,
or defined 'test' by 'Program'. Can we use 'dependent
equalities' in Function definitions?

Function test (n:nat) {measure (fun n=>n)} : unit :=
  (match n with
  n =>
    match n with
    | O => tt
    | S n' => test n'
    end
  end).

Function test (n:nat) : unit :=
  (match n as n' return (n=n' -> _) with
  n => fun H:_=>
    match n with
    | O => tt
    | S n' => test n'
    end
  end) (refl_equal n).

Program Fixpoint test (n:nat) {measure (fun n=>n)} : unit :=
  (match n as n' return (n=n' -> _) with
  n => fun H:_=>
    match n with
    | O => tt
    | S n' => test n'
    end
  end) (refl_equal n).

--
Jianzhou

[Coq-Club] An error of 'Function', Jianzhou Zhao