how to name new hypothesis using cases h with in Lean 4

Stream: new members

[Brando Miranda]

Obvious newbie question. I've search lean4 manual, TP in Lean, MIL and more but can't make it work. I have a disjunction in my hypothesis. I did:

    -- to do inv cancel let's break h_zero_abs_x into both cases 0 < x and 0 < -x and prove both cases
    #check Or
    cases h_zero_abs_x with -- TODO: how to name hypothesis with cases in lean4
      | Or.inl h_x_pos => sorry
      | Or.inr h_x_neg => sorry

but lean4 doesn't like it. What am I doing wrong? I'd like to name my new hypothesis corresponding to each input to the constructor myself.

Error

invalid alternative name 'Or.inl'

but I hovered over Or and it says it exists

Or (a b : Prop) : Prop
Or a b, or a ∨ b, is the disjunction of propositions. There are two constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b, and you can use match or cases to destruct an Or assumption into the two cases.

import Init.Prelude

so I'm puzzled.

Thanks in advance!

[Kyle Miller]

With cases syntax, you need to use inl and inr rather than Or.inl and Or.inr

[Kyle Miller]

These names come from the names of the constructors themselves, and in particular, the names of the arguments to Or.casesOn

Or.casesOn {a b : Prop} {motive : a ∨ b → Prop} (t : a ∨ b) (inl : ∀ (h : a), motive ⋯) (inr : ∀ (h : b), motive ⋯) :
  motive t

[Brando Miranda]

Sorry if this is a dumb question. What confuses me is that cases seems to have very similar syntax to match statements in function defs. When I tried defining addition for MyNats it insisted (unless I did open MyNats) that I used MyNats. So I am still confused why Lean 4 knows what constructors to use without open while in this case seems to magically know it. e.g., Why isn't it Or.casesOn.inl then?

[Kyle Miller]

It's similar to match, but it's not match. It's confusing that it looks the same but it has different behavior, but the simple answer is that it's just a different tactic.

A longer answer might be that cases doesn't work using pattern matching. You're not allowed use match on a proof anyway.

[Kyle Miller]

It's seeing it's Or because you're passing it h_zero_abs_x and it can see the type, and since cases only gives you cases for each "minor premise" of Or.casesOn, there's no need to qualify the names.

[Kyle Miller]

Potentially, cases could be modified to allow writing Or.inl and Or.inr, or at least detect that you've done it and tell you what to write instead.

[Kyle Miller]

By the way, for MyNats, if you write .succ, if Lean can figure out that the expected type is a MyNat, it will read that as MyNat.succ. That saves needing to open MyNat if you're just trying to avoid writing MyNat.succ, at the small cost of prefixing the constructor with a dot.

[Brando Miranda]

Super helpful Kyle. Thank you. However, sadly I'm still struggling to tell lean to manipulate my goal.

Now that I did

    cases h_zero_abs_x with -- TODO: how to name hypothesis with cases in lean4
      | inl h_x_pos => by
        have h_x_ne_zero : x ≠ 0 := by exact ne_of_gt h_x_pos
      | nr h_x_neg => sorry -- have h_neg_x_ne_zero : -x ≠ 0 := ne_of_gt h_x_neg

I am trying to construct the proof inside each case. But it keeps giving me syntax error e.g.,

unexpected token 'by'; expected '?', '_', '{' or tactic

I feel it's complaint make sense, since I am not stating a goal (so perhaps it's angry at the having another by) but deconstructing the hypothesis. But then I don't understand how I'm suppose to construct the proof for each case if Lean 4 doesn't let me generate the tactic proofs as I'd normally would.

[Ruben Van de Velde]

Remove the by after =>

[Brando Miranda]

Ruben Van de Velde said:

Remove the by after =>

I had tried that. But, what was wrong is that my later case had a type constructor. It says nr instead of inr. However, it was hard to me to predict that would cause a bug in the current line I was actually trying to construct a proof on. Now I know cases needs both constructors to be done properly or it fails.

[Brando Miranda]

fyi, if I have a analogous bug with match (typo in second constructor) it doesn't make Lean4 completely unusable on my other cases. e.g.,

inductive MyUnderyNat : Type
| O : MyUnderyNat
| S : MyUnderyNat -> MyUnderyNat

def add : MyUnderyNat -> MyUnderyNat -> MyUnderyNat
| MyUnderyNat.O, n => n
| MyUnderyNat.Su m, n => MyUnderyNat.S (add m n)

ie putting my cursor on n doesn't confuse lean4.

[Brando Miranda]

Kyle Miller said:

By the way, for MyNats, if you write .succ, if Lean can figure out that the expected type is a MyNat, it will read that as MyNat.succ. That saves needing to open MyNat if you're just trying to avoid writing MyNat.succ, at the small cost of prefixing the constructor with a dot.

What did you have in mind for this? I tried a specific example by defining the add function without prefixing but Lean4 didn't like it:

inductive MyUnderyNat : Type
| O : MyUnderyNat
| Succ : MyUnderyNat -> MyUnderyNat

def add : MyUnderyNat -> MyUnderyNat -> MyUnderyNat
| MyUnderyNat.O, n => n
| MyUnderyNat.Succ m, n => MyUnderyNat.Succ (add m n)

def add' (m n : MyUnderyNat) : MyUnderyNat :=
  match m with
  | O => n
  | Succ m' => Succ (add' m' n)

error

basic_nats.lean:12:24
Messages (1)
basic_nats.lean:12:4
invalid pattern, constructor or constant marked with '[match_pattern]' expected

[Scott Kovach]

Kyle was talking about this:

inductive Foo | bar
example : Foo := bar  -- unknown identifier
example : Foo := .bar -- ok; expected type is Foo, so this is resolved to mean Foo.bar

[Mark Fischer]

This is an aside, but in most cases the following two should be the same.

... := by exact ne_of_gt h_x_pos

... := ne_of_gt h_x_pos

by is a keyword that brings you into tactic mode while exact is a tactic that accepts terms (so you can think of it as bringing you back into term-mode.) Most of the time instances of by exact are redundant.

[Brando Miranda]

Scott Kovach said:

Kyle was talking about this:

inductive Foo | bar
example : Foo := bar  -- unknown identifier
example : Foo := .bar -- ok; expected type is Foo, so this is resolved to mean Foo.bar

got it, thanks. The example that worked for me what

def add' (m n : MyUnderyNat) : MyUnderyNat :=
  match m with
  | .O => n
  | .Succ m' => .Succ (add' m' n)

I didn't know before this that inductive Foo | bar would define a inductive type with cons bar and that .bar made sense. Never seen that notation in any other programming language. Cool!

[Brando Miranda]

very related. When I do cases h_zer_lt_abs_x it introduces new hypothesis into my local context with a name with a unicode. I assume this is the reason whenever I try to refer to it I can't use it or rename it. How do I refer to a hypothesis that was automatically named? Or that might have a special unicode? e.g.,
My current tactic

    cases h_zero_lt_abs_x

leads to this hypothesis being introduced (as expected):

h✝: 0 < x

but even if I copy paste the symbol ✝ or pair of symbols or manually write "\dagger", I can't refer to that hypothesis. How do I refer to that hypothesis so I can actually make progress in my proof? (ideally rename it to h_x_pos).

[Mark Fischer]

With Nat, refl & step works for me.

opaque G : Prop
example (h: 0 < x) : G := by
    cases h with
    | refl => sorry
    | @step n t => sorry

[Brando Miranda]

I don't think that is what I was looking for (?). I'm not using the with statement in this second version of using the cases tactic.

[Brando Miranda]

Lean produces goals with funny names I can refer to no matter what I do. I can't rename them or use them. But I want them of course, hence, why I called cases :)

[Johan Commelin]

@Brando Miranda Does rename_i h_x_pos do what you want?

[Mario Carneiro]

Brando Miranda said:

I didn't know before this that inductive Foo | bar would define a inductive type with cons bar and that .bar made sense. Never seen that notation in any other programming language. Cool!

Note that the syntax there is a bit compressed and possibly misleading. The more usual way to write it would be

inductive Foo
  | bar

which is shorthand for

inductive Foo : Type where
  | bar : Foo

[Mario Carneiro]

Likewise .bar is shorthand for Foo.bar, getting the type Foo from the expected type. It has precedent in Swift

[Paul Rowe]

Brando Miranda said:

Lean produces goals with funny names I can refer to no matter what I do. I can't rename them or use them. But I want them of course, hence, why I called cases :)

If you just use cases h_zero_abs_x without the with then all the cases will appear in the infoview labeled e.g. case inl and case inr. You can then use the case tactic to focus on whichever goal you want: case inl. If you add an arguments after the case identifier, it will start naming the inaccessible hypotheses: case inl h_x_pos will give you what you're looking for.

[Paul Rowe]

By the way, older versions of Lean 3 used to automatically name such hypotheses according to some pre-defined convention. While that was convenient for not having to name everything, it makes proofs quite brittle to changes in Lean, Mathlib, etc.

[Matt Diamond]

could a moderator move @Samyak Tuladhar 's post to a new thread? thanks

Edit: never mind, moved it myself

[Notification Bot]

A message was moved from this topic to #new members > Code is not live compiling by Matt Diamond.