Zulip Chat Archive

Stream: std4

Topic: List.Perm in Std

James Gallicchio (Jan 19 2023 at 08:43):

Pushed a draft PR with a half-compiling version of Perm in Std. De-mathlib'ing the file is very time consuming...

I've dropped all lemmas involving Associative/Commutative, Mathlib.Data.List.Lattice lemmas, permutations, and a couple other smaller things

James Gallicchio (Jan 19 2023 at 09:40):

Okay, stopping for now. I think I'm a majority of the way to the lemmas that are sorry in https://github.com/leanprover/std4/pull/38 !

James Gallicchio (Jan 21 2023 at 13:23):

Hm... I'm starting to wonder if maybe we should move some of the Mathlib.Init.Logic definitions to Std, in particular Symmetric, Transitive, Reflexive, Associative, Commutative. I can just expand the definitions in place, but .. I dunno ..

Wojciech Nawrocki (Jan 21 2023 at 17:11):

This is likely a good idea, especially if the Associative/Commutative classes are used by automation like ac_refl (currently it uses Lean.IsCommutative, Lean.IsAssociative).

James Gallicchio (Jan 21 2023 at 17:44):

I'm also having to move List.mem_map' to Std. This is the same as mem_map except the equality is flipped:

theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ b = f a
  | [] => by simp
  | b :: l => by
    simp only [map, mem_cons, mem_map (l := l), or_and_right, exists_or, exists_eq_left]

@[simp]
theorem mem_map' {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
  := by simp only [mem_map, eq_comm, implies_true]

I'm not sure why the divergence happened in the first place. Weirdly mem_map' doesn't prove with the same proof as mem_map due to the order of equality in mem_cons.

James Gallicchio (Jan 21 2023 at 17:45):

mem_map' in mathlib is marked with -- Porting TODO: fix `List.mem_map` in Std to this statement. so perhaps this is good :)

James Gallicchio (Jan 22 2023 at 18:51):

A first pass of Perm compiles. I removed so many lemmas that I'm not sure I'll be able to close out sorries in std#38 but I'd like to rebase it to actually see what else we need. thoughts on the best way to do that?

James Gallicchio (Jan 22 2023 at 20:34):

Ok, learned lots about git remotes and attempted a rebase, but there were a few conflicts that require actual thought. Probably won't get around to it until tomorrow.

Wojciech Nawrocki (Jan 23 2023 at 00:17):

Even if you don't manage to close all the sorries I would still encourage you to push what you have! With incremental progress we'll get there eventually.

James Gallicchio (Jan 23 2023 at 01:30):

(deleted)

James Gallicchio (Jan 23 2023 at 08:08):

I'm starting to wonder if I should also be reorganizing stuff in this PR, because I'm not sure I entirely understand how all these lemmas were organized in mathlib. Like, should I move Pairwise to the pairwise file? and Forall2 to the forall2 file? it makes way more sense to me to be there than Basic.

James Gallicchio (Jan 23 2023 at 08:09):

but I think I will stick to the simple translation for now, and we can clean it up in a future PR.

James Gallicchio (Jan 26 2023 at 22:11):

This is ready for an initial review: https://github.com/leanprover/std4/pull/89

Mario Carneiro (Jan 26 2023 at 22:14):

Can it be split into one PR per file? These files are pretty big

Mario Carneiro (Jan 26 2023 at 22:15):

you should remove the This file was ported from Lean 3 source module ... headers

James Gallicchio (Jan 26 2023 at 22:21):

Will do... I know this is a nightmare to review.

James Gallicchio (Jan 26 2023 at 23:11):

Good news, looks like this does cover enough of List.Perm to close all the sorries in std4#38 :D (just did the first couple sorries, the others look doable)

James Gallicchio (Jan 26 2023 at 23:11):

I'll try to clean this up tonight so we can get it merged soon.

Mario Carneiro (Jan 26 2023 at 23:12):

ok, let me know when I can review it without the nightmares :wink:

Last updated: Dec 20 2023 at 11:08 UTC