higher order unification failure

Stream: lean4

[Kevin Buzzard]

In Lean 3 this worked:

example (α β : Type) (a a' : α) (b : β) (rβ : β → β → Prop) (f : α → β) (he: f a' = b)
  (h : rβ b (f a)) : rβ (f a') (f a) :=
he.substr h

In Lean 4 I seem to need to tell Lean the motive:

example (α β : Type) (a a' : α) (b : β) (rβ : β → β → Prop) (f : α → β) (he: f a' = b)
  (h : rβ b (f a)) : rβ (f a') (f a) :=
--he.substr h -- higher unification gets confused
he.substr (p := λ x => rβ x (f a)) h -- tell it the motive and it's fine

I know this is higher order unification and one can't expect miracles, this post is mainly to check that behaviour like this is expected (e.g. the unification algorithm has changed). This came up when porting logic.relation.

[Gabriel Ebner]

https://github.com/leanprover/lean4/issues/1806

[Kevin Buzzard]

@David Renshaw are you also porting logic.relation? I don't want to duplicate work. I had claimed it on the wiki but you're welcome to have it (I had got up to line 190). I am on a long train journey from Bonn to London starting in 8 hours and it would be great to know whether I should start on another file.

[David Renshaw]

I started on it, but then saw that we need the mk_iffattribute. So I'm working on mk_iff now.

[David Renshaw]

(Status of mk_iff is that currently I can generate the correct theorems, but their proofs are sorried.)

[Kevin Buzzard]

Yeah, I'd just got to that point. I decided that I would just make the iffs manually :-)

[Kevin Buzzard]

So do you want to keep going on mk_iff and I'll spend the train journey tomorrow doing the rest of logic.relation? Are you much further ahead than me? Or shall I just get out of your hair, change the wiki to you, and do another file?

[David Renshaw]

You're probably exactly where I got to, and I don't intend to continue in the immediate future.

[Kevin Buzzard]

OK great, I'll keep going. I am exactly at the first mk_iff. I won't make the iff! (I might add that I am in no position to make attributes but can just about port mathlib files)

[David Renshaw]

In case you want to test out the attribute:
https://github.com/leanprover-community/mathlib4/pull/561.
It should work, but the proofs are sorried and there are still a bunch of verbose dbg_trace statements.

[David Renshaw]

I think I have a complete implementation of mk_iffnow: https://github.com/leanprover-community/mathlib4/pull/561

[Kevin Buzzard]

Thanks! I'll try and find the time tomorrow to put everything together but it's my first day back at work after a week of travelling so who knows.

[Kevin Buzzard]

I should say that I have a branch with logic.relation ported apart from the last few lemmas