Defining walks

Stream: new members

[Oskar Berndal]

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]

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]

Yes thank you ^___^

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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

[Oskar Berndal]

(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]

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]

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