flatten conjunction access

Stream: new members

[Dan Abolafia]

Noob question, is it possible to flatten conjunction access?

At the end of the conjunction section in the tutorial, it says

Lean also allows you to flatten nested constructors that associate to the right

This is nice, because I can write ⟨p, q, r⟩ instead of ⟨p, ⟨q, r⟩⟩.

I'd like to be able to flatten access. Given h : p ∧ q ∧ r, how do I get the 3rd position in a fixed number of characters?
i.e. h.3 instead of h.2.2, though h.3 is not supported for conjunction.

If I had a conjunction of n items, it seems silly to have to write h.2.2. ... .2.2 to get the last item.
examples)

[Patrick Massot]

I don't think we have anything like this, but it would be easy to write (but it's probably less useful than you think it is).

[Dan Abolafia]

Is a list of type Prop possible? Seems to me that would be equivalent to multi-way conjunction.

[Kevin Buzzard]

Although it's rare to get a .2.2.2 I've certainly seen plenty of .2.1's and .2.2's in code which undergraduates produce.

[Bryan Gin-ge Chen]

I think most of those disappeared from my code once I learned to use rcases.

[Dan Abolafia]

I guess my style is bad. I was writing a proof that uses h.2.2.2.2. What is generally the approach to avoiding many nested conjunctions in the statement of a theorem?

[Kevin Buzzard]

I think Bryan is right -- I was wondering why I hadn't written .2.2 recently.

[Kevin Buzzard]

When you introd h, you should have rintro'd it.

[Kevin Buzzard]

Or if you didn't ever intro it, you might want to rcases it.

[Patrick Massot]

Dan, you probably missed the assumption_1 -> assumption_2 -> assumption_3 -> conclusion idiom.

[Patrick Massot]

And also the fact you can put assumptions left of the colon.

[Dan Abolafia]

This is what I was doing.

def prime (n : ℕ) : Prop := ∀ m : ℕ, 1 < m ∧ m < n → ¬(m ∣ n)
def composite (n : ℕ) : Prop := n >= 2 ∧ ¬ prime n

lemma composite_factors (n : ℕ) (ngt2 : n >= 2) : composite n ↔ ∃ (a b : ℕ), 1 < a ∧ a < n ∧ 1 < b ∧ b < n ∧ a * b = n := sorry

(also spawned my question about chained inequalities)

So I could instead write

lemma composite_factors' (n : ℕ) (ngt2 : n >= 2) : composite n ↔ ∃ (a b : ℕ), 1 < a → a < n → 1 < b → b < n → a * b = n := sorry

In the body, I would write λ (h1 : 1 < a) (h2 : a < n) (h3 : 1 < b) (h4 : b < n), ...
instead of have h1 : 1 < a, from h.1, have h2 : a < n, from h.2.1, have h3 : 1 < b, from h.2.2.1, have h4 : b < n, h.2.2.2, ...

[Reid Barton]

No no, composite_factors is correct and composite_factors' is not

[Reid Barton]

in this case you can just pattern match wherever you assume the exists statement, either using rintro (as mentioned above) or lambda with pattern matching

[Reid Barton]

In other situations though it's not that uncommon to see things like h.2.2.2.2. Another alternative is to use a structure.

[Mario Carneiro]

Note that this would make h.2 ambiguous if h : p ∧ q ∧ r