`ecareful_unify` can't handle evars in if-then-else

[mansky1]

In investigating why sep_apply failed on a fairly simple example, I discovered that ecareful_unify (which ecancel uses to resolve evars) fails on if-then-else expressions.

Example:

Require Import VST.floyd.seplog_tactics.

Goal forall (a b c : bool), (if a then b else c) = if a then b else c.
Proof.
  intros.
  evar (a' : bool).
  replace a with a' at 2.
  unfold a'.
  Fail ecareful_unify.

For cancel this is only a minor annoyance, but for sep_apply it means that trying to apply a lemma with an if-then-else on the LHS of the |-- will fail with no useful error (unless all arguments are explicitly provided).

[QinshiWang]

Maybe I wrote this part of the code, but I cannot remember everything. ecareful_unify looks weaker than unify and do less evar instantiation. You want to unify if ?a then b else c with if a then b else c. This seems natural and enhancing ecareful_unify seems no harm.

[bcip]

I wrote this tactic because unify is too strong. But in what case unify is too strong?

On Fri, Jul 29, 2022, 5:29 PM Qinshi Wang @.***> wrote:

Maybe I wrote this part of the code, but I cannot remember everything. ecareful_unify looks weaker than unify and do less evar instantiation. You want to unify if ?a then b else c with if a then b else c. This seems natural and enhancing ecareful_unify seems no harm.

— Reply to this email directly, view it on GitHub https://github.com/PrincetonUniversity/VST/issues/609#issuecomment-1199958074, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVWI6MCBOYE5XROWFASUFLVWREMZANCNFSM54LDOFMQ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[andrew-appel]

As long as a,a' have type bool, then PR #684 fixes this. The more general case (arbitrary inductive datatype with two constructors) would be a bit more fiddly to implement.