# Zulip Chat Archive

## Stream: lean4

### Topic: missing tactics

#### Kevin Buzzard (Mar 23 2021 at 16:00):

In Lean 3 I could make cheap and dirty tactics with the `\[tac...]`

trick. I see that Lean 4 doesn't have a `split`

tactic yet, but my users (who never write term mode proofs) will be used to this. What is the Lean 4 version of

```
meta def tactic.interactive.split := `[apply And.intro]
```

?

#### Sebastian Ullrich (Mar 23 2021 at 16:02):

See https://leanprover.github.io/lean4/doc/tactics.html#extensible-tactics :)

#### Kevin Buzzard (Mar 23 2021 at 16:13):

Sorry. I read through the entire manual about a month ago but stuff doesn't stick in my brain like it used to.

#### Kevin Buzzard (Mar 23 2021 at 16:21):

This is great -- I now have `split`

, `left`

and `right`

. Can I get `cases (h : p \and q) with hp hq`

this way? Where can I read about how to do this? Or should I just wait?

#### Jason Rute (Mar 24 2021 at 02:22):

Do you not like the built-in Lean 4 `cases`

tactic (found on the same page)?

```
theorem ex1 : p ∨ q → q ∨ p := by
intro h
cases h with
| inl h1 =>
apply Or.inr
exact h1
| inr h2 =>
apply Or.inl
assumption
```

#### Jason Rute (Mar 24 2021 at 02:23):

Wait, that is `\or`

...

#### Jason Rute (Mar 24 2021 at 02:51):

Ok, yeah, I guess the built in version of `cases (h : p \and q)`

is a bit awkward:

```
theorem ex1 : p ∧ q → q ∧ p := by
intro h
cases h with
| intro hp hq =>
skip
```

#### Kevin Buzzard (Mar 24 2021 at 07:37):

Yes I don't like it because by default it doesn't name variables and in the examples you give the user needs to know the names of the constructors eg inl and intro. Mathematicians can use this software in a way which involves knowing nothing about what's going on under the hood you see, not even knowing what an inductive type or a constructor is for example.

#### Yakov Pechersky (Mar 24 2021 at 07:42):

By the way, you don't have to know `intro`

in the `And`

example, this is fine:

```
theorem ex1 : p ∧ q → q ∧ p := by
intro h
cases h with
| _ hp hq =>
skip
```

#### Mario Carneiro (Mar 24 2021 at 07:43):

I think I will port `rcases`

for this stuff

#### Damiano Testa (Mar 24 2021 at 07:44):

In my personal experience, `cases`

was a very good tactic to have at the beginning. Now that I am more familiar with the system, I tend to prefer `rcases`

, but I was intimidated by it, when I was starting to use Lean.

#### pcpthm (Mar 24 2021 at 07:47):

`let`

can be used to destruct a term (but it leaves unnamed hypothesis in the local context currently):

```
theorem ex1 : p ∧ q → q ∧ p := by
intro h
let ⟨p, q⟩ := h
exact ⟨q, p⟩
```

Also, `intro`

accepts patterns:

```
theorem ex1' : p ∧ q → q ∧ p := by
intro ⟨p, q⟩
exact ⟨q, p⟩
```

It is missing "or patterns" of `rcases`

/ `rintro`

, though.

#### Leonardo de Moura (Mar 25 2021 at 01:39):

@pcpthm We already have intro+match notation

```
theorem ex : p ∨ (q ∧ r) → q ∨ p := by
intro
| Or.inl h => exact Or.inr h
| Or.inr ⟨h, _⟩ => exact Or.inl h
```

#### pcpthm (Mar 25 2021 at 13:21):

Ah, I didn't think about combining `intro`

and the pattern patching syntax in that way.

While I experimenting with this kind of code I found this example:

```
example (a b : Nat) : a = 0 ∨ b = 0 → a * b = 0 := by
intro h
cases h with
| inl h => rw h; simp
| inr h => rw h; simp
-- Can I remove duplication from the proof above?
-- Using the "preprocessing" tactics feature of `cases`, I get an error "alternative 'inl' is not"
cases h with (rw h; simp)
| inl h => done
| inr h => done
-- I cannot use the patternless form of `cases` either because I cannot access resulting hypotheses:
cases h <;> (rw ???; simp) -- Can I refer to the unnamed variable?
-- it is ugly but works
refine (match h with | Or.inl h => ?_ | Or.inr h => ?_)
allGoals (rw h; simp)
```

With mathlib `rintro`

the above example can be written concisely:

```
by rintro (rfl | rfl); simp
-- Or without using the `rfl` feature
by rintro (h | h); rw h; simp
```

#### Sebastian Ullrich (Mar 25 2021 at 13:26):

You can use `simp_all`

to use all hypotheses: `cases h <;> simp_all`

#### Yakov Pechersky (Mar 25 2021 at 13:27):

This also worked for me:

```
example (a b : Nat) : a = 0 ∨ b = 0 → a * b = 0 := by
intro h
cases h with | _ h' => ?_ <;>
{ rw h';
simp }
```

#### pcpthm (Mar 25 2021 at 13:27):

Sebastian Ullrich said:

You can use

`simp_all`

to use all hypotheses:`cases h <;> simp_all`

That is an another new tactic I missed. Thank you!

#### pcpthm (Mar 25 2021 at 13:36):

Yakov Pechersky said:

This also worked for me:

`example (a b : Nat) : a = 0 ∨ b = 0 → a * b = 0 := by intro h cases h with | _ h' => ?_ <;> { rw h'; simp }`

More simply

```
example (a b : Nat) : a = 0 ∨ b = 0 → a * b = 0 := by
intro h
cases h with | _ h => rw h; simp
```

just worked for me. It is a surprise and I didn't know `cases`

works this way. It almost looks like goals are in superposition or something. I don't quite understand how it works yet.

<del>Unfortunately `simp_all`

fails with an error message "unknown free variable '_uniq.1038'" for some reason:</del>

Edit: I updated Lean to current master and it now works!

```
example (a b : Nat) : a = 0 ∨ b = 0 → a * b = 0 := by
intro h
cases h <;> simp_all
```

#### Leonardo de Moura (Mar 25 2021 at 14:42):

<del>Unfortunately simp_all fails with an error message "unknown free variable '_uniq.1038'" for some reason:</del>

Edit: I updated Lean to current master and it now works!

I fixed a bug that produced this error message last night. ~~Could you please try the ~~`master`

branch?

Last updated: May 07 2021 at 12:15 UTC