# Zulip Chat Archive

## Stream: general

### Topic: option.rec.elim

#### Kevin Buzzard (Jul 21 2018 at 12:46):

I don't want to prove the goal here, I want to prove an intermediate lemma: `∀ x : γ, option.map f (k x) = j x`

.

So what's going on is `f : α → β`

and `g : β → α`

with `f ∘ g = id`

. Given a function `j : γ → option β`

I want to lift it to `k : γ → option α`

using `g`

and then prove that applying `f`

(or more precisely `option.map f`

) to `k`

gets you back to `j`

. All this is happening in the middle of a tactic proof:

example (α β γ : Type) (f : α → β) (g : β → α) (H : ∀ b : β, f (g b) = b) (j : γ → option β) : 1 = 1 := begin let k : γ → option α := λ x, -- match (j x) with -- | none := none -- | some b := some (g b) -- end, -- here written out in term mode option.rec_on (j x) (none : option α) (λ b, some (g b)), have : ∀ x : γ, option.map f (k x) = j x, -- what I actually want -- this should be trivial by casing on j x -- if j x is none then by definition k x is none so f (k x) is none -- if j x is some b then map f (k x) = some (f (g b)) = some b intro x, cases (j x), -- first goal now option.map f (k x) = none -- but assumption that j x = none nowhere to be seen repeat {sorry} end

I want to do a `cases`

on `j x`

but I can't seem to do it directly. How do I eliminate `j`

?

#### Kenny Lau (Jul 21 2018 at 12:48):

example (α β γ : Type) (f : α → β) (g : β → α) (H : ∀ b : β, f (g b) = b) (j : γ → option β) : let k : γ → option α := λ x, option.rec_on (j x) (none : option α) (λ b, some (g b)) in ∀ x : γ, option.map f (k x) = j x := begin end

#### Kevin Buzzard (Jul 21 2018 at 12:48):

thanks -- had not occurred to me to use let in the statement. This is a rather more elegant way of asking the question.

#### Kenny Lau (Jul 21 2018 at 12:50):

example (α β γ : Type) (f : α → β) (g : β → α) (H : ∀ b : β, f (g b) = b) (j : γ → option β) : let k : γ → option α := λ x, option.rec_on (j x) (none : option α) (λ b, some (g b)) in ∀ x : γ, option.map f (k x) = j x := begin intros k x, dsimp [k], cases j x, refl, simp [option.map, option.bind, H], end

#### Kevin Buzzard (Jul 21 2018 at 12:52):

`dsimp [k]`

does the substitution. That's what I was missing. Thanks a lot Kenny!

#### Kevin Buzzard (Jul 21 2018 at 12:56):

In my actual use case I end up with a term involving `id_rhs`

. I'd never heard of this! It's defined in core lean as `abbreviation id_rhs (α : Sort u) (a : α) : α := a`

. I've never heard of `abbreviation`

either!

#### Kenny Lau (Jul 21 2018 at 12:57):

In my actual use case I end up with a term involving

`id_rhs`

.

consequence of using too many tactics

#### Kenny Lau (Jul 21 2018 at 12:57):

don't use any tactic in the definition of anything

#### Chris Hughes (Jul 21 2018 at 12:57):

You could even do this

example (α β γ : Type) (f : α → β) (g : β → α) (H : ∀ b : β, f (g b) = b) (j : γ → option β) : let k : γ → option α := λ x, do y ← (j x), return (g y) in ∀ x : γ, option.map f (k x) = j x :=

#### Kenny Lau (Jul 21 2018 at 12:58):

says the tacticmaster

#### Chris Hughes (Jul 21 2018 at 13:03):

example (α β γ : Type) (f : α → β) (g : β → α) (H : ∀ b : β, f (g b) = b) (j : γ → option β) : ∀ x : γ, (do y ← (j x), return (f (g y))) = j x := by simp [H]

#### Chris Hughes (Jul 21 2018 at 13:04):

