The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

In my coq 8.4, "apply l0" gives the error message but "eapply l0" succeeds.

Gil

On Tue, Nov 6, 2012 at 10:41 AM, Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr> wrote:

Hi Coq-club !

I have a strange behavior in presence of existential variables in my Coq development, and I would be happy to see whether it is well-known and whether there is a well-known solution. The development is quite big, so here is a smaller example that "somewhat" exhibits the core of what I identify as beeing the problem (the problems appears in both Coq 8.3pl4 and 8.4):

Require Import List.

Definition tuple (types:list Type) : Type :=
  fold_right prod unit types.

Inductive A : Type :=
  | A_constr1.

Definition typlst  (a:A) : list Type :=
  match a with
    | A_constr1 => (nat:Type)::nil
  end.

Definition pred0 (l:tuple nil) : Prop := True.

Definition pred1 (l:tuple (typlst A_constr1)) : Prop :=
  True.

Lemma l0 : forall x, pred0 x -> pred1 (1,x).
Proof.
eauto.
Qed.

Lemma l1 : exists x, pred1 x.
Proof.
eexists.
apply l0.

When trying to execute the last tactic, Coq complains with:

Toplevel input, characters 6-8:
Error: Impossible to unify "(?245 * ?246)%type" with
 "tuple (typlst A_constr1)".

Now, I actually have two problems:

1- I would have expected Coq to reduce "tuple (typlst A_constr1)" in order to unify it. It is even more frustrating knowing that the problem occurs at the type level, where everything is known by Coq, and where it suffices to reduce terms in order to unify them. I actually don't even know why it created those existential type variables ?245 and ?246, as there value are trivially known as being the types of 1 and x in l0...

2- In my full development, the error message is even stranger (however, I cannot reproduce this behavior in this smaller example): it says something which would be analogous to:

Error: Impossible to unify "(?245 * ?246)%type" with
 "tuple ?240".

Based on the existential variables numbering, ?240 has been created during the execution of eexists (it is actually "eexists t", where t contains a wildcard), but ?240 *has been instantiated* during "eexists", so it should no longer appear anywhere.

So, what do you think ?

Thank you,
--
Jacques-Henri Jourdan