The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi coq-club,

I'm slightly puzzled by the behaviour of unification in the following script 
(tested in 8.4pl4 and trunk):

    Goal forall (a: bool), exists b, a = b.
    Proof.
      intros a; eexists.

      destruct a.
      (* Two goals: [true = ?6] and [false = ?6] *)

      apply eq_refl.
      (* One goal: [false = false] *)
    Abort.

Instead of [false = false], I expected the second goal to become [false = 
true]. Unifying explicitly, instead of applying [eq_refl], yields similar 
results (this example courtesy of my labmate CJ):

    Goal forall (a: bool), exists b, a = b.
    Proof.
      intros a; eexists.

      destruct a.
      (* Two goals: [true = ?6] and [false = ?6] *)

      match goal with |- _ = ?x => unify x true end.
      (* Two goals: [true = true] and [false = false] *)
    Abort.

What seems to happen is that Coq remembers that [a] was destructed into 
[true] in the first branch, and silently replaces [true] by [a] (taken from 
the evar's context) when unifying (thus yielding [false] in the second 
branch). This behaviour is biting me in a larger example, which boils down to 
this:

    Definition f (a b: list nat) :=
      match b with
      | nil => True
      | _   => False
      end.

    Lemma f_nil : f nil nil.
    Proof I.

    Goal forall (a: list nat), exists b, f a b.
    Proof.
      eexists.
      induction a.
      apply f_nil.
      (* Unprovable: the [nil] that comes from applying [f_nil] shouldn't 
have been rewritten to [a] in the inductive case *)

Is this considered a bug, or a feature? And is this behaviour still present 
in Beta's and Matthieu's new unification algorithm?

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature