missing tactics

Stream: lean4

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

Wait, that is \or...

[Jason Rute]

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]

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]

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]

I think I will port rcases for this stuff

[Damiano Testa]

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]

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]

@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]

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]

You can use simp_all to use all hypotheses: cases h <;> simp_all

[Yakov Pechersky]

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]

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]

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]

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