Zulip Chat Archive

Stream: lean4

Topic: missing tactics


view this post on Zulip 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]

?

view this post on Zulip Sebastian Ullrich (Mar 23 2021 at 16:02):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jason Rute (Mar 24 2021 at 02:23):

Wait, that is \or...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 24 2021 at 07:43):

I think I will port rcases for this stuff

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Mar 25 2021 at 13:26):

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

view this post on Zulip 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 }

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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