difficulty porting List.perm_inv_core

Stream: mathlib4

[Scott Morrison]

I need to port List.perm_inv_core from mathlib3 to mathlib4.

To do so, I have copied and pasted (and slightly cleaned up) the beginning of mathport's suggestion, adding

@[elabAsElim]
theorem perm_induction_on {P : List α → List α → Prop} {l₁ l₂ : List α} (p : l₁ ~ l₂) (h₁ : P [] [])
    (h₂ : ∀ x l₁ l₂, l₁ ~ l₂ → P l₁ l₂ → P (x :: l₁) (x :: l₂))
    (h₃ : ∀ x y l₁ l₂, l₁ ~ l₂ → P l₁ l₂ → P (y :: x :: l₁) (x :: y :: l₂))
    (h₄ : ∀ l₁ l₂ l₃, l₁ ~ l₂ → l₂ ~ l₃ → P l₁ l₂ → P l₂ l₃ → P l₁ l₃) : P l₁ l₂ :=
  have P_refl : ∀ l, P l l := fun l => List.recOn l h₁ fun x xs ih => h₂ x xs xs (Perm.refl xs) ih
  Perm.recOn p h₁ h₂ (fun x y l => h₃ x y l l (Perm.refl l) (P_refl l)) @h₄

theorem perm_inv_core {a : α} {l₁ l₂ r₁ r₂ : List α} : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂ := by
  generalize e₁ : l₁ ++ a :: r₁ = s₁
  generalize e₂ : l₂ ++ a :: r₂ = s₂
  intro p
  revert l₁ l₂ r₁ r₂ e₁ e₂
  refine' perm_induction_on p _ (fun x t₁ t₂ p IH => _) (fun x y t₁ t₂ p IH => _) (fun t₁ t₂ t₃ p₁ p₂ IH₁ IH₂ => _)
  · sorry
  · sorry
  · sorry
  · sorry

to the bottom of Mathlib/Data/List/Perm.lean in the master branch of mathlib4.

However, the refine' tactic is producing a result that I haven't been able to understand.

The goals become:

case refine'_1
α: Type u_1
a: α
s₁s₂: List α
p: s₁ ~ s₂
l₁✝l₂✝r₁✝r₂✝: List α
⊢ l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝
case refine'_2
α: Type u_1
a: α
s₁s₂: List α
p: s₁ ~ s₂
l₁✝l₂✝r₁✝r₂✝: List α
⊢ α →
  ∀ (t₁ t₂ : List α),
    t₁ ~ t₂ →
      (l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝) →
        l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝
case refine'_3
α: Type u_1
a: α
s₁s₂: List α
p: s₁ ~ s₂
l₁✝l₂✝r₁✝r₂✝: List α
⊢ α →
  α →
    ∀ (t₁ t₂ : List α),
      t₁ ~ t₂ →
        (l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝) →
          l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝
case refine'_4
α: Type u_1
a: α
s₁s₂: List α
p: s₁ ~ s₂
l₁✝l₂✝r₁✝r₂✝: List α
⊢ ∀ (t₁ t₂ t₃ : List α),
  t₁ ~ t₂ →
    t₂ ~ t₃ →
      (l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝) →
        (l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝) →
          l₁✝ ++ a :: r₁✝ = s₁ → l₂✝ ++ a :: r₂✝ = s₂ → l₁✝ ++ r₁✝ ~ l₂✝ ++ r₂✝

whereas in mathlib3 at the corresponding point they were

