maze tactic?

Stream: new members

[Andre Popovitch]

I'm playing the natural number game (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=5&level=9) and hit upon this:

I asked around on Zulip and apparently there is not a tactic for this, perhaps because this level is rather artificial. In world 6 we will see a variant of this example which can be solved by a tactic. It would be an interesting project to make a tactic which could solve this sort of level in Lean.

I'm just getting started with lean and this seems like a fun tactic to write if it hasn't already been written. Should I write it, and if I do would I be able to get it merged into the lean standard tactic library?

[Andre Popovitch]

It seems like a relatively straightforward graph search problem

[Huỳnh Trần Khanh]

not directly related to your question but there's a cool maze game in lean 4 https://github.com/dwrensha/lean4-maze

[Kyle Miller]

Have you gotten to Proposition World, level 9? This exists as cc for propositions (vs functions).

[Andre Popovitch]

wow that is a cool game

[Andre Popovitch]

I have not @Kyle Miller, I’m still on function world

[Mario Carneiro]

Isn't solve_by_elim essentially a DFS search algorithm for this "maze"?

[Mario Carneiro]

import tactic
example (A B C D E F G H I J K L : Type)
(f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
(f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
(f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L)
 : A → L :=
by { intro, solve_by_elim { max_depth := 8 } }

You have to increase the max depth because non-artificial examples usually don't require such a long proof