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.
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.
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.
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))
note the uninstantiated meta ?M152 at the end corresponding to the sa argument of equiv_reflexive
my question / complaint: is it somewhat expected and if yes is there really no hope about legacy unification?
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.
Oh, you're right, I misunderstood the example. Actually unification performs arbitrary δ-unfolding so M152 just disappears.
But to give a bit more context, this shifts the burden on the Clenv algorithm for dependency computation.
I guess I'll have to dig deeper.
Pierre-Marie Pédrot has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC