The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

In this particular case, doing the following solves the issue in 8.3.

Lemma l1 : exists x, pred1 x.
Proof.
simpl.
eexists.
apply l0.
(* some existential variables are still undefined here*)
Qed.

In a nutshell, doing simpl before the eexists changes the type of the
existential variable into a product, and makes it possible to apply
l0.
Thomas


On Tue, Nov 6, 2012 at 11: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.
>
>
> 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