The Coq mailing list

[George Van Treeck <treeck AT yahoo.com>]

I have run into a problem where Coq seems to arbitrarily stop importing lemmas from a file.

All the lemmas in the file have proofs. But, the last couple return the error message:

Error: The reference ... was not found in the current environment.

The coq reference manual doesn't say why this error might occur when importing lemmas.

Searching the net does not provide any useful info on this.

Is this a known bug in version 8.4 of Coq,

or a limit on the number of imported lemmas,

or some undocumented requirement for a lemma to be visible when imported?

The following is a lemma that won't import:

(* Delta-epsilon proof. limit c->0,

  0 < |c - 0| < delta => |M - s| < epsilon. *)

Lemma M_minus_exact_size_lt_epsilon :

    forall a b c delta epsilon: R,

    c <> 0 /\ 0 < delta /\ 0 < epsilon /\ delta = epsilon /\

    0 < Rabs (c - 0) < delta ->

    Rabs(M a b c - exact_size a b) < epsilon.

Proof.

  intros. decompose [and] H.

  assert (Rabs (c - 0) = Rabs c).

    auto with *.

  rewrite -> H5 in H6.

  assert (Rabs(M a b c - exact_size a b) < Rabs c).

    apply abs_M_minus_s_lt_abs_c. exact H0.

  rewrite H3 in H6. revert H6. revert H7.

  apply Rlt_trans with

    (r1 := Rabs (M a b c - exact_size a b))

    (r2 := Rabs c)

    (r3 := epsilon).

Qed.

Other lemmas that use the function definitions "M" and "exact_size" import without a problem.

-George