2
$\begingroup$

Problem

I have a function leb defined in one of the (transitively) imported file: Types.v. However, calling it in my current file (Structures.v) doesn't "evaluate" to a value. Instead, it expands to itself, which is unexpected.

To illustrate what I mean, here is the layout of the Coq project directory: (Note: Relevant file content are quoted as strings.)

$PROJECT_ROOT
|- _Coqproject
   "-Q . DMFP"
|- Types.v
   "Fixpoint leb (n m : nat) : bool := ..."
|- Recursion.v
   "Require Export DMFP.Types. ..."
|- Structures.v
   "Require Export DMFP.Recursion. ..."

As you can see, the function leb is defined in Types.v. But when I tried to use it in Structures.v, it computes to itself:

Compute (leb 2 3).

gives this:

     = leb 2 3
     : bool

Then,

Print leb.

gives this:

*** [ leb : nat -> nat -> bool ]

Arguments leb (n m)%nat_scope

Questions

  1. Why does leb expands to itself?
  2. What does *** [ leb : nat -> nat -> bool ] mean with Print leb.?
  3. How to make leb available in Structures.v, such that I can use leb as in Types.v where it is defined?

Thank you!

$\endgroup$
2
  • 1
    $\begingroup$ I couldn't reproduce this. I copied your file structure and defined leb as expected. The main difference was that I also added a Makefile (this one, that I copied from somewhere but I don't remember where) and included the file names in the _CoqProject so that make could compile everything. Then I obtained the expected outputs in Structures.v, not the ones you did. Question: what happens when you Compute and Print in Types.v? Are you sure this is related to doing it on a different file? $\endgroup$
    – Ana Borges
    Jun 1 at 10:54
  • $\begingroup$ Thanks, Compute and Print are indeed working fine in Types.v. $\endgroup$
    – zacque
    Jun 1 at 11:16

1 Answer 1

5
$\begingroup$

Your outputs are consistent with leb being defined as a parameter, not as a specific function. So, for example:

Parameter leb : nat -> nat -> bool.

Compute (leb 2 3).
(*     = leb 2 3
     : bool
*)

Print leb.
(*
*** [ leb : nat -> nat -> bool ]

Arguments leb (_ _)%nat_scope
*)

Compare with having an actual definition for leb:

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S k =>
      match m with
      | O => false
      | S k' => leb k k'
      end
  end.

Compute (leb 2 3).
(*
     = true
     : bool
*)

Print leb.
(*
leb = 
fix leb (n m : nat) {struct n} : bool :=
  match n with
  | 0 => true
  | S k => match m with
           | 0 => false
           | S k' => leb k k'
           end
  end
     : nat -> nat -> bool

Arguments leb (n m)%nat_scope
*)

I'm guessing at this point, but here is what could have happened:

  1. You stated the existence of leb in Types.v without giving it a definition (eg with Fixpoint leb (n m : nat) : bool. Admitted.)
  2. You compiled Types.v
  3. You went back to Types.v to fill in your definition of leb
  4. You started working on Structures.v without compiling Types.v again, and so it was still using the old version where you hadn't filled in the definition for leb yet.

If this is not what's happening, then please provide more details. As I explained in my comment, I can't reproduce your data.

$\endgroup$
3
  • $\begingroup$ Thanks! Indeed your guess is right, after compiling Types.v and Recursion.v again, now the function can be used normally in Structures.v. $\endgroup$
    – zacque
    Jun 1 at 11:23
  • $\begingroup$ Not sure why, I thought Proof General will auto compile some .v files on demand. because when I'm just getting started yesterday, I started seeing .vo being produced without me invoking any command. $\endgroup$
    – zacque
    Jun 1 at 11:25
  • $\begingroup$ Another solution is to make clean and make build again. $\endgroup$
    – zacque
    Jun 1 at 11:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.