In my actual use case I end up with a term involving

`id_rhs`

. I'd never heard of this! It's defined in core lean as`abbreviation id_rhs (α : Sort u) (a : α) : α := a`

. I've never heard of`abbreviation`

either!

I think abbreviation is more or less the same as reducible

#### Kevin Buzzard (Jul 21 2018 at 13:08):

*boggle* `option.map.none'`

is what I want to use to finish my base case, but alpha and beta have to be in the same universe and this is exactly the situation I'm not in :-)

#### Kevin Buzzard (Jul 21 2018 at 13:10):

First few lines of `data/option.lean`

in mathlib:

namespace option universe u variables {α β : Type u}

and then things like `@[simp] theorem map_none' {f : α → β} : option.map f none = none := rfl`

. Why are alpha and beta in the same universe?

#### Kevin Buzzard (Jul 21 2018 at 13:12):

I will have to use the non-API `refl`

:-)

#### Kevin Buzzard (Jul 21 2018 at 15:33):

This is still no good in my use case -- I want to do `cases (j x)`

and in the case `some val`

I would like to keep track of the fact that `j x = some val`

because I will need to know this later. Am I somehow doing the wrong thing entirely, or is there a trick I'm missing?

#### Kevin Buzzard (Jul 21 2018 at 15:38):

Maybe I can refactor exactly what I want out as some awful ugly auxiliary lemma

#### Kevin Buzzard (Jul 21 2018 at 15:40):

I am supposed to be spending the weekend doing continuous valuations, and all I am doing is slowly proving that some definition doesn't depend on which universe I use :-/ I am just trusting that Mario is right when he says I need to make the type of Gamma the same as the type of R. My fear is that if I don't go through this pain now then I'll go through worse pain later.

#### Chris Hughes (Jul 21 2018 at 15:45):

This is still no good in my use case -- I want to do

`cases (j x)`

and in the case`some val`

I would like to keep track of the fact that`j x = some val`

because I will need to know this later. Am I somehow doing the wrong thing entirely, or is there a trick I'm missing?

try `destruct (j x)`

#### Mario Carneiro (Jul 21 2018 at 15:47):

and then things like @[simp] theorem map_none' {f : α → β} : option.map f none = none := rfl. Why are alpha and beta in the same universe?

OMG! No wonder that thing never works

#### Kenny Lau (Jul 21 2018 at 15:48):

lol

#### Mario Carneiro (Jul 21 2018 at 15:48):

This is why I make a habit of avoiding explicit universes whenever possible

#### Kevin Buzzard (Jul 21 2018 at 15:52):

`destruct (j x)`

@Chris Hughes this is *exactly* what I needed! This just saved me a huge refactoring pain! Thanks a lot! Even though I could see my lemma was unprovable I kept going, because I could see I could reduce it to exactly the hypothesis which wasn't in the context :-) I was worried I was wasting my time but using destruct instead gave me exactly what I needed. Wow, who needs `cases`

!

#### Kevin Buzzard (Jul 21 2018 at 15:53):

OMG! No wonder that thing never works

If you hadn't told me to be universe polymorphic I'd never have spotted this :-) Thanks also to @Johan Commelin -- your "come on, it's just a glorified axiom of infinity" was what persuaded me to go back to `Type u`

-- that and Mario saying that sticking to `Type`

was futile anyway.

I am still kind-of fearing the discussion I'll one day have with a serious ZFC-ist who will be horrified that I am assuming the existence of universes when teaching my students undergraduate level maths. This is perfectoid spaces stuff but still -- Scholze's section 4 implies it can all be done in ZFC, and I'm not doing it in ZFC. Perhaps I should try and understand better what Mario was saying about all this a week or two ago.

#### Kenny Lau (Jul 21 2018 at 15:58):

how do you do category without universes?

#### Mario Carneiro (Jul 21 2018 at 16:13):

You aren't *using* universes so much as playing fast and loose with them. It *can* all be made precise and ZFC like, you just aren't bothering

