Problem with high order unification

Stream: lean4

[Tomas Skrivan]

I have encountered a problem with high order unification that I would like to understand properly.

It looks like that λ x => ?m x (f x) can be unified with λ x => (f x * g x)

but λ f x => ?m x (f x) can't be unified with λ f x => (f x * g x)

To test this I have this mwe:

-- Test to unify `λ x => ?m x (f x)` with `λ x => (f x * g x)`
class D (F : (α → β))
instance bar (g : α → β → γ) (f : α → β) : D (λ (x : α) => g x (f x)) := ⟨⟩
example (g f : Nat → Nat) : D λ (x : Nat) => (f x * g x) := by apply bar _ _

-- Test to unify `λ f x => ?m x (f x)` with `λ f x => (f x * g x)`
class C (F : (α → β) → (γ → δ))
instance foo (g : α → β → γ) : C (λ (f : α → β) (x : α) => g x (f x)) := ⟨⟩
example (g : Nat → Nat) : C λ (f : Nat → Nat) (x : Nat) => (g x * f x) := by apply foo _ -- works
example (g : Nat → Nat) : C λ (f : Nat → Nat) (x : Nat) => (f x * g x) := by apply foo _ -- fails

---

I would like to test the unification directly i.e. create an expression with and without metavariables and test if they can be equal.

Here is my attempt:

#eval show (TermElabM Unit) from do
  let a ← elabTerm (← `(λ (f : Nat → Nat) (x : Nat) => x * f x)) none
  let b ← elabTerm (← `(λ (f : Nat → Nat) (x : Nat) => (_ : Nat → Nat → Nat) x (f x))) none
  IO.println (← isDefEq a b)
  IO.println (← instantiateMVars b)

but it I have few questions about it:

1. How can I turn on set_option trace.Meta.isDefEq true in only for (← isDefEq a b)? If I turn on the tracing for the whole #eval command I get tons of messages I do not care about.
2. The unification does not seem to work the same as in the apply tactic. If I change a to elabTerm (← (λ (f : Nat → Nat) (x : Nat) => (x + ) * f x)) none the (← isDefEq a b) returns false. However, that corresponds to the working example with g = (· + 1)

[pcpthm]

1 is

  withOptions (·.insert `trace.Meta.isDefEq true) do
    IO.println (← isDefEq a b)

[Tomas Skrivan]

Thanks! Now the answer to 2. is that the hole translates to ?m f x instead of just ?m, that is why there is a difference.

Thus I'm doing unification fun f x => x * f x =?= fun f x => ?m f x x (f x) instead of fun f x => x * f x =?= fun f x => ?m x (f x).

The question is how do I create expression for fun f x => ?m x (f x) i.e. alternative to let b ← elabTerm (← `(λ (f : Nat → Nat) (x : Nat) => (_ : Nat → Nat → Nat) x (f x))) none

[Tomas Skrivan]

One way of creating fun f x => ?m x (f x) is:

  let mId ← mkFreshMVarId
  let m ← mkFreshExprMVarWithId mId
  let natToNat :=
  let b := mkLambda `f BinderInfo.default (mkForall Name.anonymous BinderInfo.default (mkConst ``Nat) (mkConst ``Nat)) $
           mkLambda `x BinderInfo.default (mkConst ``Nat) $
           mkApp (mkApp m (mkBVar 0)) (mkApp (mkBVar 1) (mkBVar 0))

Which is quite ugly. I guess one way to do it would be to use Gabriel's quote4 library. What is the best way without any library?