4 goals
α: Type uu
a: α
s₁s₂: list α
p: s₁ ~ s₂
⊢ ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = nil → l₂ ++ a :: r₂ = nil → l₁ ++ r₁ ~ l₂ ++ r₂
α: Type uu
a: α
s₁s₂: list α
p: s₁ ~ s₂
x: α
t₁: list α
t₂: list α
p: t₁ ~ t₂
IH: ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = t₁ → l₂ ++ a :: r₂ = t₂ → l₁ ++ r₁ ~ l₂ ++ r₂
⊢ ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = x :: t₁ → l₂ ++ a :: r₂ = x :: t₂ → l₁ ++ r₁ ~ l₂ ++ r₂
α: Type uu
a: α
s₁s₂: list α
p: s₁ ~ s₂
x: α
y: α
t₁: list α
t₂: list α
p: t₁ ~ t₂
IH: ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = t₁ → l₂ ++ a :: r₂ = t₂ → l₁ ++ r₁ ~ l₂ ++ r₂
⊢ ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = y :: x :: t₁ → l₂ ++ a :: r₂ = x :: y :: t₂ → l₁ ++ r₁ ~ l₂ ++ r₂
α: Type uu
a: α
s₁s₂: list α
p: s₁ ~ s₂
t₁: list α
t₂: list α
t₃: list α
p₁: t₁ ~ t₂
p₂: t₂ ~ t₃
IH₁: ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = t₁ → l₂ ++ a :: r₂ = t₂ → l₁ ++ r₁ ~ l₂ ++ r₂
IH₂: ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = t₂ → l₂ ++ a :: r₂ = t₃ → l₁ ++ r₁ ~ l₂ ++ r₂
⊢ ∀ {l₁ l₂ r₁ r₂ : list α}, l₁ ++ a :: r₁ = t₁ → l₂ ++ a :: r₂ = t₃ → l₁ ++ r₁ ~ l₂ ++ r₂

Can anyone assist me in working out how to successfully apply perm_induction_on here?

[Mario Carneiro]

It looks like implicit lambdas triggered just before the perm_induction_on application, meaning that it's actually doing refine' fun {l1 l2 r1 r2} => perm_induction_on p _ (fun x t₁ t₂ p IH => _) (fun x y t₁ t₂ p IH => _) (fun t₁ t₂ t₃ p₁ p₂ IH₁ IH₂ => _) which is not what you want

[Mario Carneiro]

You can disable implicit lambdas by using @ before perm_induction_on, although that will also make the arguments to perm_induction_on explicit; possibly@(perm_induction_on ..) does what you want (EDIT: confirmed)

[Scott Morrison]

Thanks. That solves the tombstone issue. I now see that there are two separate problems: note that the goal in the first branch is now

case refine'_1
α: Type u_1
a: α
s₁s₂: List α
p: s₁ ~ s₂
l₁l₂r₁r₂: List α
e₁: l₁ ++ a :: r₁ = s₁
e₂: l₂ ++ a :: r₂ = s₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

whereas in the mathlib3 version we have

e₁: l₁ ++ a :: r₁ = nil
e₂: l₂ ++ a :: r₂ = nil

(which is what we need to proceed!)

[Mario Carneiro]

I don't understand that goal at all, it looks like you didn't do anything

[Mario Carneiro]

what's the actual term you used?

[Mario Carneiro]

also show_term might help

[Mario Carneiro]

maybe the motive didn't abstract over s1 and s2 correctly? elabAsElim is relatively untested for mathlib problems so there could be an elaboration bug

[Scott Morrison]

show_term refine' @(perm_induction_on p _ (fun x t₁ t₂ p IH => _) (fun x y t₁ t₂ p IH => _) (fun t₁ t₂ t₃ p₁ p₂ IH₁ IH₂ => _)) prints:

𝔗𝔯𝔶 𝔱𝔥𝔦𝔰: refine
  @perm_induction_on α
    (fun x x => ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂) s₁ s₂ p
    (fun {l₁} => @?_ l₁) (fun x t₁ t₂ p IH => @?_ x t₁ t₂ p IH) (fun x y t₁ t₂ p IH => @?_ x y t₁ t₂ p IH)
    fun t₁ t₂ t₃ p₁ p₂ IH₁ IH₂ => @?_ t₁ t₂ t₃ p₁ p₂ IH₁ IH₂

[Scott Morrison]

This is pretty trivial to separate from mathlib, so I'll create a Lean4 issue, as it seems it's an elaboration bug with elabAsElim.