Zulip Chat Archive

Stream: maths

Topic: Lists: head versus last


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 08 2020 at 15:55):

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

view this post on Zulip 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!

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:01):

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.

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:02):

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

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:03):

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

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:04):

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

view this post on Zulip Eric Wieser (Dec 08 2020 at 16:04):

list.ilast is the symmetric version of list.head

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:04):

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

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:04):

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

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:05):

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

view this post on Zulip 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.

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:06):

Mmm.

view this post on Zulip 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

view this post on Zulip 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) := ...

view this post on Zulip 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.

view this post on Zulip 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 )

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:15):

You might like list.sorted

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:15):

Oh that's nice.

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:15):

sorted (>) l or something.

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:22):

Very rough sketch

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:30):

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

view this post on Zulip 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.)

view this post on Zulip 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'

view this post on Zulip 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?

view this post on Zulip 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]⟩

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:33):

Yes, docs#list.chain'_iff_pairwise

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:34):

What are you using ring_theory.ideal.prod for?

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:34):

docs#list.sorted_of_sorted_cons might also work here.

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 16:35):

Just wanted an import that worked

view this post on Zulip Wrenna Robson (Dec 08 2020 at 16:35):

Fair.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 17:02):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Wrenna Robson (Dec 08 2020 at 17:08):

But I like the way you did it.

view this post on Zulip Yakov Pechersky (Dec 08 2020 at 17:11):

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

view this post on Zulip Wrenna Robson (Dec 08 2020 at 17:11):

RIght.

view this post on Zulip 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

view this post on Zulip Wrenna Robson (Dec 08 2020 at 17:28):

Thank you.

view this post on Zulip 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 ).

view this post on Zulip 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.

view this post on Zulip Wrenna Robson (Dec 08 2020 at 17:32):

Aye.


Last updated: May 06 2021 at 17:38 UTC