## Stream: new members

### Topic: Defining walks

#### Oskar Berndal (Oct 30 2020 at 15:01):

Hello everyone! I am trying to define a type of walks in a square grid. I want to parametrize the type over endpoints of the walk and the number of backwards-moves (moves that are either up or left). I made the following definition

def node := ℕ×ℕ

inductive back_walk: node → ℕ → node → Type
| start: Π s: node, back_walk s 0 s
| d: Π s: node, Π n x y : ℕ, back_walk s n ⟨ x, y ⟩ → back_walk s n ⟨ x+1, y ⟩
| r: Π s: node, Π n x y : ℕ, back_walk s n ⟨ x, y ⟩ → back_walk s n ⟨ x, y+1 ⟩
| l: Π s: node, Π n x y : ℕ, back_walk s n ⟨ x+1, y ⟩ → back_walk s (n+1) ⟨ x, y ⟩
| u: Π s: node, Π n x y : ℕ, back_walk s n ⟨ x, y+1 ⟩ → back_walk s (n+1) ⟨ x, y ⟩


which seems to do what I want it to do, but it would be nice to be able to have the variables of the constructors somehow be captured by the scope of the inductive definition rather than the \Pi's at the constructors. I'm wondering if anyone has a suggestion? Thanks ^__^

#### Yakov Pechersky (Oct 30 2020 at 15:29):

Is this more what you mean?

def node := ℕ×ℕ

inductive back_walk (s : node) : ℕ → node → Type
| start : back_walk 0 s
| d : Π n x y : ℕ, back_walk n ⟨ x, y ⟩ → back_walk n ⟨ x+1, y ⟩
| r : Π n x y : ℕ, back_walk n ⟨ x, y ⟩ → back_walk n ⟨ x, y+1 ⟩
| l : Π n x y : ℕ, back_walk n ⟨ x+1, y ⟩ → back_walk (n+1) ⟨ x, y ⟩
| u : Π n x y : ℕ, back_walk n ⟨ x, y+1 ⟩ → back_walk (n+1) ⟨ x, y ⟩


#### Oskar Berndal (Oct 30 2020 at 15:35):

Yes thank you ^___^

#### Yakov Pechersky (Oct 30 2020 at 15:36):

I'm not sure how you plan on using it, so that might not be the right way to express it

#### Yakov Pechersky (Oct 30 2020 at 15:43):

def node := ℕ×ℕ

inductive back_walk (s : node) : ℕ → node → Type
| start : back_walk 0 s
| d : Π {n x y : ℕ}, back_walk n ⟨ x, y ⟩ → back_walk n ⟨ x+1, y ⟩
| r : Π {n x y : ℕ}, back_walk n ⟨ x, y ⟩ → back_walk n ⟨ x, y+1 ⟩
| l : Π {n x y : ℕ}, back_walk n ⟨ x+1, y ⟩ → back_walk (n+1) ⟨ x, y ⟩
| u : Π {n x y : ℕ}, back_walk n ⟨ x, y+1 ⟩ → back_walk (n+1) ⟨ x, y ⟩

open back_walk

instance {x y x' y' n : ℕ} : has_repr (back_walk ⟨x, y⟩ n ⟨x', y'⟩) :=
⟨λ _, string.intercalate ", " ["end: " ++ repr (x, y), "steps: " ++ repr n, "start: " ++ repr (x', y')]⟩

#eval (start : back_walk (5,5) _ _).u.d.l.d.l.d.r
/-
end: (5, 5), steps: 3, start: (6, 5)
-/


#### Oskar Berndal (Oct 30 2020 at 15:49):

Oh you are quite right I have d and rmixed up. Thank you, also for providing the nice debugging thingie :^)

#### Oskar Berndal (Oct 30 2020 at 15:50):

(Although I'd say that you have end and start mixed up there, I'm following the strange convention that pos y-dir is down and pos x-dir is right)

#### Yakov Pechersky (Oct 30 2020 at 15:52):

Well, if it's a "back walk" then I think you're counting the l and u taken backwards. Of course, not sure of the actual problem, so easy to change the labels =)

#### Oskar Berndal (Oct 30 2020 at 15:55):

Maybe it's just the name 'back_walk' that is bad, because it is meant to convey something like 'a walk where we count the number of backs' which 'back_walk' does not convey

Last updated: May 06 2021 at 21:09 UTC