# Zulip Chat Archive

## Stream: maths

### Topic: Lists: head versus last

#### Wrenna Robson (Dec 08 2020 at 15:47):

Why, conceptually, are `list.head`

and `list.last`

different?

```
def list.last {α : Type u} (l : list α) :
l ≠ list.nil → α
```

Reasonable - given a list of some type and proof the list isn't empty, give its last element.

```
def list.head {α : Type u} [inhabited α] :
list α → α
```

Given a list of some inhabited type, give either the first element of the list, or if the list is empty, default α. This means we have `list.last_mem`

, but there isn't (and cannot be?) any `list.head_mem`

. I don't really understand why these work in two different ways.

#### Wrenna Robson (Dec 08 2020 at 15:49):

It is a bit of a headache as the head is quite natural to work with, more so than the last element, and I'm in a context where I'm dealing with non-empty lists.

#### Eric Wieser (Dec 08 2020 at 15:54):

```
lemma list.head_mem {α : Type*} (l : list α) (h : l ≠ list.nil) [inhabited α] : l.head ∈ l :=
list.mem_of_mem_head' $ list.head_mem_head' h
```

#### Eric Wieser (Dec 08 2020 at 15:55):

Although that doesn't answer the question of why they're defined differently

#### Wrenna Robson (Dec 08 2020 at 15:56):

Indeed, not so hard to whip up my own custom lemma, but seemed a bit odd that they were defined like this to me!

#### Wrenna Robson (Dec 08 2020 at 16:01):

`list.tail`

has the following type:

```
def list.tail {α : Type u} :
list α → list α
```

(With`list.nil`

sent to `list.nil`

.)

With `list.init`

defined in a similar way. So there's sort of a symmetry here which isn't present for the "other" operations.

#### Yakov Pechersky (Dec 08 2020 at 16:02):

There's also `head'`

which gives an `option α`

, with `none`

is the list is empty.

#### Wrenna Robson (Dec 08 2020 at 16:03):

Aye, indeed: and a corresponding last'. Which is reasonable!

#### Yakov Pechersky (Dec 08 2020 at 16:04):

And perhaps the `list.nil`

case would already be taken care of by something upstream.

#### Eric Wieser (Dec 08 2020 at 16:04):

`list.ilast`

is the symmetric version of `list.head`

#### Yakov Pechersky (Dec 08 2020 at 16:04):

So you'd have a `l ≠ list.nil`

hypothesis, and an `l = a :: l'`

hypothesis.

#### Yakov Pechersky (Dec 08 2020 at 16:04):

So you wouldn't even need `head`

, you'd just use `a`

.

#### Wrenna Robson (Dec 08 2020 at 16:05):

`list.cons_head_tail`

and `list.init_append_last`

both require the `l ≠ list.nil`

hypothesis.

#### Yakov Pechersky (Dec 08 2020 at 16:06):

Proofs about lists often use `induction`

so that the empty and `hd :: tl`

cases are dealt with separately.

#### Wrenna Robson (Dec 08 2020 at 16:06):

Mmm.

#### Eric Wieser (Dec 08 2020 at 16:08):

Since I missed this - worth noting that there are two doc pages for these basic list definitions: core and mathlib

#### Yakov Pechersky (Dec 08 2020 at 16:09):

So whatever API you're building with lists, you could phrase it instead as

```
lemma something_about_lists {α : Type*} (x : α) (xs : list α) (p : list α -> Prop) : p (x :: xs) := ...
```

#### Wrenna Robson (Dec 08 2020 at 16:09):

Aye, I've been consulting them. Essentially I am defining something (the chains stuff I was talking about previously) - I am trying to decide "which way round" to put my chain. At some point in a proof I am going to want to add an element to the start/end of the chain and I'm trying to decide what the best way to orientate things is.

#### Wrenna Robson (Dec 08 2020 at 16:10):

So my type in question looks like:

```
structure prime_ideal_chain (R : Type u) [comm_ring R] :=
( carrier : list (ideal R))
( primes {I} : I ∈ carrier → ideal.is_prime I )
( is_chain : list.chain' (>) carrier )
( not_nil : carrier ≠ list.nil )
```

#### Wrenna Robson (Dec 08 2020 at 16:13):

I'm getting the biggest element of some C of this type (in this formulation, the head of C.carrier), using C.primes to show that's prime, and then constructing a bigger element and adjoining it to C.carrier and creating a new `prime_ideal_chain`

