The “Function World” level of the Natural Number Game explores this concept in Lean3. You are given a maze of functions between types (or equivalently material implications between formulas) and can either advance from your starting type or transform your goal type back through the maze, or do both and meet in the middle.
It was very confusing to me at first, mostly because the same inference rule can be applied both backwards and forwards. And because not all tactics use inference rules (some just do term rewriting).
The “Function World” level of the Natural Number Game explores this concept in Lean3. You are given a maze of functions between types (or equivalently material implications between formulas) and can either advance from your starting type or transform your goal type back through the maze, or do both and meet in the middle.
It was very confusing to me at first, mostly because the same inference rule can be applied both backwards and forwards. And because not all tactics use inference rules (some just do term rewriting).
Yeah I’m still not 100% clear on what the difference is between two-way implication and equality here.
In this Lean example or in the example in this post?
Oh sorry, I meant in Lean.