#### Mario Carneiro (Jul 21 2018 at 16:13):

that's what you should tell the ZFC-ist

#### Mario Carneiro (Jul 21 2018 at 16:14):

you would certainly be in good company in doing so

#### Mario Carneiro (Jul 21 2018 at 16:19):

If you want an equality proof in your `cases`

, you can use `cases h : e`

instead of just `cases e`

#### Mario Carneiro (Jul 21 2018 at 16:19):

I think `destruct`

is just a longer way to say `cases`

#### Kevin Buzzard (Jul 21 2018 at 16:26):

If you want an equality proof in your

`cases`

, you can use`cases h : e`

instead of just`cases e`

Yes it sounds like this would have done as well. I've seen `cases e with ...`

but I hadn't realised how to name the hypothesis (or I had seen it before and forgotten).

#### Mario Carneiro (Jul 21 2018 at 16:28):

and if that doesn't work you can also split the generalization and cases steps by using `generalize h : e = x`

first and then `cases x`

#### Kevin Buzzard (Jul 21 2018 at 16:35):

how do you do category without universes?

So you don't prove general theorems about categories, you prove results about the categories which you care about. For example I'm a number theorist so I might have a representation $\rho : G\to GL(n,k)$ and I might want to take its universal deformation. I might *say* "now consider the category whose objects are local rings $R$ with an identification of the residue field with $k$, such that these rings are projective limits of Artin local rings, and consider the functor from this category to the category of sets sending $R$ to the set of lifts of $\rho$ to $\tilde{\rho} : G \to GL(n,R)$ which lift $\rho$; then under certain finiteness assumptions on $G$ this functor is representable by some pair $R^{univ},\rho^{univ}$. Now consider the following elements of $R^{univ}$... . But when the ZFCist challenges me I say "aah there's a trick. I can prove that given any object $R$ of this category I can replace it with a subring $R'$ with cardinality at most $\kappa(R,k)$ for some explicit cardinal $\kappa$ such that anything interesting happening happens already in $R'$ (all this can be made rigorous but this is not the place to do it), so we can just consider the category of rings $R'$ with cardinality at most $\kappa$ and this is equivalent to a *small* category which is a set, and I can reformulate the statement I want purely as a statement about this latter set, so I didn't use universes after all".

#### Kevin Buzzard (Jul 21 2018 at 16:36):

And in the past I have linked to explicit places in the stacks project and in work of Scholze, where explicit arguments of this nature are given, always of this form ("we only need to consider things of size 2^2^2^(max(stuff we're looking at right now)), so we're all OK").

#### Kevin Buzzard (Jul 21 2018 at 16:37):

So that's how an actual working mathematician does categories without universes

#### Kevin Buzzard (Jul 21 2018 at 16:38):

I have no idea what the category theorist do and I'm not sure I care. Probably some work in ZFC and some don't.

#### Kevin Buzzard (Jul 21 2018 at 16:38):

All I know is that the universes showing up in the category theory stuff which me and my number theory colleagues use can all be dealt with in this way.

#### Kevin Buzzard (Jul 21 2018 at 16:55):

If you want an equality proof in your

`cases`

, you can use`cases h : e`

instead of just`cases e`

`e`

is a term here. `cases (h : e)`

doesn't typecheck (and indeed makes no sense). `cases h : e`

does work but now I look at it it looks pretty weird.

#### Mario Carneiro (Jul 21 2018 at 16:58):

it's meant to be suggestive of the `h : e = x`

hypothesis you get

#### Mario Carneiro (Jul 21 2018 at 16:59):

it looks better in `generalize`

, but in `cases`

it doesn't make sense to have a `= x`

there

#### Mario Carneiro (Jul 21 2018 at 17:00):

By the way, in tactic documentation `e`

is often used as a placeholder for a term or `e`

xpression, while `x`

is a variable

Last updated: May 14 2021 at 04:22 UTC