[Merged by Bors] - feat(combinatorics/simple_graph/connectivity): Transfer walks from a simple_graph to another

[bottine]

---

[kmill]

These are some style comments mostly so far.

Regarding the private lemmas, for very short ones that don't have any other uses, a have block inside a proof is fine. Otherwise, it'd be best to have non-private lemmas.

[bottine]

Maybe this should be protected ?

[kmill]

Here are the tradeoffs as I see them:

If it's protected,

• then we never have to worry about it conflicting with anything else named transfer
• while you need to refer to walk.transfer, you likely would write p.transfer H prf anyway

If it's not protected,

• then we do have to worry about it conflicting with something named transfer, but this is not a common name.
• then we can just write transfer p H prf

I'll leave it to you!

[kmill]

Here are some more comments. There shouldn't be too many more rounds of this -- I think the general structure looks good. The next pass will likely be more careful consideration of names and the exact type signatures of lemmas (i.e., deciding whether variables should be implicit or not).

[kmill]

Here are the tradeoffs as I see them:

If it's protected,

• then we never have to worry about it conflicting with anything else named transfer
• while you need to refer to walk.transfer, you likely would write p.transfer H prf anyway

If it's not protected,

• then we do have to worry about it conflicting with something named transfer, but this is not a common name.
• then we can just write transfer p H prf

I'll leave it to you!

[kmill]

Here's a shorter way to write this case. I prefer it because it doesn't use tactic mode for the definition, but that's not a strict mathlib rule.

Suggested change

	| _ _ (walk.cons a p) H h := by
	{ refine walk.cons _ (p.transfer H _);
	simp only [walk.edges_cons, list.mem_cons_iff, forall_eq_or_imp, mem_edge_set] at h,
	exact h.1, exact h.2, }
	| _ _ (walk.cons' u v w a p) H h :=
	walk.cons (h ⟦(u, v)⟧ (by simp)) (p.transfer H (λ e he, h e (by simp [he])))

[kmill]

Thanks for putting these into mathlib style. Now that you've done it, let me ask you to possibly change them again 😉

I noticed that this and many other proofs can be replaced by

Suggested change

	begin
	induction p,
	{ simp only [transfer] },
	{ simp only [p_ih, transfer, eq_self_iff_true, heq_iff_eq, and_self] },
	end
	by induction p; simp [*]

Sometimes you might need additional simp lemmas, but you can switch that simp to simp [*, extra_lemma].

[bottine]

The previous style was actually a remnant of one-line simp heavy proofs as you're using, but I thought I'd rather have simp only. I'll revert the changes

[kmill]

You can still do a simp only if you want. You can do squeeze_scope { induction p; squeeze_simp [*] } to get the simp lemmas you need, but you might need to manually dedup the simp list.

[kmill]

One way to think of these induction p; simp [*] proofs is that they strongly indicate "the proof is trivial." For these types of proofs, I usually only squeeze my simps if either (1) there's a small list of simp lemmas and knowing them is informative or (2) the simp takes longer than a second, since mathlib compilation time is important.

[bottine]

Regarding shortening the proofs again: a few of them are kind of just between one-line and begin-end ones: I tried to have something shortish enough. Hope it's OK

[kmill]

This might be the last round, unless I missed something.

Thanks for creating this PR!

[kmill]

I suggest deleting this definition since it's the "easy" mapping direction and it's already covered by p.map (simple_graph.hom.map_spanning_subgraphs GH).

Maybe at some point having an p.map_le GH abbreviation would be good.

[kmill]

I think this should be a lemma about map since again it's in the "easy" mapping direction. You'd still get to use this result via transfer_eq_map_of_le.

[bottine]

I haven't gotten rid of induce_le yet, essentially because it seems less "overkill" than p.map (simple_graph.hom.map_spanning_subgraphs GH) (and it's much shorter to type!), but also: if I'm to get rid of it, where would you put this is_cycle_transfer_le, restated in terms of map_spanning_subgraphs GH ?
If keeping induce_le is negotiable, I'd keep it, otherwise would welcome a proposal for where to fit this lemma (I actually use it in the tree stuff, hence it appearing here -- btw, I should probably also add the is_path version).
Would just leaving it here work, even if it (superficially at least) is not related to induce ?

