Using Existential in a hypothesis

Stream: new members

[Gabriel Alfour]

Hey, I come from a Coq background, and am not sure how to destruct an existential in a hypothesis.

I tried cases, but then:

• I failed to name the variables. Like cases tl with | Exists n hn => doesn't work
• If I let it autogenerate variable names, I get w✝ and h✝, which I can not refer to in code without a tokenization error

I looked for a lot of docs, and asked GPT4, but can't find anything that helps. So as well as help, if you have pointers, that would be very nice

[Kyle Miller]

I usually use the obtain tactic (from std)

example {p : Nat → Prop} (h : ∃ x, p x) : False := by
  obtain ⟨n, hn⟩ := h
  /-
  α : Type
  P : α → Bool
  p : ℕ → Prop
  n : ℕ
  hn : p n
  ⊢ False
  -/
  sorry

Here are some other options:

example {p : Nat → Prop} (h : ∃ x, p x) : False := by
  cases h with | intro n hn => -- you need to know that the name of the constructor is `intro`
  sorry

example {p : Nat → Prop} (h : ∃ x, p x) : False := by
  cases h
  rename_i n hn
  sorry

example {p : Nat → Prop} (h : ∃ x, p x) : False := by
  cases' h with n hn -- mathlib tactic (like Lean 3 `cases`)
  sorry

[Patrick Massot]

The recommended Mathlib style is rcases h with ⟨n, hn⟩.

[Shreyas Srinivas]

Kyle Miller said:

Here are some other options:

example {p : Nat → Prop} (h : ∃ x, p x) : False := by
  cases h with | intro n hn => -- you need to know that the name of the constructor is `intro`
  sorry

The infoview shows the constructor name.

[Kyle Miller]

Something I forget we can do now in Lean 4 is let ⟨n, hn⟩ := h in a tactic proof.

[Kyle Miller]

Re constructor names, if you have std imported, then in VS Code if you put your cursor on the cases line you can see

image.png

Clicking that lightbulb shows an option

image.png

and clicking that option yields

  cases h with
  | intro w h => sorry

[Richard Copley]

Kyle Miller said:

Something I forget we can do now in Lean 4 is let ⟨n, hn⟩ := h in a tactic proof.

Also available is have ⟨n, hn⟩ := h (with subtly different effects), and both versions, let and have, work in term mode.
In tactic mode, intro does most (but not all) of what rintro does, too. And in term mode, there is fun ⟨n, hn⟩ => _.

[Yaël Dillies]

Patrick Massot said:

The recommended Mathlib style is rcases h with ⟨n, hn⟩.

I really think we should discourage rcases. Its syntax is far from have and its name doesn't reflect the semantics as well as obtain does.

[Gabriel Alfour]

@Kyle Miller Thx a lot!

[Gabriel Alfour]

• Is there a way to have this let/have destruct h at the same time?
• How can I make it so that on my own variants, I can destructure them in tactics mode with let / have?
• I tried to import std but it's not recognizes, and when I open Std, I don't get those suggestions

[Kyle Miller]

You can nest destructuring:

example {p q : Nat → Prop} (h : ∃ x, p x ∧ q x) : False := by
  have ⟨n, ⟨hp, hq⟩⟩ := h
  sorry

And you can use that angle bracket notation is right associating:

example {p q : Nat → Prop} (h : ∃ x, p x ∧ q x) : False := by
  have ⟨n, hp, hq⟩ := h
  sorry

[Kyle Miller]

Gabriel Alfour said:

• How can I make it so that on my own variants, I can destructure them in tactics mode with let / have?

By "variant" do you mean type? So long as your type has just one constructor you can use this angle bracket notation.

[Kyle Miller]

Here's a working example with obtain:

import Std

example {p : Nat → Prop} (h : ∃ x, p x) : False := by
  obtain ⟨n, hn⟩ := h
  sorry

[Gabriel Alfour]

@Kyle Miller I see, thx a lot!

[Gabriel Alfour]

There's still a part that I don't understand with cases: it only destructs variables. But if I have f x in an hypothesis, and I do cases (f x), nothing happens (except creating as many identical goals as there are cases of the type of f x. But f x itself doesn't get rewritten

Or possibly something equivalent to case_eq?

[Patrick Massot]

#mwe?

[Kyle Miller]

example (n : Nat) : False := by
  cases h : n + 1 -- generates h : n + 1 = ... hypotheses in each case

[Notification Bot]

This topic was moved here from #general > Using Existential in a hypothesis by Kyle Miller.

[Gabriel Alfour]

@Patrick Massot I have just posted it in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Add.20new.20goal.20and.20hypothesis.20at.20the.20same.20time/near/401046232

It might make sense to merge the two threads? Not sure if that's possible