Data.List.Perm mathlib4#1478

Stream: mathlib4

[James Gallicchio]

I can get it compiling with a manual rec. Weird.

[James Gallicchio]

anyone who knows how congr lemmas work: Perm.filter_map and Perm.map were marked @[congr] in mathlib3 but mathlib4 does not like it. thoughts?

[James Gallicchio]

@[congr]
theorem Perm.filter_map (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    filterMap f l₁ ~ filterMap f l₂ :=
/-
invalid 'congr' theorem, equality expected
  filterMap ?f ?l₁ ~ filterMap ?f ?l₂
-/

[James Gallicchio]

Evidently equivalence relations that aren't equalities are not yet supported.

[Mario Carneiro]

yes, support for congruence with relations other than equality was never that great and they are not a part of simp/congr in lean 4. I don't think they really did anything in lean 3 either, so you can just comment it out (with a porting note).

[James Gallicchio]

Okay, after way too long playing around with it, I figured out what went wrong with perm_inv_core translation

in lean3 if your goal is ∀ {l₁ l₂ r₁ r₂ : list α}, ... and you refine with an elaborator, the motive includes the implicits. but in lean4 doing the same introduces the implicits before generating the motive

[James Gallicchio]

I fixed it by just making the implicit parameters explicit before refining, but is there a better way to change the elaboration behavior?

[James Gallicchio]

(and can we do it automatically..? not sure how frequently we're refining by an elaborator though)

[James Gallicchio]

okay, my brain is tired :zzz: feel free to pick it up while I am asleep; otherwise I'll continue in 8hr or so

[Johan Commelin]

sleep tight!

[Johan Commelin]

What's the lean 4 equiv of

attribute [protected] subperm.cons

[Mario Carneiro]

there is no @[protected] attribute, but you can put protected on structure fields and inductive constructors

[Eric Wieser]

What's the syntax for that?

[James Gallicchio]

Huge progress :D thanks Johan!

[James Gallicchio]

oh wait, Johan and Chris! :big_smile:

[Johan Commelin]

I've kicked it on the queue

[Chris Hughes]

(deleted)

[James Gallicchio]

awesome. I'm now looking into moving stuff from here to Std -- once a file is ported, is it open to PRs that don't align with mathlib3?

[Johan Commelin]

if it moves to Std, and you leave the #aligns in place