constructor is the new split

Stream: lean4

[Kevin Buzzard]

Am I really supposed to be telling the undergraduates that when faced with ⊢ P ∧ Q they now have to type constructor (because split now means something else)? Is there something less verbose which turns this into two goals P and Q?

[Kevin Buzzard]

I guess I could introduce pointy brackets and do refine \<_, _\>...

[Matthew Ballard]

Can you write a small macro or is split reserved?

[Eric Wieser]

Or apply and.intro which is more verbose, but at least the first 5 characters are something they already know

[Kevin Buzzard]

I can't write a small macro whether or not split is reserved. Is there some basic "writing small macros in lean 4 for dummies" md file somewhere?

When I was slowly but surely learning Lean 3, when random stuff like this came up (looks like a useful skill or thing to know, no obviously nice reference for dummies) I would badger people until I understood enough myself and then I'd write a small md file and dump it in the Xena Project chaos. I'm talking 2018 here. Then I'd start linking to it in various places, and pointing people to it on the chat. Then the lean prover community decided that some of the stuff I was generating was useful for the community, and moved it to the community website. This is the origin of files such as this. Eventually someone would come along and just be annoyed by my amateurish attempts to explain stuff and just rewrite them completely, and then they became even more useful.

I wonder if there's room for this kind of document on the community website for lean 4 "tips and tricks"? Or another place to put stuff like this?

[Kevin Buzzard]

The calc mode file was also mine, Patrick wrote the conv mode file, and Chris Hughes wrote the well-founded recursion file because I nagged him to write it because I found it completely impossible to work out with no reference. At the time the only reference we had was #tpil . In the early days of the community when only a few people knew the contents of those files, this stuff was super-useful.

[Matthew Ballard]

macro_rules | `(tactic| split) => `(tactic| constructor)

seems to work

[Newell Jensen]

You can also use angle brackets, fwiw

example : s ∧ q ∧ r → p ∧ r → q ∧ p := by
  intro ⟨_, ⟨hq, _⟩⟩ ⟨hp, _⟩
  exact ⟨hq, hp⟩

[Patrick Massot]

Kevin, if you write useful doc then we'll find or create a place for it.

[Kevin Buzzard]

OK! How do I make my_induction n with d hd do induction' a using MyNat.induction with d hd?

[Kevin Buzzard]

Here myNat.induction is a custom induction principle which uses the numeral 0 rather than MyNat.zero.

[Kevin Buzzard]

:cry:

case a
⊢ 0 + 0 = 0
case a
d: MyNat
hd: 0 + d = d
⊢ 0 + succ d = succ d

Even better, how do I make the cases be zero and succ?
mwe:

import Mathlib.Algebra.Group.Defs -- `import tactic` in mathlib4

whatsnew in
inductive MyNat : Type
| zero : MyNat
| succ : MyNat → MyNat

namespace MyNat

-- notational typeclass for 0
instance : Zero MyNat where
  zero := MyNat.zero

#check (0 : MyNat)

theorem induction : {P : MyNat → Prop} →
  (t : MyNat) → P (0 : MyNat) → ((a : MyNat) → P a → P (a.succ)) → P t :=
fun {_} t zero succ => MyNat.rec zero succ t

def add (a : MyNat) : MyNat → MyNat
| zero => a
| (succ b) => succ (add a b)

instance : Add MyNat where
  add := add

theorem zero_add (a : MyNat) : 0 + a = a := by
  induction' a using MyNat.induction with d hd
/-
unsolved goals
case a
⊢ 0 + 0 = 0

case a
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
-/

[Kyle Miller]

Naming the arguments should be sufficient:

theorem induction : {P : MyNat → Prop} →
  (t : MyNat) → (zero : P (0 : MyNat)) → (succ : (a : MyNat) → P a → P (a.succ)) → P t :=
fun {_} t zero succ => MyNat.rec zero succ t

[Heather Macbeth]

Kevin Buzzard said:

OK! How do I make my_induction n with d hd do induction' a using MyNat.induction with d hd?

@Kevin Buzzard
https://github.com/hrmacbeth/math2001/blob/7b7e5f59ec0fc832cf4f80fd23a4495e6108b2b3/Math2001/Tactic/Induction.lean#L46
(courtesy @Rob Lewis)

[Kevin Buzzard]

Heh, it was Rob who told me all the tactic hacks to make this work in lean 3 :-) Hi Rob!

[Kyle Miller]

@Kevin Buzzard It looks like you don't need a custom induction tactic. The @[eliminator] attribute can be used to override which eliminator to use.

import Mathlib.Algebra.Group.Defs

inductive MyNat : Type
| zero : MyNat
| succ : MyNat → MyNat

namespace MyNat

instance : Zero MyNat where
  zero := MyNat.zero

@[eliminator]
theorem induction : {P : MyNat → Prop} →
  (t : MyNat) → (zero : P (0 : MyNat)) → (succ : (a : MyNat) → P a → P (a.succ)) → P t :=
fun {_} t zero succ => MyNat.rec zero succ t

def add (a : MyNat) : MyNat → MyNat
| zero => a
| (succ b) => succ (add a b)

instance : Add MyNat where
  add := add

theorem zero_add (a : MyNat) : 0 + a = a := by
  induction' a with d hd
  /-
  case zero
  ⊢ 0 + 0 = 0

  case succ
  d: MyNat
  hd: 0 + d = d
  ⊢ 0 + succ d = succ d
  -/

end MyNat

[Moritz Doll]

Kevin Buzzard said:

I can't write a small macro whether or not split is reserved. Is there some basic "writing small macros in lean 4 for dummies" md file somewhere?

Actually, I thought about writing a small 'tactic writing for dummies' file (mainly to not forget what I have learned). If there is real interest in that, I can put it higher on my todo list.

[James Gallicchio]

I know it's long/has way more information than you might want, but the examples in the metaprogramming book are a pretty good cheat sheet. E.g. here for macros