automatic cases

Stream: general

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

good! are you a tactic-learner?

[Kevin Buzzard]

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...

[Kevin Buzzard]

(and of course I was no help)

[Kevin Buzzard]

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.

[Kevin Buzzard]

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? ;-)

[Johan Commelin]

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.