using mathlib3port

Stream: mathlib4

[Scott Morrison]

When I made the minimal port of Fintype using the mathport output contained in mathlib3port, I also wrote some notes about what I needed to change to get mathport output working again.

@Mario Carneiro, do you think you might have time to go through these with me? I'd like to know how you think these changes should split up amongst:

• we should fix mathport to handle this!
• we could maybe manyana have mathport handle this
• we should add stuff in mathlib4 to make this smoother
• humans doing the porting are just going to have to cope

I wrote my changes down here. If there's a time we could chat in real-time that would be great, but we can also do it here if that's more efficient.

Hopefully we can create some issues/PRs/documentation for porters to make these things easier in future.

[Scott Morrison]

Quick summary of what I learnt from Mario, for anyone following along:

• There is lots of sadness about how mathport sometimes camelCases successfully, and sometimes_does_not. It's hard, and will take some work.
• The definition of List membership has changed from Lean3 to Lean4, so rcases on list membership hypotheses will all have to be written (and similarly in analogous cases). This would probably be a pain to have mathport handle automatically.
• Simp's behaviour with multiple binders has changed, making some simp lemmas which want to see some but not all of the binders in an expression not fire anymore. I'll make an issue somewhere about this, whether it's fixable or just for the sake of documenting the change.
• example : Nat → Nat := by refine' (fun x => _) produces the goal ⊢ Nat → Nat, rather than x : Nat ⊢ Nat as you might expect. With fun x => ?_ we get the expected behaviour. This is not necessarily incorrect, but confusing when porting. Again, I'll make an issue somewhere.

[Ruben Van de Velde]

Scott Morrison said:

• The definition of List membership has changed from Lean3 to Lean4, so rcases on list membership hypotheses will all have to be written (and similarly in analogous cases). This would probably be a pain to have mathport handle automatically.

Is this backportable? Not sure how big a deal the manual porting would be

[David Renshaw]

re the mem_split proof

• I couldn't get rcases h with (rfl | h), or any variant, to work.
  Using rfl generates an error, but replacing it with _ gives the desired behaviour.
  I couldn't get rcases to introduce a new hypothesis named h in the 2nd branch.

This works (but is arguably no better than what you wrote):

theorem mem_split {a : α} {l : List α} (h : a ∈ l) : ∃ s t : List α, l = s ++ a :: t := by
  induction l with
  | nil => cases h
  | cons b l ih =>
    rcases h with _ | ⟨_, _, _, h⟩
    · exact ⟨[], l, rfl⟩
    · rcases ih h with ⟨s, t, rfl⟩
      exact ⟨b :: s, t, rfl⟩

[David Renshaw]

I don't understand why we need 3 underscores in ⟨_, _, _, h⟩ here. Looking at the definition of List.Mem, I would expect to only need one, for the parameter (a : α). The other parameters of tail have curly braces, so should be implicit, right?

[David Renshaw]

For what it's worth, the behavior is the same in Lean 3 (with a backported version of Lean 4's List.Mem):

inductive list_mem' {α : Type} : α → list α → Prop
| head (a : α) (as : list α) : list_mem' a (a::as)
| tail (a : α) {b : α} {as : list α} : list_mem' b as → list_mem' b (a::as)

example {α : Type} (a b : α) (as : list α) (h : list_mem' a  (b :: as)) :
   (a = b ∨ list_mem' a as) :=
begin
  rcases h with _ | ⟨_, _, _, h'⟩,
  { exact or.inl rfl },
  { exact or.inr h' },
end

[Scott Morrison]

It looks like Mario is changing the behaviour of rcases in a way that will make less of a problem.