Stream: Coq devs & plugin devs

Topic: ✔ Legacy unification semantics


view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:17):

I know this is a trap question, but do we have any idea about the expected semantics for the Unification functions? I was naively expecting that if w_unify succeeds on t ~ u where t is meta-free, then after that t would be convertible to u. But there are actually not so complicated instances where this is just not true.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:17):

I came up with a simple example arising from the stdlib:

Definition relation (A : Type) := A -> A -> Prop.
Axiom Reflexive : forall {A : Type}, relation A -> Prop.
Axiom Equivalence : forall {A : Type}, relation A -> Prop.

Definition equiv {A} (R : relation A) (_ : Equivalence R) : relation A := R.

Axiom equiv_reflexive : forall (A : Type) (R : relation A) (sa : @Equivalence A R), @Reflexive A (@equiv A R sa).

Lemma respecting_equiv A B (R : relation B) :
  Reflexive (fun (f g : A -> B) => forall (x : A), R (f x) (g x)).
Proof.
apply equiv_reflexive.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:18):

apply internally tries to unify the goal with the type of its argument, but even after unification some metas remain unsolved, due to non-empty rel contexts.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:19):

More precisely on the problem

(Reflexive (forall _ : A, B) (fun f g : forall _ : A, B => forall x : A, R (f x) (g x)))
~
(Reflexive ?M150 (equiv ?M150 ?M151 ?M152))

the unification produces the result

(Reflexive (forall _ : A, B) (equiv (forall _ : A, B) (fun f g : forall _ : A, B => forall x : A, R (f x) (g x)) ?M152))

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:20):

note the uninstantiated meta ?M152 at the end corresponding to the sa argument of equiv_reflexive

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:21):

my question / complaint: is it somewhat expected and if yes is there really no hope about legacy unification?

view this post on Zulip Guillaume Melquiond (Apr 27 2023 at 11:24):

I don't understand what the issue is. There is nothing to unify ?M152 with, is there? So, it seems expected that it is still there at the end.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:28):

Oh, you're right, I misunderstood the example. Actually unification performs arbitrary δ-unfolding so M152 just disappears.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:28):

But to give a bit more context, this shifts the burden on the Clenv algorithm for dependency computation.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2023 at 11:30):

I guess I'll have to dig deeper.

view this post on Zulip Notification Bot (Apr 27 2023 at 11:30):

Pierre-Marie Pédrot has marked this topic as resolved.


Last updated: Nov 29 2023 at 22:01 UTC