syntax options for `obtain`

Stream: new members

[rzeta0]

So far I have seen obtain used in the following two ways:

obtain ha | hb := h -- where h is a disjunction

obtain ⟨ha , hb⟩ := h -- where h is a conjunction

I was trying to decode the syntax (couldn't find any explanatory documentation) because the syntax doesn't appear to be consistent.

I'd welcome an explanation or a pointer to docs. here are my immediate questions / assumptions:

• I guess the | is part of a pattern that unifies with disjunctions.
• I guess the comma is part of a pattern that unifies with conjunctions.
• But why does one have brackets and the other not?

Are there other patterns used with obtain?

[Ruben Van de Velde]

| is if you have an inductive type with multiple variants; \<> matches the syntax for constructors of types with multiple fields

[rzeta0]

Hi @Ruben Van de Velde I don't know what those words mean - sorry I am a beginner.

I can't see any connection between induction (inductive proofs) and a disjunctive statement.

Similarly I can't see the connection between constructors (object orients programming?) and conjunctive statements.

I appreciate you trying to help. Are the words you are using from "type theory" ?

[Kyle Miller]

"Inductive type" is a general concept, and they are defined using the inductive and structure commands. If you've heard of "algebraic data type" from other languages, it's similar.

[Kyle Miller]

The notation ⟨a, b, c, ...⟩ is used in Lean for creating data using a constructor, and so obtain uses it to extract data from a constructor.

The | is used in the inductive command for separating all the constructors, and so obtain uses it to separate each alternative.

[Ruben Van de Velde]

Basically, you can have two kinds of types:

• a type where you have fields a, b, c, and a value of your type has all of those. For example: a rational number given by a numerator and denominator
• a type where you have one of several options: e.g. an integer defined as either a nonnegative number or a negative one <-- these are inductive types

[Kyle Miller]

⟨ha | hb⟩ would mean "match a value from a type with a unique constructor whose first value is from a type with two constructors, and bind the result to ha or hb, respectively."

[Kyle Miller]

They're called "inductive types" because they come with induction principles. The definition of Nat in Lean as an inductive type automatically gives the usual induction principle for natural numbers.

[Ruben Van de Velde]

A value of the first kind can be written as { a := ..., b := ..., c := ... } or shorter as ⟨..., ...., ...⟩

[Eric Wieser]

Explicitly, if you have

inductive MyType where
| one (x y z : Nat)
| two (w : Nat)
| three

then you would use this with obtain as

let m : MyType := ...
obtain ⟨x, y, z⟩ | w | - := m

[rzeta0]

thanks for the replies, I will have to print this out ands study it

[Johan Commelin]

The syntax is documented in the docstring of rcases. If obtains docstring does not point to that, we should fix that.