Zulip Chat Archive

Stream: new members

Topic: Defining walks


view this post on Zulip 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 ^__^

view this post on Zulip 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 

view this post on Zulip Oskar Berndal (Oct 30 2020 at 15:35):

Yes thank you ^___^

view this post on Zulip 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

view this post on Zulip 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)
-/

view this post on Zulip 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 :^)

view this post on Zulip 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)

view this post on Zulip 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 =)

view this post on Zulip 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