Question about unification

Stream: general

[Frédéric Tran Minh]

Hi everyone, First, I'm sorry if I do not post at the right place. Here is the question, hope it's not too stupid.
The general context is that I'm trying to generate a definition from a proposition.
Let's consider the following code :

def drec (f : Nat → Nat → Nat)  : Nat → Nat
  | 0   => 0
  | n+1 => f n (drec f n)

theorem t (f : Nat → Nat → Nat)  : ∃ g : Nat → Nat,  ∀ n :Nat, g (n+1) = f n (g n)
       :=  ⟨drec f,by intro n ;  rfl⟩

noncomputable  def u_sub1 :=
   Classical.indefiniteDescription _ (t _ : ∃ u:Nat → Nat , ∀ n:Nat,  u (n+1) = n + u n)
noncomputable  def u_sub2 :=
   Classical.indefiniteDescription _ (t _ : ∃ u:Nat → Nat , ∀ n:Nat,  u (n+1) = (fun m x => m+x)  n (u n))

def g1 :  Nat → Nat → Nat := fun m x => x+m
def g2 :  Nat → Nat → Nat := fun m x => m+x
noncomputable  def u_sub3 :=
   Classical.indefiniteDescription _ (t _ : ∃ u:Nat → Nat , ∀ n:Nat,  u (n+1) = g1 n (u n))
noncomputable  def u_sub4 :=
   Classical.indefiniteDescription _ (t _ : ∃ u:Nat → Nat , ∀ n:Nat,  u (n+1) = g2 n (u n))


--noncomputable  def u_sub5 :=
--   Classical.indefiniteDescription _ (t _ : ∃ u:Nat → Nat , ∀ n:Nat,  u (n+1) = u n + n)
    -- does not typecheck

--noncomputable  def u_sub6:=
--   Classical.indefiniteDescription _ (t _ : ∃ u:Nat → Nat , ∀ n:Nat,  u (n+1) = (fun m x => x+m)  n (u n))
      -- does not typecheck

u_sub1, u_sub2, u_sub3, u_sub4 typecheck but u_sub5 and u_sub6 don't.

Why ??

The error message is :

type mismatch
  t ?m.580
has type
  ∃ g, ∀ (n : Nat), g (n + 1) = ?m.580 n (g n) : Prop
but is expected to have type
  ∃ u, ∀ (n : Nat), u (n + 1) = u n + n : Prop

I'm using Lean v4.15.0

Thanks in advance !

[Kyle Miller]

Here's what I've figured so far. The higher-order unification is able to succeed here in a special case (for reasons I don't quite understand). In the following, I'm using refine rfl to make it be possible to assign to ?f1 even though it's a synthetic opaque metavariable.

example (u : Nat → Nat) (n : Nat) : True := by
  have : n + u n = (?f1 : Nat → Nat → Nat) n (u n) := by refine rfl -- succeeds
  let f1 := ?f1
  -- f1 : Nat → Nat → Nat := HAdd.hAdd
  have : u n + n = (?f2 : Nat → Nat → Nat) n (u n) := by refine rfl -- fails

Basically, n + u n is notation for HAdd.hAdd n (u n). Unifying against ?f1 n (u n) is allowed to succeed here. I'm not sure the rule, but at least we have two expressions with the same arguments, so assigning ?f1 to the function makes some sense.

In the second case, ?f1 (u n) n doesn't have the same argument order, so that doesn't work anymore.

[Frédéric Tran Minh]

Thanks a lot for your clear answer, and for minimizing the example. I did not know this possibility of working directly with metavariables. A lesson for me : higher order unification is far from straighforward. That's probably why there is a 'triangle' macro on top of Eq.subst to help unifiying the motive.
Your analysis is consistent with the fact that :

axiom f : Nat → Nat → Nat
example ( a b : Nat) : True := by
  have : f a b = (_ : Nat → Nat → Nat) a b := rfl -- succeeds
--  have : f b a = (_ : Nat → Nat → Nat) a b := rfl -- fails
  trivial

This suggests that when trying to unify (f b a) with (?f1 a b) isDefEq (itself?) seems to first succeed in unifying f with ?f1 and then fail while recursing into arguments. (it does not try to abstract parameters and rebuild a function).