The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

On Nov 13, 2019, Samuel Gruetter 
<gruetter AT mit.edu>
 wrote:

> https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Tactics/syntactic_unify.v

I tried the syntactic_unify tactic from there, and it worked better
than the set method in some simple situations.  But unfortunately
syntactic_unify failed to unify some terms that look easy to unify.
(See below.)  And the original tactic I posted in the first message of
this thread is able to handle those.  So the current situation is

  my original tactic > syntactic unify method > set method

I'll post a separate message later asking for help with my original
tactic.

Here's how I tried to use syntactic_unify:

  let lemH := fresh "lem" in
  pose lem as lemH;
  insterU lemH;  (* put evars in for all arguments *)
  let src := source lemH in
      lazymatch goal with
      | |- ?lhs = _ =>
        match lhs with
        | context[?trm] =>
          syntactic_unify trm src;
          ...

I can't easily give a reproducible example of where it fails, since it
involves a large development using the HoTT library, but here are the
terms:

src:

  (@ap ?A (smash ?A ?B)
          (fun a : ?A => @smin ?A ?B (a, @point ?B (ispointed_type ?B))) 
          ?x
          ?y
          ?q0)

a sub-term of lhs:

  (@ap X (smash X Y)
         (fun x : X => @smin X Y (x, @point Y (ispointed_type Y)))
         (f (@point A (ispointed_type A)))
         (@point X (ispointed_type X))
         (@point_eq A X f))

(The @ at the start of the last line is like eq_trans.)

Both rewrite and my original tactic unify src with the sub-term
(probably using more ambient information), but both syntactic_unify and
the built-in unify fail.  If I help the latter two by doing some partial
unification, they succeed, so the terms are unifiable.

Any ideas?

Thanks again!

Dan