The Coq mailing list

[Martin Bodin <martin.bodin AT inria.fr>]

Hi again,

I can't say that I really have a minimalistic example, but I found 
something related (trying to focus more and more on the problematic 
parts). From what I've understood, this is actually not “Qed”’s guilt, 
but the general mechanism that adds a term in the environment.

Here is how my code looks like: I first define a dummy environment like 
the following.
Definition E := write_env initial "x"%string Sign.tops.

This environment is an abstract environment, equipped with a lattice 
structure: this is why having a close context is difficult… But here is 
a look at the definition of “write_env”:
Print write_env.
write_env =
fun (E : aEnv) (x : var) (v : aVal) =>
MapDefault.write var aValVar var_OrderedType
  (SumLattice.Lattice aVal (LiftBot.t UnitLattice.t) Sign.LatticeDec
     (LiftBot.Lat UnitLattice.t UnitLattice.Lat)) E x
  (Some (inl v))
     : aEnv -> var -> aVal -> aEn
This definition—using “MapDefault.write” which is at its turn defined 
using a lot of complex definitions—is I think sufficiently complex to 
cause problem if Coq wants to unfold it until the end. But Coq accepts 
this definition without problem.

However the following definition freezes:
Definition test_freezes : forall e, e = E -> True :=
  fun e (_ : e = E) => I.
What is more surprising is that the following axiom definition also freezes:
Axiom test_freezes : forall e, e = E -> True.

This thus seems not to be “Qed”’s guilt, but some computations’s (a 
normal form computation?) performed after it, when adding a term into 
Coq's context.

However, the following definition works without problem:
Definition test_doesn_t_freeze : E = write_env initial "x"%string 
Sign.tops := eq_refl.
Also, the following lemma statement is accepted, and only freezes at the 
“Qed”:
Lemma test_doesn_t_really_freeze : forall e, e = E -> True.
Proof.
  exact (fun e (_ : e = E) => I).
Qed. (* Freezes at this line, but not at the lemma definition. *)

Did you already heard of such a phenomenon? Is that plausible that the 
exact cause of my problem is because of some additional computations 
performed after the definition of an object?

I don't know if that can help, but I'm on Coq 8.4pl2.

I have to admit being really surprised to discover such a thing in Coq, 
naively thinking that “Axiom” wasn't doing any work other than typing…
Any ideas are welcomed!
Thanks again,
Martin.

> > And what happens when you are trying:
> >
> > Definition test : A -> B -> C := fun a => proj1 T.
> > Does it take a long time ?
>
> Hi,
> Yes! It does take the “same” (I didn't see it terminate) amount of 
> time. I thus guess that the “exact” tactic does less work than I thought.
>
> I'm afraid that Gregory Malecha is right: I'll work on a minimalistic 
> example runnable without library… and trying to add explicit types to 
> the problematic terms.
>
> Thanks a lot for your help! I've learned about “Qed” ;-)
> Martin.