Zulip Chat Archive

Stream: general

Topic: option.rec.elim


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

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

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

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

view this post on Zulip Kevin Buzzard (Jul 21 2018 at 12:52):

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

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

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

view this post on Zulip Kenny Lau (Jul 21 2018 at 12:57):

don't use any tactic in the definition of anything

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

view this post on Zulip Kenny Lau (Jul 21 2018 at 12:58):

says the tacticmaster

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

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

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

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

view this post on Zulip Kevin Buzzard (Jul 21 2018 at 13:12):

I will have to use the non-API refl :-)

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

view this post on Zulip Kevin Buzzard (Jul 21 2018 at 15:38):

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

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

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

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

view this post on Zulip Kenny Lau (Jul 21 2018 at 15:48):

lol

view this post on Zulip Mario Carneiro (Jul 21 2018 at 15:48):

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

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

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

view this post on Zulip Kenny Lau (Jul 21 2018 at 15:58):

how do you do category without universes?

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

view this post on Zulip Mario Carneiro (Jul 21 2018 at 16:13):

that's what you should tell the ZFC-ist

view this post on Zulip Mario Carneiro (Jul 21 2018 at 16:14):

you would certainly be in good company in doing so

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

view this post on Zulip Mario Carneiro (Jul 21 2018 at 16:19):

I think destruct is just a longer way to say cases

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

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

view this post on Zulip 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 ρ:GGL(n,k)\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 RR with an identification of the residue field with kk, such that these rings are projective limits of Artin local rings, and consider the functor from this category to the category of sets sending RR to the set of lifts of ρ\rho to ρ~:GGL(n,R)\tilde{\rho} : G \to GL(n,R) which lift ρ\rho; then under certain finiteness assumptions on GG this functor is representable by some pair Runiv,ρunivR^{univ},\rho^{univ}. Now consider the following elements of RunivR^{univ}... . But when the ZFCist challenges me I say "aah there's a trick. I can prove that given any object RR of this category I can replace it with a subring RR' with cardinality at most κ(R,k)\kappa(R,k) for some explicit cardinal κ\kappa such that anything interesting happening happens already in RR' (all this can be made rigorous but this is not the place to do it), so we can just consider the category of rings RR' 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".

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

view this post on Zulip Kevin Buzzard (Jul 21 2018 at 16:37):

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

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

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

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

view this post on Zulip Mario Carneiro (Jul 21 2018 at 16:58):

it's meant to be suggestive of the h : e = x hypothesis you get

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

view this post on Zulip 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 expression, while x is a variable


Last updated: May 14 2021 at 04:22 UTC