Zulip Chat Archive

Stream: new members

Topic: lifting

Amaury Hayat (Jun 23 2021 at 20:09):

Hello ! Is there a way to use the tactic lift to lift from \nat to \br? For instance I have (a:\nat)(x:\br)and the assumption (h:\uparrow a=x) and I would like to deduce that x is in fact a natural number. I see how to do with \int but for some reason I did not manage with \br.

Johan Commelin (Jun 23 2021 at 20:11):

If you already have a, then you should be able to just use that.

Yakov Pechersky (Jun 23 2021 at 20:11):

What are you going to do after doing the deduction that x is a nat? You know that via h, so just rewrite with h in the appropriate places.

Johan Commelin (Jun 23 2021 at 20:12):

And rw with h, whenever necessary.

Amaury Hayat (Jun 24 2021 at 08:34):

Thanks ! indeed I'll try this way using rw h (quick question by the way, is there a way to rw at a certain location, for instance I have x+x = y+x and h: x = z and for some reason I only want to rewrite the first x and not all of them ?). Concerning the lift there are still some things I don't understand: if I look at this mwe:

example (s :   ) (f :   ) (x : )
  (d1 : (s 1) = (1:)) :
  (s (1:)) = (1:):=

Using assumption won't work although looking at the state \uparrow 1 belongs to \br (so it should be the same thing as (1:\br) ?). If I use convert d1 it reduces to 1 = \uparrow 1 and then refl, trivial, or dec_trivial don't work but finishdoes so I guess there is some rule that finish applies that I don't get.

Kevin Buzzard (Jun 24 2021 at 08:42):

This is the second time that the rewrite question has come up in the last 24 hours, perhaps it's worth putting something in the docstring. See here for rewrite question.

Amaury Hayat (Jun 24 2021 at 08:55):

Thanks a lot ! Sorry for asking a question that has already been asked...

Kevin Buzzard (Jun 24 2021 at 08:56):

oh don't worry about that :-) This site is huge now. Occasionally I do a site search when asking a question which I feel must have come up before.

Amaury Hayat (Jun 24 2021 at 09:12):

I'll do this more carefully next time :-)

Yakov Pechersky (Jun 24 2021 at 12:43):

You can prove this after your convert with "norm_cast", or without convert using "nth_rewrite_rhs 0 <-d1" then some combination of congr and simp

Amaury Hayat (Jun 24 2021 at 14:16):

Thanks a lot ! That's very helpful :) I am still a little puzzled that (1:\br)and \uparrow 1 are not the same thing in this example, what is the difference ?

Eric Rodriguez (Jun 24 2021 at 14:18):

↑1 is the liftingof ℕ's 1 into an arbitrary semiring, whie (1 : ℝ) is ℝ's literal 1

Johan Commelin (Jun 24 2021 at 14:18):

They are provably equal, but not the same by definition.

Eric Rodriguez (Jun 24 2021 at 14:18):

they are ofc equal but not defeq

Yakov Pechersky (Jun 24 2021 at 14:27):

The pretty printer shows arrows instead of type ascriptions. But that doesn't mean it's best practice to use arrows to imply coercions or type ascriptions

Yakov Pechersky (Jun 24 2021 at 14:28):

Until the elaboration can guess what you mean by (\u 1), it's not determined what that expression means

Amaury Hayat (Jun 24 2021 at 21:28):

Ok, \u 1 is a bit different from what I thought then. Thanks a lot for the explanation, I learn many things here !

Last updated: Dec 20 2023 at 11:08 UTC