Everything is ported, except for a bisimulation tactic that is also defined in this file. I'm not really sure how to deal with that, I don't really know how to read the Lean 3 tactic code, so help would be appreciated.

Now needs help with a universe issue:

stuck at solving universe constraint
  max u ?u.141339 =?= u
while trying to unify
  (TypeVec (n + 1) → Type (max ?u.141339 u)) (n + 1) → TypeVec (n + 1) → Type (max ?u.141339 u)
with
  (TypeVec (n + 1) → Type u) (n + 1) → Type u

Now needs help with a universe issue:

stuck at solving universe constraint
  max u ?u.141339 =?= u
while trying to unify
  (TypeVec (n + 1) → Type (max ?u.141339 u)) (n + 1) → TypeVec (n + 1) → Type (max ?u.141339 u)
with
  (TypeVec (n + 1) → Type u) (n + 1) → Type u

It seems something beyond just an universe issue. It's trying to apply (TypeVec (n + 1) → Type u) to (n + 1), which doesn't really make sense?

EDIT: Yes, the universe issue is resolved by giving explicit universes, but that just reveals more issues with the proof itself.

@alexkeizer @Ruben-VandeVelde
I've ported mv_bisim tactic.
(The implementation is extortionately messy. I hope that this is fixed.)

@Komyyy Thanks for picking this up! I'll try having a look at the tactic, but I'm having a bit of trouble to parse what exactly is going on. Since you ported it, I assume you have more of a clue, so if you could write some documentation explaining what the tactic does, I would really appreciate it

@alexkeizer
I've rewritten the tactic.
The implementation is improved and become "lean" much or less.
You needn't to fixed this tactic, thank you.

What mv_bisim e with R a b x Ha Hb do:

1. generalize e = x.
2. When goal is l[x] = r[x], Define R := fun a b => ∃ x, a = l[x] ∧ b = r[x].
3. refine MvQPF.Cofix.bisim₂ R ?_ _ _ ⟨_, rfl, rfl⟩.
4. rintro a b ⟨x, Ha, Hb⟩,.
5. clear x

The tactic is fine. It's also only ever used in this file, which is a leaf anyway...

bors d+

✌️ alexkeizer can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Thanks 🎉

bors merge

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style