Stream: maths

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 :=


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 α


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

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

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]⟩


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

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.

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


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