The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

My 2cts:

Using our algorithm you get the other solution, so effectively the goal is [false = true]. (Similarly for the larger program.)

But, as Hugo said, that is just a heuristic. It works in many cases (like yours), but sometimes it fails. What I foresee in a hopefully-not-so-far-away future is an algorithm with all the heuristic clearly explained in the Reference Manual, with switches to turn on and off certain heuristics. There is no way one algorithm will fit everyone's expectancies, but at least we can give tools for the interested proof developer (e.g., me!).

Best regards,

Beta

On Sat, Oct 31, 2015 at 7:30 PM, Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi Clément,

I might try to give some comments.

First, about your f_nil example, there are indeed two say "canonical"
solutions [a |- ?b:=a] and [a |- ?b:=nil] (*) and Coq heuristically
chooses the first one, and, in this case, one could indeed consider
that it should at least not commit to a solution (as a comparison, in
versions up to 8.2, Coq was doing the other choice!). I don't know
what Beta and Matthieu's algorithm is doing here.
 

(*) Of course, there are also less canonical solutions such as
e.g. [?b:=match a with nil => nil | _ => cons 0 (cons 0 nil) end], etc.


Second, I realized that there is a simple way in 8.5 to force the
choice of the second solution (i.e. nil). Just do

Unshelve.
[b]:clear a; shelve.

before the apply, so as to cut the dependency of ?b into the
substitution [a:=nil].

Actually, I even have a patch which allows to directly apply tactics
on goals of the shelve, where the two lines above (actually working as
such only when exactly b is on the shelve) can simply be replaced by:

[b]:clear a.

However, we are in the process of releasing 8.5beta3 soon and we did
not decide yet whether this patch shall go in it or if it will go only
to 8.6.

Note in passing that the trick is also applicable to Jonathan's issue
from 10 days ago.


Third, there is phenomenon in your example which is specific to the
fact that you are in the constant case nil. If you had f_cons instead
of f_nil as in

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

Lemma f_cons : forall a l, f (cons a l) (cons a l).
Proof. intros. exact I. Qed.

Goal forall (a: list nat), exists b, f a b.
Proof.
 intros.
 eexists.
 induction a as [|n l].
 2:apply f_cons.

Then, the second solution above (i.e. [?b:=cons n l] is not anymore a
solution, because ?b can depend on n and l only via its dependency in
[a:=cons n l], since n and l are bound below ?b.

So, what looks to you expected (choosing ?b:=nil in the nil case
rather than ?b:=a) is actually possible because we are in a degenerate
case where the constructor has no argument. So, the schema that you're
expecting does not scale to non-constant constructors.


In any case, Coq's unification algorithm has been developed
progressively from case studies and heuristics, starting in the mid
90's. In some cases it works as expected (for instance the heuristic
choosing "a" in the nil case is good for inference of the return
clause of a "match") and in some cases not, and I'm not able to assert
that there is a "universal" algorithm and combination of heuristics
that work always as intuitively expected. This is to me
research/engineering problem and that's good that people like Beta and
Matthieu did the effort to start formally writing on paper some of the
ingredients involved in Coq's unification.

Hoping it helps.

Hugo

On Fri, Oct 30, 2015 at 12:29:21PM -0400, 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.
>