[kmill]

Rather than induce_le, I'd like to have

/-- The specialization of `simple_graph.walk.map` for mapping walks to supergraphs. -/
@[reducible] def map_le {G G' : simple_graph V} (h : G ≤ G')
  {u v : V} (p : G.walk u v) : G'.walk u v :=
p.map (hom.map_spanning_subgraphs h)

which can go right after the definition of map. I think we should prefer map whenever possible.

By the way, a more general statement of this cycle transfer lemma would be an analogue of map_is_path_of_injective for cycles. (And also that means you don't need to add an is_path version.)

[bottine]

OK, then I'll just remove induce_le, and I think map_le and map_is_path_of_injective probably belong to another PR?

[kmill]

It probably would have been fine to slip in map_le into this PR, but creating a followup PR is fine too, so now that you've removed it let's do that.

[bottine]

OK, working on it

[bottine]

Bah, probably not done with it this week-end. I figured the easiest way for map_is_cycle_of_injective and friends would be to have a lemma p.is_cycle <-> p.length ≥ 3 /\ p.support.nodup but then I also figured the lemma is_path_def : p.is_path <-> p.support.nodup should also be used to prove map_is_path_of_injective and friends, because it would simplify the proofs, but I think for that to work I'd need l.nodup <-> l.length = l.to_finset.card, which seemingly isn't there?

[kmill]

They still need refinement (and might have unnecessary steps!), but here's what I came up with:

lemma map_is_trail_of_injective (hinj : function.injective f) (hp : p.is_trail) :
  (p.map f).is_trail :=
begin
  rw is_trail_def at hp ⊢,
  induction p with w u v w huv hvw ih,
  { simp, },
  { simp at hp,
    specialize ih hp.2,
    rw [map_cons, edges_cons, list.nodup_cons],
    split,
    { rw [edges_map],
      change sym2.map f ⟦(u, v)⟧ ∉ _,
      rw list.mem_map_of_injective (sym2.map.injective hinj),
      exact hp.1, },
    { exact ih, }, },
end

@[simp] lemma map_eq_nil_iff {p : G.walk u u} : p.map f = nil ↔ p = nil :=
begin
  split,
  { intro h,
    cases p,
    { refl },
    { injection h } },
  { rintro rfl,
    refl, }
end

lemma map_is_cycle_of_injective {p : G.walk u u} (hinj : function.injective f) (hp : p.is_cycle) :
  (p.map f).is_cycle :=
begin
  rw is_cycle_def at hp ⊢,
  simp [map_is_trail_of_injective hinj hp.1],
  split,
  { intro h,
    apply hp.2.1 h, },
  { replace hp := hp.2.2,
    rwa [← list.map_tail, list.nodup_map_iff hinj], }
end

[kmill]

Thanks for your work on this.

After improving the docstring (just reading the docstring, it's hard to tell what the function is about) and possibly changing a refine to an exact, and then making sure CI passes, feel free to merge!

bors d+

[bors]

✌️ bottine can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kmill]

Thanks!

bors r+

[bors]

Build failed (retrying...):

• Run tests

[bors]

Build failed (retrying...):

• Lint mathlib

[bottine]

What's that bors failing? The errors have nothing to do with this PR afaiu, so I assume the PR itself is not at fault?

[YaelDillies]

Yes, it's why bors says "retrying..." 😉

[kmill]

To add a bit to this, there were 7 PRs in the last bors batch. Since there are so many PRs for mathlib, and each CI run takes hours, we merge multiple PRs using bors and commit them simultaneously. Sometimes things don't merge cleanly and there are errors. Bors will automatically start to solve for which PR is the one that could be said to be the cause of an error by breaking a batch into smaller sub-batches and retrying.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests