Lists: head versus last

Stream: maths

[Wrenna Robson]

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]

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]

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]

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

[Wrenna Robson]

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]

list.tail has the following type:

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

(Withlist.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]

There's also head' which gives an option α, with none is the list is empty.

[Wrenna Robson]

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

[Yakov Pechersky]

And perhaps the list.nil case would already be taken care of by something upstream.

[Eric Wieser]

list.ilast is the symmetric version of list.head

[Yakov Pechersky]

So you'd have a l ≠ list.nil hypothesis, and an l = a :: l' hypothesis.

[Yakov Pechersky]

So you wouldn't even need head, you'd just use a.

[Wrenna Robson]

list.cons_head_tail and list.init_append_last both require the l ≠ list.nil hypothesis.

[Yakov Pechersky]

Proofs about lists often use induction so that the empty and hd :: tl cases are dealt with separately.

[Wrenna Robson]

Mmm.

[Eric Wieser]

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

[Yakov Pechersky]

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]

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]

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]

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]

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]

You might like list.sorted

[Wrenna Robson]

Oh that's nice.

[Wrenna Robson]

sorted (>) l or something.

[Yakov Pechersky]

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]

Very rough sketch

[Wrenna Robson]

Why do you think sorted is better than chain', incidentally?

[Wrenna Robson]

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

[Wrenna Robson]

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]

Is there a lemma to convert chain' r to pairwise r given the fact that r is transitive?

[Yakov Pechersky]

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]

Yes, docs#list.chain'_iff_pairwise

[Wrenna Robson]

What are you using ring_theory.ideal.prod for?

[Yakov Pechersky]

docs#list.sorted_of_sorted_cons might also work here.

[Yakov Pechersky]

Just wanted an import that worked

[Wrenna Robson]

Fair.

[Wrenna Robson]

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]

Then perhaps your structure can store what the head is and use list.chain instead?

[Yakov Pechersky]

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]

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]

But I like the way you did it.

[Yakov Pechersky]

Well under this definition, that wouldn't be possible because [] is not a valid chain.

[Wrenna Robson]

RIght.

[Yakov Pechersky]

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]

Thank you.

[Wrenna Robson]

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

[Yakov Pechersky]

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]

Aye.