avoiding bit0 bit1 when using <-one_div_one

Stream: new members

[Amaury Hayat]

Hi !
I have a question concerning the encoding bit0/bit1, I would like to prove for instance:

example (x0 x1: ℝ)
  (h0 : -(6 + x0) * (real.cosh (1 + x1))<0) :
  -(6 + x0) *(real.cosh (1/1 + x1)) <0 :=
begin
 sorry,
end

I expected rwa [<-one_div_one] at h0,
to do the job, but the state after using rw [<-one_div_one] becomes
-(bit0 (bit1 (1 / 1)) + x0) *real.cosh (1 / 1 + x1)< 0 instead of the desired -(6 + x0) *(real.cosh (1/1 + x1)) <0 , and thus
assumption will not work. How could I fix this ? Is there a way to avoid the state to be expressed with bit0 / bit1 ? Of course one option would simply be to use rwa one_div_one, instead but I wonder whether there is a way to do what I originally planned.
Thanks a lot !

[Alex J. Best]

You could use tactic#conv to pick the right one, like conv in (1+x1) at h0 {rw \l one_div_one } (untested, hopefully i got it right)

[Amaury Hayat]

OK thanks a lot I'll try this :)

[Amaury Hayat]

Hm, Lean does not seem to like the syntax but I am sure conv indeed solves the issue ! More generally, is there a way to transform all pos_num expressed with bit1 and bit0 in the tactic state to regular nat (1,2,3,4,etc.) ?

[Patrick Johnson]

6 is internally represented in terms of 1, so rw doesn't know which 1 you want to rewrite.
Using docs#tactic.interactive.nth_rewrite should work: nth_rewrite 1 ←one_div_one at h0

[Amaury Hayat]

Ok, thanks ! :) I will need to count more carefully the occurences of 1 then