Assigning metavariables by unification

Stream: lean4

[Eric Rodriguez]

This came from a discussion in the Xena server; is there any hope for code such as the below working? Some variation of this used to work in Lean3, iirc:

def my_complicated_goal : Nat → Prop := sorry
def simpler_goal : Nat → Prop := sorry
theorem my_lemma : ∀ k, my_complicated_goal k ↔ simpler_goal k := sorry

example : ∃ x, my_complicated_goal x := by
  have lem : ∃ t : Nat, ?_ := ?_
  cases lem with
  | intro t h =>
    refine ⟨t, ?_⟩
    rw [my_lemma]
    exact h -- type mismatch...

  exact simpler_goal t -- should be forced by the `exact h`
  sorry

[Scott Morrison]

Yes, that is sad. At first I thought replacing the have with a let would help, but I can't get it to work.

[Kyle Miller]

This seems to be a workaround:

example : ∃ x, my_complicated_goal x := by
  have lem : ∃ t : Nat, (?a : Nat → Prop) t := ?b
  cases lem with
  | intro t h =>
    refine ⟨t, ?c⟩
    rw [my_lemma]
    exact h
  done
  /-
  case b:
  ⊢ ∃ t, (fun t ↦ simpler_goal t) t
  -/

[Kyle Miller]

It's got something to do with delayed assignment metavariables, but I don't know what the issue is exactly. If you have just ∃ t : Nat, ?a, you'll notice you just have h : ?m.45 t, where (I didn't check this but I have a good guess that) ?m.45 is registered as a delayed assignment, where it will be assigned once ?a is. If ?a could be a natural metavariable, then the exact h might go through.

[Kyle Miller]

I'm not sure to what extent isDefEq can handle assigning to delayed assignment metavariables with withAssignableSyntheticOpaque on. Maybe there's a way to get ?m.45 t =?= simple_goal t to see that it's OK to solve ?a =?= simple_goal t. Though a problem with delayed assignment metavariables is that instantiateMVars doesn't do anything with them until the metavariable associated to them is completely assigned, with no metavariables remaining.

[Kyle Miller]

In particular, you can't reduce ?m.45 t =?= e to ?a =?= e unless e has no metavariables, if I'm understanding this all correctly.

[Kyle Miller]

(My workaround is simulating how natural metavariables get abstracted.)

[Kyle Miller]

Hmm, docs#Lean.Meta.expandDelayedAssigned? suggests that it does try to solve ?m.45 t =?= e by reducing it to ?a =?= e

[Kyle Miller]

Oh, but then the t in simpler_goal t is not the same fvar as the t in the local context for ?a, so defeq fails.

[Kyle Miller]

There's a comment in that function explaining a possible improvement to the algorithm that should help here.

[Patrick Massot]

Recall that, for people who are not Kyle and look for an interesting and useful meta-programming challenge, we need to port coq-procrastination.

[Yaël Dillies]

cc @Anand Rao Tadipatri, @Jovan Gerbscheid, @Mantas Baksys who worked with handling metavariables this summer to implement something pretty similar to this

[Jovan Gerbscheid]

The particular example is easy to do with the targeted rewrite that we have, which is able to rewrite under binders.