tactic-writing kata

Stream: Codewars

[Jalex Stark]

Just to extract some discussion from the old general thread, I think "write kata on codewars that require / teach tactic-writing" might be an effective way to seed the community with tactic-writing knowledge. Quoting from the old thread:

For such a kata, the initial solution would look like
meta def submission_tactic :=
and the test cases would look like

example : test_prop1 := by submission_tactic
example : test_prop2 := by submission_tactic

So an 8 kyu "tactic-writing hello world" might have an answer that's morally equivalent to

meta def submission_tactic := repeat {apply lemma1 <|> apply lemma2}
and the test cases are things that fall to (possibly long) repeated applications of lemma1 and lemma2. That probably means that something morally equivalent to
meta def submission_tactic := simp only [lemma1, lemma2]
works too, but I'd be fine with that.

[Jalex Stark]

I am half-heartedly trying to learn enough from chapter 8 of programming in Lean to start doing this. I'd be thrilled for someone to beat me to it.

[Mario Carneiro]

You can actually write meta def submission_tactic := `[simp only [lemma1, lemma2]] fyi

[Donald Sebastian Leung]

and the test cases would look like

example : test_prop1 := by submission_tactic
example : test_prop2 := by submission_tactic

Keep in mind to check the generated proofs for sorries and forbidden axioms; otherwise, I would imagine that one could just define their tactic to use sorry and pass all the tests.