search

kbuzzard / FilterGame

An interactive game introducing the concept of a filter.
MIT License
5 stars 3 forks source link

A start to Function World: Levels 1,2,3 #11

Closed IainMcWhinnie closed 3 months ago

IainMcWhinnie commented 3 months ago

Hello Kevin, I've created the first three levels of function world with content and hints. Note that the conclusion of level 3 tells the player the fact you can just use tauto for all three levels; I don't think we should hide this from players given they are likely pretty good at using intro, apply and rw already to prove logical goals.

Let me know what you think, Iain

kbuzzard commented 3 months ago

Thanks a lot! These look basically fine to me; I had a couple of minor comments about language but I'll just make the changes myself.

kbuzzard commented 3 months ago

The reason tauto is solving these goals, by the way, is not because of the tauto part, it's because when tauto is done it tries solve_by_elim, which is basically "apply on steroids" like simp is rw on steroids. This is like how rw tries rfl.

Seems like the plan for the rest of function world is written in comments in FunctionWorld.lean BTW.