Zulip Chat Archive

Stream: general

Topic: automatic cases


view this post on Zulip Kenny Lau (Jul 28 2018 at 08:56):

Can we have a tactic that does cases on the argument of XX.rec or XX.rec_on?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 09:01):

That sounds like a really nice basic tactic for a tactic-learner to write!

view this post on Zulip Kenny Lau (Jul 28 2018 at 09:08):

good! are you a tactic-learner?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 09:36):

Maybe @Chris Hughes is? I think he got a bit disheartened when he realised he had 100 questions and couldn't face asking Mario and Simon all of them though...

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 09:36):

(and of course I was no help)

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 09:37):

Maybe there should be a basic tactic-writing thread. The workflow I see is: start Zulip thread, spam it with basic questions which are not covered in PIL, experts occasionally make insightful comments, someone writes some notes and sticks them up in the mathlib docs project, we all learn something.

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 09:45):

From Programming In Lean:

open tactic

meta def destruct_conjunctions : tactic unit :=
repeat (do
l  local_context,
first $ l.map (λ h, do
ht  infer_type h >>= whnf,
match ht with
| `(and %%a %%b) := do
n  get_unused_name `h none,
mk_mapp ``and.left [none, none, some h] >>= assertv n a,
n  get_unused_name `h none,
mk_mapp ``and.right [none, none, some h] >>= assertv n b,
clear h
| _ := failed
end))

example (P Q : Prop) (HPQ : P  Q) : false :=
begin
  destruct_conjunctions,
  exact false.intro
end

That's how to break up an and in the hypotheses. You just want to break up a rec in the conclusion. How hard can it be? ;-)

view this post on Zulip Johan Commelin (Jul 28 2018 at 09:46):

Maybe there should be a basic tactic-writing thread. The workflow I see is: start Zulip thread, spam it with basic questions which are not covered in PIL, experts occasionally make insightful comments, someone writes some notes and sticks them up in the mathlib docs project, we all learn something.

Or a "tactics" stream? We've got a "maths" stream after all. This seems like a general enough topic (in the non-Zulip sense) to turn it into a stream.


Last updated: May 18 2021 at 17:44 UTC