The Coq mailing list

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

Is there any improvement if you use:

Definition E : @aEn <explicitely put the implicits arguments here> := write_env initial "x"%string Sign.tops.

This is a good idea. I guess that it might help Coq knowing what kind of types I want.
In this context “aEnv”, the type of “E”, has no implicit arguments, but I can retry the tests passing every implicit argument I can.

The definition of “E” naturally works:
Definition E : @aEnv := write_env initial "x"%string Sign.tops.

Erratum, the following definition doesn't work (sorry, I guess that I didn't checked enough last time… :-\ ):
Definition test1 : E = write_env initial "x"%string Sign.tops := eq_refl.
And this similarly doesn't work:
Definition test2 : (E : @aEnv) = (write_env (initial : aEnv) "x"%string Sign.tops : aEnv) := @eq_refl (@aEnv) E.

However, this works (I've double checked, because I though that this really was the same than the definition of “test1” above):
Lemma test3 : E = write_env initial "x"%string Sign.tops.
Proof. reflexivity. Qed.

And just to be sure:
Set Printing All.
Print test3.
test3 = @eq_refl aEnv (write_env initial (String (Ascii.Ascii false false false true true true true false) EmptyString) Sign.tops)
 : @eq aEnv E (write_env initial (String (Ascii.Ascii false false false true true true true false) EmptyString) Sign.tops)

The fact that this is accepted by Coq but not the other ones makes me feel very strange about this.

Let's continue. The following freezes:
Axiom test4 : forall (e : aEnv), e = (E : aEnv) -> True.
Similarly, this one freezes:
Definition test5 : forall (e : aEnv), e = (E : aEnv) -> True := fun (e : aEnv) (_ : e = (E : aEnv)) => I.

This works:
Section Test.
Variable A : aEnv.
Lemma test6 : forall e, e = A -> True.
Proof. auto. Qed.
End Test.
Print test6.
test6 = fun (A e : aEnv) (_ : @eq aEnv e A) => I
  : forall A e : aEnv, @eq aEnv e A -> True
Arguments A, e are implicit

But not this, that freezes:
Definition test7 : forall e : aEnv, e = E -> True := @test6 E.

And this freezes at the “Qed”:
Lemma test8 : forall e : aEnv, e = (E : aEnv) -> True.
Proof.
  auto.
  Show Proof. (* (fun (e : aEnv) (_ : @eq aEnv a (E : aEnv)) => I) *)
Qed.

I have to admit being completely lost… I'll try to simplify the most I can next week.
And thanks again for your attention!
Martin.