From 2861d4eba613217496c95cc55ce9e28dba1ba12c Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 31 Mar 2022 15:26:34 +0000 Subject: [PATCH] feat(combinatorics/simple_graph/connectivity): walk constructor patterns with explicit vertices (#13078) This saves a couple underscores, letting you write `walk.cons' _ v _ h p` instead of `@walk.cons _ _ _ v _ h p` when you want that middle vertex in a pattern. --- src/combinatorics/simple_graph/connectivity.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/combinatorics/simple_graph/connectivity.lean b/src/combinatorics/simple_graph/connectivity.lean index 9db4fa2c809bf..3ddc887fd620d 100644 --- a/src/combinatorics/simple_graph/connectivity.lean +++ b/src/combinatorics/simple_graph/connectivity.lean @@ -32,7 +32,8 @@ counterparts in [Chou1994]. ## Main definitions -* `simple_graph.walk` +* `simple_graph.walk` (with accompanying pattern definitions + `simple_graph.walk.nil'` and `simple_graph.walk.cons'`) * `simple_graph.walk.is_trail`, `simple_graph.walk.is_path`, and `simple_graph.walk.is_cycle`. @@ -62,7 +63,10 @@ variables {V : Type u} (G : simple_graph V) the type `walk u v` consists of all walks starting at `u` and ending at `v`. We say that a walk *visits* the vertices it contains. The set of vertices a -walk visits is `simple_graph.walk.support`. -/ +walk visits is `simple_graph.walk.support`. + +See `simple_graph.walk.nil'` and `simple_graph.walk.cons'` for patterns that +can be useful in definitions since they make the vertices explicit. -/ @[derive decidable_eq] inductive walk : V → V → Type u | nil {u : V} : walk u u @@ -75,6 +79,13 @@ instance walk.inhabited (v : V) : inhabited (G.walk v v) := ⟨by refl⟩ namespace walk variables {G} +/-- Pattern to get `walk.nil` with the vertex as an explicit argument. -/ +@[pattern] abbreviation nil' (u : V) : G.walk u u := walk.nil + +/-- Pattern to get `walk.cons` with the vertices as explicit arguments. -/ +@[pattern] abbreviation cons' (u v w : V) (h : G.adj u v) (p : G.walk v w) : G.walk u w := +walk.cons h p + lemma exists_eq_cons_of_ne : Π {u v : V} (hne : u ≠ v) (p : G.walk u v), ∃ (w : V) (h : G.adj u w) (p' : G.walk w v), p = cons h p' | _ _ hne nil := (hne rfl).elim