my PRs that need help

Stream: mathlib4

[Arien Malec]

mathlib4#1464: universe issues, should be straightforward for someone who understands universe resolution issues. Mathport complains about suspect translations and proofs later fail due to universe comparison issues.
mathlib4#1216: three issues, one needs a replacement for change…with, one is a proof that's backed into a corner, last is a type resolution issue.
mathlib4#1179: one proof where the goal state is too unfolded, to fields with motives, and rws that should work don't, two generalize_proofs that are broken with unknown free variable, two proofs that also seem to be oddly unfolded, and a by tidy proof where my attempt to replicate the tidy? output gets to the same "too unfolded" state.
mathlib4#809: I think I should delete this one -- waiting on a higher_order attr, and no work lost.

[Arien Malec]

(deleted mathlib4#809)

[Kevin Buzzard]

Just about to get on the tube so thought I'd try one of these on the journey (I don't have internet underground so it's hard to switch branches). mathlib4#1464 seems to have been put on the queue and then fell off again? Bors failed for some reason? Are mathlib4#1216 and mathlib4#1179 still in the same state as above?

[Kevin Buzzard]

gaargh does lake exe cache get not work on 1179 because it's too old or something? Can this be fixed by merging master or rebasing master or whatever you're supposed to do? (note: I'll not do it, I'll just look at 1216)

[Kevin Buzzard]

1216 (data.seq.computation) I managed to fix one of the errors; I pushed. I'm not sure if I care to diagnose why things had changed; I left a porting note. One issue was that Lean 3 foo._match_1 and Lean 4 Foo.match_1 had totally different types (I mean widely different) when foo=corec.F, but mathport or you had aligned them anyway.

[Arien Malec]

Kevin Buzzard said:

Just about to get on the tube so thought I'd try one of these on the journey (I don't have internet underground so it's hard to switch branches). mathlib4#1464 seems to have been put on the queue and then fell off again? Bors failed for some reason? Are mathlib4#1216 and mathlib4#1179 still in the same state as above?

There was a build failure due to failure to get cache, and I rebuilt, but realized I needed to kick bors again

[Arien Malec]

Kevin Buzzard said:

1216 (data.seq.computation) I managed to fix one of the errors; I pushed. I'm not sure if I care to diagnose why things had changed; I left a porting note. One issue was that Lean 3 foo._match_1 and Lean 4 Foo.match_1 had totally different types (I mean widely different) when foo=corec.F, but mathport or you had aligned them anyway.

_match_1 just isn't a thing in Lean 4; I switched to .match_1 so I could see what the issues are, but my conclusion was that the whole thing needed to be redone...

[Arien Malec]

OK, I fixed one more issue (intros in Lean 3 behaves differently in Lean 4 and requires careful comparison in both sides to get everything right).

Down to a single issue....

[Arien Malec]

I truly don't understand the last issue -- all the types line up, there must be some autoimplicit issues, but none of the tricks I know work....

[Kevin Buzzard]

Higher unification is failing in Lean 4 when it worked in Lean 3 -- this seems to be a general regression where unification doesn't work as well in Lean 4. I'm working on a fix.

[Kevin Buzzard]

Pushed! mathlib4#1216 now compiles.

[Kevin Buzzard]

I'm building mathlib4#1179 from scratch just like the old days. Does someone who knows the difference between merge and rebase and knows which one is the right one to do, want to merge/rebase master onto that branch, namely feat-port-data.pfun?

[Arien Malec]

Down to two lints, one [both?] of which is/are incorrect:

In LiftRelRec.lem the linter complains that in have h := h HC, but h is reverted then intro'd. Seems like a linter bug, but how do I tell the linter to ignore this?

In lift_rel_pure the linter wants to use lift_rel_pure_right to simplify the rhs of the lemma, but I think the very point of the lemma is to express a core invariance of LiftRel and lift_rel_pure_right is a means to an end here.

[Arien Malec]

& now that I think about it, it should probably be liftRel_pure :-)

[Arien Malec]

Arien Malec said:

In LiftRelRec.lem the linter complains that in have h := h HC, but h is reverted then intro'd. Seems like a linter bug, but how do I tell the linter to ignore this?

The linter was right, actually.

[Arien Malec]

Arien Malec said:

In lift_rel_pure the linter wants to use lift_rel_pure_right to simplify the rhs of the lemma, but I think the very point of the lemma is to express a core invariance of LiftRel and lift_rel_pure_right is a means to an end here.

nolint'd to push to review.

[Kevin Buzzard]

For mathlib4#1179 it might be the case that the reason you had to add noncomputable in the def of fix on line 255 (something to do with WellFounded not reducing? I don't really understand this stuff) is the same reason why the proof of mem_fix_iff 15 lines later doesn't work. The chaos starts right on the first line let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h --the lean 4 h_2 has several Eq.ndrec's in which aren't present in Lean 3. I can't figure this one out.

[Kevin Buzzard]

It would be great if someone could make this PR work with caching without messing up the git history but I don't know how to do that either.

[Arien Malec]

It does now...

[Arien Malec]

@Ruben Van de Velde did the git magic.

[Kevin Buzzard]

Thanks! The issue is that simp [e] at h₃ no longer succeeds; the motive is not type correct in mathlib4 presumably because everything is so much more complicated than the corresponding mathlib3 term.

[Arien Malec]

This is probably the same issue that's borking fixInduction'_stop and fixInduction'_fwd