lifting

Stream: new members

[Amaury Hayat]

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]

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

[Yakov Pechersky]

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]

And rw with h, whenever necessary.

[Amaury Hayat]

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:ℝ):=
begin
  sorry
end

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]

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]

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

[Kevin Buzzard]

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]

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

[Yakov Pechersky]

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]

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]

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

[Johan Commelin]

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

[Eric Rodriguez]

they are ofc equal but not defeq

[Yakov Pechersky]

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]

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

[Amaury Hayat]

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