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.