Zulip Chat Archive

Stream: new members

Topic: flatten conjunction access


view this post on Zulip Dan Abolafia (Mar 29 2020 at 18:07):

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)

view this post on Zulip Patrick Massot (Mar 29 2020 at 18:08):

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).

view this post on Zulip Dan Abolafia (Mar 29 2020 at 18:12):

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 18:14):

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.

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2020 at 18:14):

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

view this post on Zulip Dan Abolafia (Mar 29 2020 at 18:16):

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?

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 18:17):

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 18:18):

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 18:18):

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

view this post on Zulip Patrick Massot (Mar 29 2020 at 18:19):

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

view this post on Zulip Patrick Massot (Mar 29 2020 at 18:19):

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

view this post on Zulip Dan Abolafia (Mar 29 2020 at 18:39):

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, ...

view this post on Zulip Reid Barton (Mar 29 2020 at 18:56):

No no, composite_factors is correct and composite_factors' is not

view this post on Zulip Reid Barton (Mar 29 2020 at 18:57):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 18:58):

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.

view this post on Zulip Mario Carneiro (Mar 29 2020 at 21:54):

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


Last updated: May 10 2021 at 18:22 UTC