Zulip Chat Archive

Stream: Codewars

Topic: tactic-writing kata


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 11 2020 at 00:44):

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

view this post on Zulip 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