The Coq mailing list

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

Hi Beta and Hugo,

Thanks for the explanations; both were very helpful. What mostly surprised me 
in the example that I posted is that, while I did expect eauto to be able to 
find non-obvious solutions, I did not expect [unify x with true] to behave 
differently from [instantiate (1 := true)]. Neither did I expect calling 
[reflexivity] on [true = ?1] to produce anything else than [true] for [?1].

Thanks for the explanations!
Clément.

On 11/01/2015 10:25 AM, Beta Ziliani wrote:
> 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
>  
> <mailto: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.
>     >
> 
> 
>