## Stream: Codewars

### Topic: tactic-writing kata

#### Jalex Stark (May 11 2020 at 00:27):

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 (May 11 2020 at 00:28):

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 (May 11 2020 at 00:44):

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

#### Donald Sebastian Leung (May 11 2020 at 05:08):

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.

Last updated: May 08 2021 at 23:10 UTC