The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Clément,

The unification heuristics involving evar instances is a feature, 
although not a perfect one.  There are (at least) two reported bugs 
against it: 3141 and 3918.  Both still exist in recent 8.5 (I'm using 
7bf9bbe).

I have been bitten by both cases (a bad heuristic [3918], and 
unification prevented due to lack of a heuristic [3141]).

-- Jonathan

On 10/30/2015 12:29 PM, Clément Pit--Claudel wrote:
> 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.