.

#### Wrenna Robson (Dec 08 2020 at 16:15):

Obviously I could flip everything (then I'd be using `last`

instead) - but I thought this would be nicer; as `head`

isn't symmetrical to `last`

, however, I got to wondering the thought that started the OP.

#### Yakov Pechersky (Dec 08 2020 at 16:15):

You might like `list.sorted`

#### Wrenna Robson (Dec 08 2020 at 16:15):

Oh that's nice.

#### Wrenna Robson (Dec 08 2020 at 16:15):

sorted (>) l or something.

#### Yakov Pechersky (Dec 08 2020 at 16:22):

```
def prime_ideal_chain.cons {R : Type u} [comm_ring R] (bigger : ideal R) (pic : prime_ideal_chain R) :=
⟨bigger :: pic.carrier,
by { simp [bigger.is_prime, pic.primes] }, --uses list.mem_cons_iff
by { simp [show (∀ (I : ideal R), I ∈ pic.carrier), bigger > I), from bigger.is_bigger, pic.is_sorted] } --uses list.sorted_cons,
by simp
⟩
```

#### Yakov Pechersky (Dec 08 2020 at 16:22):

Very rough sketch

#### Wrenna Robson (Dec 08 2020 at 16:30):

Why do you think `sorted`

is better than `chain'`

, incidentally?

#### Wrenna Robson (Dec 08 2020 at 16:31):

