GroupTheory.FreeGroup mathlib4#1867

Stream: mathlib4

[Joachim Breitner]

I’m inclined to get myself lost in leany stuff for a two or three hours now. I hope that’s still useful when starting from scratch.
Looking at https://leanprover-community.github.io/mathlib-port-status/ group_theory.free_group might be useful, given that it’s math I am familiar with.
I guess I’ll follow https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki until I am lost or stuck, and then whine here?

[Joachim Breitner]

Should I create the PR in a fork, or ask for permissions to push to the mathlib4 repo?

[Jireh Loreaux]

Ask for permission.

[Shreyas Srinivas]

Joachim Breitner said:

Should I create the PR in a fork, or ask for permissions to push to the mathlib4 repo?

@maintainers

[Joachim Breitner]

I’ll add that step to https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki
(Once I have permissions :-))

[Mario Carneiro]

don't forget to include your github name in permission requests

[Shreyas Srinivas]

Also, to avoid the pit I fell into, I suggest opening a thread here titled `<module> mathlib4#<Pull request no>``

[Joachim Breitner]

nomeata is my handle, dear @maintainers

[Johan Commelin]

Voila, fellow Freiburger: https://github.com/leanprover-community/mathlib4/invitations

[Arien Malec]

It needs to_additive.map_namespaces or the equivalent -- does this exist?

[Joachim Breitner]

That’s what I just stumbled over…
But I think I can do without if I just tell to_additive about this naming convention.

[Arien Malec]

It looks like you can just do
@[to_additive freeAddGroup.Red.Step] etc.

[Johan Commelin]

@Joachim Breitner I'm not sure if these are mentioned already in the wiki, but there are some useful scripts:

• start_port.sh to start the port
• fix-lints.py to auto fix warnings about unused variables or unnecessary <;>
• fix-comments.py to update names mentioned in comments.

[Arien Malec]

Johan Commelin said:

Joachim Breitner I'm not sure if these are mentioned already in the wiki, but there are some useful scripts:

• start_port.sh to start the port
• fix-lints.py to auto fix warnings about unused variables or unnecessary <;>
• fix-comments.py to update names mentioned in comments.

start_port.sh and fix-lints.py were already mentioned, but I added reference to fix-comments.py

[Floris van Doorn]

Arien Malec said:

It needs to_additive.map_namespaces or the equivalent -- does this exist?

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20to_additive.2Emap_namespace
It is waiting for an open PR to do this properly, but you can just do something like @[to_additive freeAddGroup.Red.Step] manually

[Joachim Breitner]

Ok, the first 1100 lines are compiling. Now hitting

code generator does not support recursor 'List.recOn' yet, consider using 'match ... with' and/or structural recursion

but it’s gotten late, so I’ll stop now and go to bed. The PR is free for anyone to take over .

[Joachim Breitner]

Ok, I was able to fix that one :-)

[Joachim Breitner]

There is a big block

/- failed to parenthesize: parenthesize: uncaught backtrack exception
[PrettyPrinter.parenthesize.input] (Command.declaration
…

I guess mathport failed? I hope it was not stupid to not check for that before hand-editing everything above.

[Mario Carneiro]

that's a bug (mathport produced invalid syntax), usually caused by a change to mathlib4 tactic syntax

[Mario Carneiro]

link?

[Mario Carneiro]

it's not an error that would have affected anything before or after, but the affected declaration itself is probably a lost cause when you get this error

[Joachim Breitner]

https://github.com/leanprover-community/mathlib4/pull/1867

[Joachim Breitner]

Now I’m off to bed for good :-)

[Joachim Breitner]

I think this is the only input missing

@[to_additive]
theorem reduce.not {p : Prop} :
  ∀ {L₁ L₂ L₃ : list (α × bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, bnot b) :: L₃ → p
| [] L2 L3 _ _ := λ h, by cases L2; injections
| ((x,b)::L1) L2 L3 x' b' := begin
  dsimp,
  cases r : reduce L1,
  { dsimp, intro h,
    have := congr_arg list.length h,
    simp [-add_comm] at this,
    exact absurd this dec_trivial },
  cases hd with y c,
  dsimp only,
  split_ifs with h; intro H,
  { rw H at r,
    exact @reduce.not L1 ((y,c)::L2) L3 x' b' r },
  rcases L2 with _|⟨a, L2⟩,
  { injections, subst_vars,
    simp at h, cc },
  { refine @reduce.not L1 L2 L3 x' b' _,
    injection H with _ H,
    rw [r, H], refl }
end

so not too bad

[Mario Carneiro]

the mathport bug is fixed, so it should be updated in a few hours

[Arien Malec]

I manually formatted this (but no harm just replacing whatever mathport produces), and fixed a bunch of the other issues.

reduce.not has some typing issues I don't have the brainpower rn to track down, & then there's a single decidable typing issue.

[Arien Malec]

plus the usual lints and docu fixes

[Joachim Breitner]

Compiles now, and line lengths and docu fixed.

[Siddhartha Gadgil]

I was looking at FreeGroup.lean to use in some lectures and was struck by some unusual choices. For instance, I see

theorem reduce.not {p : Prop}: ∀ {L₁ L₂ L₃: List (α × Bool)} {x : α} {b},
  ((reduce L₁) = L₂ ++ ((x,b)::(x ,!b)::L₃)) → p

I would have expected False in place of p, i.e.,

theorem reduce.not: ∀ {L₁ L₂ L₃: List (α × Bool)} {x : α} {b},
  ((reduce L₁) = L₂ ++ ((x,b)::(x ,!b)::L₃)) → False

is was also unusual to see reduce defined directly in terms of List.rec instead of pattern matching.

Should clarify that this is very nice and useful to me. I am not complaining, just commenting on something that seems unusual.

@Kenny Lau I believe you wrote/ported this.