Zulip Chat Archive

Stream: new members

Topic: how to name hypotheses introduced by `split` ?

Ranjit Jhala (Sep 21 2024 at 23:33):

Hi all, I'm very much a beginner and my apologies if this is the wrong place to ask -- but how can I name the hypotheses introduced by the split tactic? Thanks!

Derek Rhodes (Sep 21 2024 at 23:55):

Hi @Ranjit Jhala , it sounds like you might be working through an older tutorial/book based on Lean 3, could you please check?

The reason why I say that is because lean4 uses constructor instead of split, at least for the beginner material that I have seen, and as mentioned in the lean3 to 4 survival guide:

https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users

Ranjit Jhala (Sep 22 2024 at 01:23):

Thanks @Derek Rhodes!

I came across split using the below which seems to be for lean4?

https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#split-tactic

For some context, I'm trying to do something like:

def length {α : Type} (xs: List α) : Nat :=
  match xs with
  | nil => 0
  | cons _ xs' => 1 + length xs'

def pos_length (xs: List Nat) : Nat :=
  match xs with
  | nil => 0
  | cons x xs' => if x = 1 then length xs' + x else length xs'

theorem pos_len: ∀ (xs : List Nat), pos_length xs <= length xs := by
  intros xs
  induction xs
  case nil  => simp [pos_length]
  case cons x xs' _ =>
    simp [pos_length, length]
    split
    . simp [*, Nat.add_comm]
    . simp []

The above proof works -- as the * does the job of using the hypothesis to rewriting the x with 1.

Replacing split with constructor does not: I get

tactic 'constructor' failed, no applicable constructor found

However, I'm wondering how I can name the hypothesis x=1 them if in fact I do need to use it specifically...

Derek Rhodes (Sep 22 2024 at 01:55):

Yep you can name the hypothesis (in this case h1) within the definition of pos_length, with something like:

cons x xs' => if h1: x = 1 then length xs' + x else length xs'

then instead of split, we can use split_ifs. But, I've only used that a couple of times. I'll try to find more info. (maybe split by itself will pick up the hypothesis name?)

By the way, I'm still a newbie and I think the previous statement I made regarding using constructor instead of split only applies to Mathlib projects, so please disregard that.