(I only have that my bigger element is definitely bigger than the previously-biggest element, y'see.)

#### Wrenna Robson (Dec 08 2020 at 16:32):

I can get quite far using `chain'`

although I'm not sure how to deal with a hypothesis of the form `hy: y ∈ C.carrier.head'`

#### Eric Wieser (Dec 08 2020 at 16:32):

Is there a lemma to convert `chain' r`

to `pairwise r`

given the fact that `r`

is transitive?

#### Yakov Pechersky (Dec 08 2020 at 16:33):

```
import ring_theory.ideal.prod
import data.list.sort
universe u
structure prime_ideal_chain (R : Type u) [comm_ring R] :=
( carrier : list (ideal R))
( primes {I} : I ∈ carrier → ideal.is_prime I )
( is_chain : list.sorted (>) carrier )
( not_nil : carrier ≠ list.nil )
def prime_ideal_chain.mem {R : Type u} [comm_ring R] (I : ideal R) (pic : prime_ideal_chain R) : Prop :=
I ∈ pic.carrier
instance {R : Type u} [comm_ring R] : has_mem (ideal R) (prime_ideal_chain R) := ⟨prime_ideal_chain.mem⟩
lemma prime_ideal_chain.mem_def {R : Type u} [comm_ring R] (I : ideal R) (pic : prime_ideal_chain R) :
I ∈ pic ↔ I ∈ pic.carrier := iff.rfl
def prime_ideal_chain.cons {R : Type u} [comm_ring R] (pic : prime_ideal_chain R) (bigger : ideal R)
(hprime : bigger.is_prime) (hbig : ∀ I ∈ pic, I < bigger):
prime_ideal_chain R :=
⟨bigger :: pic.carrier,
by simpa only [hprime, true_and, forall_eq_or_imp, list.mem_cons_iff] using pic.primes,
by simpa only [pic.is_chain, list.sorted_cons, and_true] using hbig,
by simp only [ne.def, not_false_iff]⟩
```

#### Yakov Pechersky (Dec 08 2020 at 16:33):

Yes, docs#list.chain'_iff_pairwise

#### Wrenna Robson (Dec 08 2020 at 16:34):

What are you using `ring_theory.ideal.prod`

for?

#### Yakov Pechersky (Dec 08 2020 at 16:34):

docs#list.sorted_of_sorted_cons might also work here.

#### Yakov Pechersky (Dec 08 2020 at 16:35):

Just wanted an import that worked

#### Wrenna Robson (Dec 08 2020 at 16:35):

Fair.

#### Wrenna Robson (Dec 08 2020 at 16:37):

Maybe I want to pre-write a way to get the head of a chain along with the fact it's prime also.

#### Yakov Pechersky (Dec 08 2020 at 17:02):

Then perhaps your structure can store what the `head`

is and use `list.chain`

instead?

#### Yakov Pechersky (Dec 08 2020 at 17:06):

```
import ring_theory.ideal.prod
universe u
structure prime_ideal_chain (R : Type u) [comm_ring R] :=
(largest : ideal R)
(rest : list (ideal R))
(primes {I} : I ∈ (largest :: rest) → ideal.is_prime I )
(is_chain : list.chain (>) largest rest)
def prime_ideal_chain.mem {R : Type u} [comm_ring R] (I : ideal R) (pic : prime_ideal_chain R) : Prop :=
I ∈ (pic.largest :: pic.rest)
instance {R : Type u} [comm_ring R] : has_mem (ideal R) (prime_ideal_chain R) := ⟨prime_ideal_chain.mem⟩
lemma prime_ideal_chain.mem_def {R : Type u} [comm_ring R] (I : ideal R) (pic : prime_ideal_chain R) :
I ∈ pic ↔ I ∈ (pic.largest :: pic.rest) := iff.rfl
def prime_ideal_chain.cons {R : Type u} [comm_ring R] (pic : prime_ideal_chain R) (bigger : ideal R)
(hprime : bigger.is_prime) (hbig : pic.largest < bigger):
prime_ideal_chain R :=
⟨bigger,
pic.largest :: pic.rest,
by simpa only [hprime, true_and, forall_eq_or_imp, list.mem_cons_iff] using pic.primes,
by simpa only [pic.is_chain, and_true, list.chain_cons] using hbig⟩
```

#### Wrenna Robson (Dec 08 2020 at 17:07):

mhm. That does work, though I suppose in a sense it would be nice if rest was itself a prime_ideal_chain (because of course it is).

#### Wrenna Robson (Dec 08 2020 at 17:08):

But I like the way you did it.

#### Yakov Pechersky (Dec 08 2020 at 17:11):

Well under this definition, that wouldn't be possible because `[]`

is not a valid chain.

#### Wrenna Robson (Dec 08 2020 at 17:11):

RIght.

#### Yakov Pechersky (Dec 08 2020 at 17:27):

```
import ring_theory.ideal.prod
section prime_ideal_chain
universe u
variables (R : Type u) [comm_ring R]
structure prime_ideal_chain (R : Type u) [comm_ring R] :=
(largest : ideal R)
(rest : list (ideal R))
(primes {I} : I ∈ (largest :: rest) → ideal.is_prime I )
(is_chain : list.chain (>) largest rest)
open prime_ideal_chain
namespace prime_ideal_chain
variable {R}
variables (I : ideal R) (pic : prime_ideal_chain R)
protected def mem : Prop :=
I ∈ (pic.largest :: pic.rest)
variable {I}
instance : has_mem (ideal R) (prime_ideal_chain R) := ⟨mem⟩
lemma mem_def :
I ∈ pic ↔ I ∈ (pic.largest :: pic.rest) := iff.rfl
def cons (hprime : I.is_prime) (hbig : pic.largest < I):
prime_ideal_chain R :=
⟨I, pic.largest :: pic.rest,
by simpa only [hprime, true_and, forall_eq_or_imp, list.mem_cons_iff] using pic.primes,
by simpa only [pic.is_chain, and_true, list.chain_cons] using hbig⟩
lemma is_prime_largest : pic.largest.is_prime :=
begin
apply pic.primes,
simp only [list.mem_cons_iff, true_or, eq_self_iff_true]
end
lemma is_prime_of_rest (h : I ∈ pic.rest) : I.is_prime :=
begin
apply pic.primes,
simp only [h, list.mem_cons_iff, or_true]
end
def of_rest {x : ideal R} {xs : list (ideal R)} (h : pic.rest = x :: xs) :
prime_ideal_chain R :=
⟨x, xs,
λ I hI, pic.is_prime_of_rest (h.symm ▸ hI),
by { apply list.chain_of_chain_cons, convert pic.is_chain, exact h.symm }⟩
end prime_ideal_chain
end prime_ideal_chain
```

#### Wrenna Robson (Dec 08 2020 at 17:28):

Thank you.

#### Wrenna Robson (Dec 08 2020 at 17:29):

Think it is a little easier to have `(primes : largest.is_prime ∧ ∀ I ∈ rest, ideal.is_prime I )`

.

#### Yakov Pechersky (Dec 08 2020 at 17:30):

However you write it (and your way is definitely easier to deconstruct), you might still have an API lemma like `is_prime_largest`

, the proof of which will be just `_.1`

in your case.

#### Wrenna Robson (Dec 08 2020 at 17:32):

Aye.

Last updated: May 06 2021 at 17:38 UTC